The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

I've read through the Ltac2 section of the 8.11 refman, and still have
many qeustions.  Perhaps seeing some examples would help.  Is there
somewhere I can find some links to Ltac2 examples?

The Ltac2 section appears to have been targeted in spots to Coq devs
with Ocaml knowledge.  At one point it says: "We recall that the
Proofview.tactic monad is essentially a IO monad together with
backtracking state representing the proof state."  There are
several other cases of this - so without the Coq Ocaml internals
background info, I'm left with many holes in my understanding.

There are also apparent inconsistencies, or at least omissions, in the
refman.  At the end, it says: "Ltac2 features a proper
exception-catching mechanism. For this reason, the Ltac1 mechanism
relying on fail taking integers, and tacticals decreasing it, has been
removed. Now exceptions are preserved by all tacticals, and it is your
duty to catch them and re-raise them as needed."  But I don't see any
catch mechanism described.  Indeed, at an earlier point, it says:
"There is currently no way to catch such an exception, which is a
deliberate design choice. Eventually there might be a way to catch it
and destroy all backtrack and return values."