The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

Hi,

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.

I do not see any mean to use the variable v (as an hypothesis) to
constrain the match in the goal, but I am maybe missing something
obvious. Any help welcome.

With best regards,
thomas