blob: f2b2e57b9cd5ade3fc2a5fa63e559d758165692a (
plain)
1
2
3
4
5
|
(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *)
Set Universe Polymorphism.
Set Printing Universes.
Inductive Empty : Set := .
(* Error: Universe inconsistency. Cannot enforce Prop <= Set). *)
|