The Coq mailing list

[Armaël Guéneau <armael.gueneau AT ens-lyon.fr>]

On 29/06/2018 21:20, John M Grosen wrote:
> Unfortunately, the instantiate + refine trick doesn't help in my scenario. 
> In particular, I don't know the index of the existential variable I want to 
> instantiate. 

What about:

   Goal exists (n : nat), n = 42.
     eexists.
     match goal with |- ?x = _ =>
       pose (foo := x);
       instantiate (1 := 42) in (Value of foo)
     end.

In short, it looks like you can introduce a local definition for the
evar you just matched, and then the index of that evar will necessarily
be 1 when you instantiate _in that definition_ using Value of.

And you can still do `unshelve instantiate (1 := _) in (Value of foo)`
to get a goal corresponding to instantiating the evar.