An API for info traces.
TEMP! Print info trace on all tactics.
Info: dispatching-branches are declared as such in the info trace.

Hence dispatches are printed as dispatches rather than sequences.
Info: print a name for the primitive tactics in [Proofview].

The name is chosen in accordance to Ltac's syntax. In particular [refine] prints as Ltac's refine, which is not entirely correct (Ltac's refine does some βι-reduction after refinement). Maybe it would be better to give make it clear that it is a different refine. Still in refine, the constr is printed without taking into account the new evars, which, apart from potentially getting the order of the goals wrong, prints new evars as ?x instead of ?[x]. A printer for terms with new evars will be necessary.

In the case of [V82.tactic], the name is just <unknown> because there is no way to retrieve any information. It won't appear in the first level of info in Ltac, however, if the user would require a deeper trace, he may see internal tactics (Tactics defined with TACTIC EXTEND also have weird, unparsable, internal names).
Info: Ltac's idtac logs its message in the info trace.
Add a interpreted level [tacexpr] to [Tacexpr] together with its printer.

Re-add, in fact, since it was there in v8.3 but was dead code in v8.4 hence was deleted. It is necessary for printing info traces, however. A lot of the code had changed since v8.3, so adapting the code was non-trivial and some thing may be printed wrong.

It require re-adding a [tacexpr] argument to [gen_tactic_expr]. It had been made obsolete by the deletion of [pr_tactic] in v8.4 (even though printing [glob_tactic_expr] in a [tactic_expr] is only an approximation of the appropriate behaviour).

A new kind of argument, [delayed_constr], has made an appearance between v8.4 and trunk, and it differs from [constr] in the typed level. So it required its own parameter in [gen_tactic_expr]. At this point [delayed_constr] are printed in the globalised level because they are interpreted as closures. Maybe a better approximation is warranted.

Both in the printing of rewrite and induction, I changed a [pr_lconstr] (note the 'l') by a [pr_dconstr]. It is probably not quite correct, and may need fixing (adding a [pr_dlconstr] to [Pptactics] I guess?).
Info: a few atomic Ltac tactics declare their names.
More tactics record their names.
Inversion prints its name.
Info: placeholder for the tactics which are still in old style in tacinterp.
Tactics coming from [TACTIC EXTEND] register their names.
Tentative commit for TacAlias (tactic notations) to register their names.
Info: name calls to Ltac constants.
Info: print correctly Ltac-level aliases.

Previously: would keep only one of a class of aliases.
Info: print correctly Ltac definitions which are not syntactically functions or tactics.

Previous version lost the name for [Ltac t := let … in …], or [match], etc…
Don't raise an error when printing intro-patterns in [functional induction].
Info: a function to collapse the info trace and observe a deeper level of tactics.
Info: add syntax entry for the info command.
Info: Proof.run_tactic exports info trace.
Info: plug Info command syntax in.