test-suite/failure/pattern.v


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 |- *.