The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 03/12/2013 07:07 AM, Enrico Tassi wrote:
> > In any case, if you want
> > to have an irreducible/opaque let-in for "abstract", you'll have to stick
> > you hand into Term.constr, won't you?
> >      
> No, an opaque identity function is enough.
>    

But then reduction could still happen within the argument to the 
identity function, right?  That could be a serious performance bottleneck.