The Coq mailing list

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

On Wed, Mar 13, 2013 at 09:22:46AM +0100, Arnaud Spiwack wrote:
> 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).

Can you be more specific?  What goes wrong?  Is Qed too slow?  Were you
using types depending on proofs?  Do you consider your practice an hack
to work around an inefficiency?

> I must say, I'm amazed it works.

Why shouldn't it work?  It is exactly what abstract does, but instead of
putting the abstracted term in the environment my code puts it in a
letin.  The type of the term is the same, its body is the same, the
typing rule used to typecheck its occurrences is the same (lookup in the
context/environment for a rel/name to find its type).
Am I missing something? 

Ciao
-- 
Enrico Tassi