The Coq mailing list

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

> ...
> > 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 

Oops - that last bit got truncated - it said "those of us unfamiliar
with Coq internals".

I think I am beginning to understand how case works - it looks like
Ltac1's "try tac", with a result that can be interpreted by a match to
determine if tac succeeded or failed.  The code in user_contrib/Ltac2
is giving me small clues...