The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 27/02/2015 16:06, Jonathan Leivent wrote:
> And even if there were good documentation on how to write OCaml
> plugins, would creating exceptions there be an easy task?

Forgot to answer this question: yes, you can do this in a
straightforward way. I think you can write two ML tactics

raise val
try t (fun x -> u)

with the expected semantics. Still, it would look like an addendum to
Ltac not really fitting into the landscape, and making its kludgy nature
grow even more.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature