The Coq mailing list

[Aaron Bohannon <bohannon AT cis.upenn.edu>]

Alternatively, instead of using a nested match, you can use
"constr_eq", which compares the ASTs of the terms.  So you can do
something like this:

match goal with
| v : T ?n |- context name [?v1] =>  constr_eq v v1; idtac v
end.

 - Aaron

On Wed, Feb 23, 2011 at 11:39 AM, Adam Chlipala 
<adam AT chlipala.net>
 wrote:
> 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.
>