The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear John,

then I don't understand your problem. If you want to instantiate the evar in 
the context of the current goal (rather than focus another goal in whose 
context the evar can be instantiated more easily), what is wrong with e.g.:

  Goal exists (n : nat), n = 2.
    eexists.
    reflexivity.

Or maybe 
   
  Goal exists (n : nat), n = 2.
    eexists.
    match goal with
    | [ |- ?x = _ ] => is_evar x; reflexivity
    end.

Or in case you have an evar in a term:

  Goal exists (n m : nat), n + m = 2.
    eexists.
    eexists.
    match goal with
    | [ |- ?x + ?y = _ ] => assert(x=0) as H by reflexivity; clear H
    end.

The problem with your example is that you cannot possibly instantiate the 
evar with 0, because this would lead to 0=2. If none of the above works, it 
would help if you post a minimal sample which actually could work (doesn't 
lead to False) and whose solution would solve your issue. As is, it is hard 
to guess what your issue is.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928