The Coq mailing list

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

Maybe the problem has to do with choosing an evar instantiation that 
refers to new local variables created since the birth of that evar?  I'm 
a bit confused by the code below, which defines [t] and [t'] but doesn't 
seem to refer to them.  If they were used somehow to instantiate [e], 
then you would have an instance of the problem I suggested, in which 
you'd want to do something like [let t0 := eval unfold t in t ...] and 
refer to [t0] instead of [t].

On 03/14/2013 04:31 PM, Jason Gross wrote:
> Is there a systematic way to partially instantiate an evar?  That is, 
> if I have an evar [e] and I want to instantiate [e] as [f _ _] for a 
> known [f] (and get the two holes as new evars), is there a way to do 
> that?
>
> I feel like I should be able to do it with something like the 
> following, but I haven't managed to make it work.
>
> Record NT := Build_NT { CO :> forall x : nat, x = x;
>                               HO : CO = CO }.
>       Goal exists x : NT, x = x.
>       clear.
>       esplit.
>       match goal with
>         | [ |- appcontext[?e] ] => is_evar e;
>                                   let T := fresh in let t := fresh in 
> evar (T : Type); evar (t : T); subst T;
>                                   let T' := fresh in let t' := fresh 
> in evar (T' : Type); evar (t' : T'); subst T';
>                                                                       
>   assert (e = @Build_NT (CO e) (HO e))
>       end.
>       apply f_equal2.
>
> Thanks,
> Jason