The Coq mailing list

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

OK, I've found that mechanism to be almost impossible to use for most 
debugging tasks.  [info] has been much more useful.  The problem with 
the tactic debugger is that it has an odd notion of the granularity of 
steps, with no way to skip steps beside counting them, rather than 
saying something like "run until we are done evaluating tactic [foo]".  
(Or maybe I'm just not familiar with its capabilities.)  This is 
especially bad when debugging a tactic that calls [intuition], which 
generates many steps that the debugger chooses to show when stepping!

Pierre Courtieu wrote:
> It is the same command.
> P.
>
> 2012/1/6 Adam Chlipala 
> <adamc AT csail.mit.edu>:
>   
> > Pierre Courtieu wrote:
> >     
> > > For this use there is a debug mechanism for Ltac. It has been there
> > > for a while but is now shortly documented
> > > (http://coq.inria.fr/coq/refman/Reference-Manual012.html#@default763).
> > >
> > > Set Ltac Debug.
> > >
> > >       
> > Is this different from [Debug On]?
> >