The Coq mailing list

[t x <txrev319 AT gmail.com>]

After something like 6 months of Coq, I finally came up with this trick:

Ltac log expr :=
  let l := fresh "log__" in
    set (l := expr).

which I've found to be much more useful than both idtac and "Set Ltac Debug on" for debugging since I can now do things like:

match expr

| blah blah blah => ... ; log ("we're doing XYZ using", x, y, z)
...

end

This now means that when I see unprovable goal, I can look at the log__ strings and understand "what stupidity did I do to get into this unprovable state."

At the risk of starting a chain mail spam -- anyone have really cool Ltac tricks / Ltac debugging tricks that completely changed their ltac development cycle they want to share?

(If you don't want to spam the list, feel free to reply to me only -- I'll happily read duplicate emails in search of cool hacks).