The Coq mailing list

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

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

Attachment: signature.asc
Description: OpenPGP digital signature