universes2.v « failure « test-suite - coq - the Coq proof assistant

about summary refs log tree commit diff homepage

path: root/test-suite/failure/universes2.v

blob: e74de70fc8bf14aa046fb7f289b5643a73d97b9a (plain)

(* Example submitted by Randy Pollack *)

Parameter K : forall T : Type, T -> T.
Check (K (forall T : Type, T -> T) K).