The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

The abstracted term I is there, so the concerns of Adam may be relevant
if you start comparing proofs.  

 

I have written a number of functions using tactics that used abstract to opacify their proofy parts (whithout which they simply couldn't run in an efficient time). It's actually pretty common. It sounds hard to do in your style without having some kind of a "this-subterm-is-opaque" construction in terms.

And yes, you are right, these changes
are non local.  I perform them at the very end, when the proof status is
transformed into a proof term by applying the substitution to the
initial evar.

 

I must say, I'm amazed it works.


--

Arnaud