Trace shortening

[Tragicus]

Changes a few things in the way the trace is printed so that it takes less space.

• Goals are not aligned with their heads anymore, but have one more indentation than the rid... line.
• Pis are factorized, e.g. pi c0 \ pi c1 \ ... is printed pi c0 c1\ ...

[Tragicus]

@gares I gave it a try but it seems that my vague understanding of how the formatter works is broken. With something like

From elpi Require Import tc.

Elpi Trace.
Elpi Query TC.Solver lp:{{
pi x y\ x = x, x = x, x = x, x = y.
}}.

I see

rid:5 step:1 gid:36 user:curgoal = pi
 pi c0 c1 \
                                          c0 = c0 , c0 = c0 , c0 = c0 , c0 = c1

Do you see what I am doing wrong?

[gares]

When this happens, it is probably that you mix an outer box and/or someone sneaks a \n in confusing the column counter of Format.