aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/failure/pattern.v
blob: 129c380ed942fc66d532b05c10dc7eb56676b967 (plain)
1
2
3
4
5
6
7
8
9
(* Check that untypable beta-expansion are trapped *)

Variable A : nat -> Type.
Variable n : nat.
Variable P : forall m : nat, m = n -> Prop.

Goal forall p : n = n, P n p.
intro.
pattern n, p in |- *.