An API for info traces.
Add [Info] command.

Called with [Info n tac], runs [tac] and prints its info trace unfolding [n] level of tactic names ([0] for no unfolding at all).
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: print the name of atomic tactics.

The printing uses the printer for interpreted tactics. It only works for tactics which are defined in the new style. There are still a few atomic tactics in tacinterp which are defined in [V82] style. Namely:

exact, apply, clear, rename, reduce, change, (mutual variant of) fix, (mutual variant of) cofix

These print placeholder names which are never reparsable and not as useful.
Info: Tactics coming from [TACTIC EXTEND] print their names.

Since PMP's intervention, the [TACTIC EXTEND] tactics are not uniform: some are syntax, and some are just an internal name for an Ltac definition. The latter kind prints an internal name. It may be better to avoid printing them in the trace altogether. But I haven't figured out how to detect that properly yet.
Info: tactic notations (TacAlias) print their names.

Empirically it works better on some notations than on others and I have no idea why. I've seen notations not printing their arguments, for instance, and other printing perfectly.
Info: print name of calls to Ltac constants ([TacCall]).

Some particular care needed to be taken to print aliases properly.

The printing of argument is just the generic printer for [genarg]. The trouble is that (apart from being incomplete), it does not know that it's printing Ltac arguments. As a consequence, the arguments are not properly quoted (e.g. if they are tactic expressions, they are not within [ltac:(...)].
Don't raise an error when printing intro-patterns in [functional induction].
Add an [Info Level] option to print info traces automatically.

[Set Info Level n] prints all info traces at level [n]. [Unset Info Level] stops the automatic printing of info traces. The unfolding level [n] can be overloaded by local [Info m tac] calls.
Info: do not record info trace unless needed.
Info: the warning message of the defunct [info] tactic now points to the [Info] command.
Document [Info] command.