The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Thomas Braibant wrote:
> I have a problem that can be reduced to the snippet below.
>
> Section t.
>    Variable T : nat ->  Type.
>    Variable f : forall n, T n ->  Prop.
>    Goal forall n m (x : T n) (y : T m), f n (x).
>      intros.
>      match goal with
>        | v : T ?n |- context name [?v] =>  idtac v (* prints [f n x],
> while I would like [x]*)
>      end.
> End.
>    

Hypothesis variable names are not treated as bound elsewhere in the same 
Ltac pattern.  You can achieve what you want by nesting one [match] 
inside another, making each responsible for just one part of the pattern 
above.