The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Arnaud Spiwack wrote:
>     As a devoted Adamizer of proof scripts (with a summer's worth of
>     Ltackery to prove it), I can't imagine life without info ...
>
>
> I'd be interested in knowing how you use it.

The usual scenario is that some complex Ltac program isn't behaving as 
expected, so you run that tactic with [info], which outputs the sequence 
of steps taken "at one level lower in the abstraction stack."  Then you 
run each of these tactics, until one behaves unexpectedly.  Now run that 
tactic with [info] and repeat.  This can really be a lifesaver in Ltac 
debugging.  I don't know if some new 8.4 facility compensates.  (I try 
to stick to the Debian testing packages only, so I've only yet 
experienced behaviors up to 8.3.)