The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I do not have access to Coq at the moment, but does something like this work?
Goal Type.
  refine ((fun (x : nat) (y : _) => _) = (fun (x : nat) (y : _) => _)).

On 1:11am, Wed, Jan 7, 2015 Jonathan Leivent <jonikelee AT gmail.com> wrote:

Is it possible in Coq for an evar instance to exist in a goal such that
it is "trapped" under binders?  Meaning that after all possible intros
are done, the evar instance still can't be found using Ltac's context[]
construct (as in [match .. with context[?V] => is_evar V ...], but
has_evar senses it)?  Any case of an evar instance "trapped" under
binders would seem to require that its type depends on bound variables.
I can construct such cases within the conclusion of a goal, but they
would become untrapped by doing sufficient intros, at which point
context[] can find them.  I can't seem to construct any cases in
hypotheses (trapped under vars bound in the hypothesis), however.  But,
that's certainly not proof that it isn't possible.

If such trapped evar instances are possible, can anyone come up with an
example?

-- Jonathan