The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

I had a quick look at the code of pf_abs_evar, which seems to do the
same kind of transformation as what I implemented (except that what I
did takes some extra steps to fold applications of terms).

Since we now have at least two versions outside of Coq's code of the
same very useful piece of code, I feel it would be cool to push one of
them in the general code :).
Thomas


On Thu, Jan 24, 2013 at 7:41 PM, Enrico Tassi 
<enrico.tassi AT inria.fr>
 wrote:
> 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