The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 02/27/2015 06:13 AM, Pierre-Marie Pédrot wrote:
> On 27/02/2015 04:31, Jonathan Leivent wrote:
> > However, in 8.5, one can do the following:
> >
> >      Inductive maybeException {T:Type} : Type :=
> >      | Exception(val:T)
> >      | NoException(val:T).
> >
> >      Axiom raised : forall T (val:T) X, X.
> >
> >      Ltac raise val := apply (raised _ val).
> >
> >      Ltac catch tac type :=
> >        let X:=constr:($(tac)$ : type) in
> >        lazymatch X with
> >        | context [raised] =>
> >          multimatch X with
> >          | context [raised _ ?V _] => constr:(Exception V)
> >          end
> >        | _ => constr:(NoException X)
> >        end.
> The more I see the horrendous hacks people build up using tactics in
> terms, the more I regret having introduced this feature without thinking
> twice about how people use Ltac.
>
> Timeo tacticas et dona ferentes...
>
> PMP

Again, I apologize for yet another "horrendous hack" - but this one I 
thought was both rather mild and useful.  Also, I don't think the mere 
introduction of an exception-like mechanism into Ltac would violate 
"Arnaud's Dictum" that Ltac is not and should not become a full 
programming language.  And even if there were good documentation on how 
to write OCaml plugins, would creating exceptions there be an easy task?

Or, perhaps you are suggesting that Ltac is better off without any 
exception-like mechanism?

-- Jonathan