The Coq mailing list

[John Grosen <jmgrosen AT mit.edu>]

I am currently dealing with a problem in which I have an existential
variable in the goal and want to apply a lemma to the goal, but Coq's
unifier is not powerful enough to automatically unify the relevant part
of the lemma with the evar. However, in this particular case, it is
programatically obvious how to unify them, so I would like to write some
Ltac to do so. Imagine this (greatly simplified) example:

  Goal exists (n : nat), n = 2.
    evar (n : nat).
    exists n.
    only [n]: refine (S _).

This works, but I usually don't have a name for the existential
variables I'm dealing with and the automation certainly doesn't know
about any. So what I'd like to do is this:

  Goal exists (n : nat), n = 2.
    eexists.
    match goal with
    | [ |- ?x = _ ] =>
      only [x]: refine (S _)
    end.

However, Coq complains with "No such goal." As far as I can tell, this
is because the argument in "only [_]" is a syntactic identifier.

Then, is there any way to select a goal with a non-syntactic identifier,
like I have in this situation?

Thanks,
John