aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/HoTT_coq_097.v
blob: 38e8007b6c38efa70e011db923fa04adad914789 (plain)
1
2
3
4
5
(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
Set Universe Polymorphism.
Set Printing Universes.
Inductive Empty : Set := .
(* Error: Universe inconsistency. Cannot enforce Prop <= Set). *)