Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] vm_compute and evars

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] vm_compute and evars


Chronological Thread 
  • From: Enrico Tassi <enrico.tassi AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] vm_compute and evars
  • Date: Thu, 24 Jan 2013 19:41:40 +0100

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



Archive powered by MHonArc 2.6.18.

Top of Page