The Coq mailing list

[Michael Shulman <mshulman AT ucsd.edu>]

I am confused by some behavior of metavariable binding in Ltac.  This
works as I would expect:

Lemma test {A B} (f : forall x:A, B x) (a : A) : B a.
Proof.
  match goal with
    | |- B ?y => apply f with (x := y)
  end.
Qed.

But this doesn't (just replace both y's with x):

Lemma test {A B} (f : forall x:A, B x) (a : A) : B a.
Proof.
  match goal with
    | |- B ?x => apply f with (x := x)
  end.
Qed.

It seems to me that there should be no difference; isn't the latter
just an alpha-conversion of the first?  Surely the 'x' on the
left-hand side of the := exists in a different scope (the dependent
arguments of f) and shouldn't be affected by the name of a local
metavariable?  Or is there some other subtlety I'm missing?

Thanks!
Mike