The Coq mailing list

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

On Thu, Jan 24, 2013 at 06:38:42PM +0100, Thomas Braibant wrote:
> The idea is that when you have a term [T] that contains evars, it is
> possible to transform [T] into a function [F] in which evars have been
> abstracted, applied to these evars

The ssreflect plugin does this all over the place, but the main
motivation is to pass around just a constr (no evar map is needed if the
term is evar free).

If you want to give a look, the function is called pf_abs_evars, but it is
really tricky code.

Cheers
-- 
Enrico Tassi