aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/failure/pattern.v
blob: 216eb254c1882b38aa7502aea3d9529e612227e9 (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.
Fail pattern n, p.