The Coq mailing list

[Mariusz Giero <giero AT cs.kun.nl>]

Hello,

In the below example  pattern matching doesn't work  when
TAC '([x:A] (P x)) is called, while it does for TAC '([x:A] R).
Why is it so?

------------------------------------------------------------
Variable A:Set; P: A -> Prop; R : Prop.
Tactic Definition TAC arg :=  Match arg With [ ([id : ?1] ?2) ] -> Idtac.

Lemma test: True.

TAC '([x:A] (P x)).

TAC '([x:A] R).
----------------------------------------------------------------

Thanks,

Mariusz Giero