The Coq mailing list

[Luke Maurer <maurerl AT cs.uoregon.edu>]

On Jan 6, 2012, at 2:18 AM, Arnaud Spiwack <aspiwack AT lix.polytechnique.fr> 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.

Well, anything from finding out what theorems auto ends up using to figuring out how something like the remember tactic works or debugging my own proof script by checking that it's doing what I think it's doing. Very useful for peeking under the hood when I don't need the fine detail of the debugger.

In the meantime, preferred tools for understanding what ltac does are Set Ltact Debug ( http://coq.inria.fr/distrib/V8.4beta/refman/Reference-Manual012.html#@command244 ) and debug eauto (undocumented, but works just like eauto while outputing debug information).

The debugger is sometimes helpful, but as Adam said, the lack of control over granularity can make it clumsy to use or worse. I wasn't aware of debug eauto though - thanks, that should cover part of my needs.

- Luke