The Coq mailing list

[Bruno Woltzenlogel Paleo <bruno.wp AT gmail.com>]

Hi, 

Could someone tell me why tac1 defined below succeeds in matching while tac2 
throws a "no matching clauses" error:

Parameter I: Type.
Parameter b: I.
Parameter f: (I -> Prop) -> (I -> Prop).

Ltac tac1 H := let P := match type of H with
   ((f ?p) _) => p
end in cut (P b).

Ltac tac2 H := let F := match type of H with
  ((f ?p) ?a) => (p a)
end in cut F.

Theorem t1: forall x q, (f q x) -> False.
Proof.
intros x q H.
tac1 H.
Admitted.

Theorem t2: forall x q, (f q x) -> False.
Proof.
intros x q H.
tac2 H. (* No matching clause error here*)
Admitted.




Best regards,

Bruno