The Coq mailing list

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

On 27/02/2015 16:06, Jonathan Leivent wrote:
> Or, perhaps you are suggesting that Ltac is better off without any
> exception-like mechanism?

I think I'm suggesting Ltac is better off without any Ltac.

More seriously, your hack is legitimate, but I just wanted to warn you
not to rely too much on the current semantics of tactics-in-terms. The
only use case where the semantics is fully specified is when:

1. The tactic is totally solving the current hole (so always writing
$(solve [tac])$ is a good idea).
2. The tactic does not mess with the global evars of the current proof
state (do not try to do $(instantiate (i := foobar))$)
3. The tactic do not rely on global side-effects (that currently
includes the abstract tactical).

If you comply with these three conditions, you should be safe regarding
the potential evolutions of the implementation. Still, be careful.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature