The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Mon, Mar 11, 2013 at 11:05:19AM +0100, Arnaud Spiwack wrote:
> I used to think it was pretty much insurmountable a task, but I'm not so
> sure any more. With the proviso that without Enrico's aforementioned branch
> the abstract (and admit) tactic will not work as expected

Just to be sure we understand eachother.  

In my branch abstract does not imperatively alter the environment to
insert the abstracted lemma to make Qed happy.  It adds to the proof
state enough information so that the procedure generating the proof term
actually generates a local letin within the main proof for the abstracted
piece of the proof.  The letin should be made opaque, but this is a
detail.  The important thing is that the system does not expect
abstracted lemmas to magically apper in the environment.

The admit tactic is just implemented as "case daemon" where daemon is
an Axiom of False.  Again no side effects (no axiom injected into the
environment by the tactic).

Unfortunately the code (for abstract) is not easy to disentagle from
the rest of the patch.  It is a general mechanism to declare "side
effects", like an abstracted sub lemma or an elimination principle
generated on the fly, that touches many layers, from the tactics to
the kernel IIRC.

Cheers
-- 
Enrico Tassi