@Pierre-Marie Pédrot : the manual says at (https://coq.github.io/doc/master/refman/proof-engine/ltac2.html#exception-catching) that Ltac2 has proper exception catching. I wonder what the syntax is - the standard OCaml syntax doesn't work and looking at the .gml file also didn't enlighten me. Up to now I use a match! with an additional catch branch, but this doesn't allow me to catch only exceptions of a specific type. How would I do that?
This refers to the backtracking mechanism, not the panic one.
To catch an exception you can use Control.plus or Control.case, depending on the exact semantics you want.
There is no dedicated syntax for this, but you can roll your own notation.
Thanks, I will try that!
Last updated: May 31 2023 at 02:31 UTC