The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

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