The Coq mailing list

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

On Wed, 22 Apr 2020 00:16:12 -0400
Jason Gross 
<jasongross9 AT gmail.com>
 wrote:

> Examples: I have some Ltac2 files in
> https://github.com/JasonGross/doctoral-thesis/tree/master/performance-experiments
> (see
> files with ltac2 in the names)
> There's also two implementations of reification using a slightly older
> version of Ltac2 at
> https://github.com/mit-plv/reification-by-parametricity (see files
> starting with Ltac2)

Thanks for that, Jason!

> 
> I believe the exception-catching mechanism is Control.case (in
> https://github.com/coq/coq/blob/master/user-contrib/Ltac2/Control.v).
>  It can catch exceptions from Control.zero, and the bit you were
> reading about uncatchable exceptions was probably talking about those
> raised by Control.throw.

Oh - I was not making the connection between "catching an exception"
and tactic branching - which is what zero, plus, and case appear to be
for.  It looks like zero is like Ltac1's fail, and plus is like Ltac1's
'+' branching tactical.  I'm not sure what case is for, though.  And I
don't see how this semantics eliminates the need for those kludgy Ltac1
numeric failure levels.  Is there a way to catch conditionally based on
type, allowing non-matching values to continue to unwind?  I think that
how proof state and backtracking is handled by the monad needs to be
described in more detail for those