blob: d9ac09d8d358270e6d9d9b574489c38ad62a49c8 (
plain)
1
2
3
4
5
6
|
(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
Set Universe Polymorphism.
Set Printing Universes.
Inductive Empty : Set := .
(* Toplevel input, characters 15-41:
Error: Universe inconsistency. Cannot enforce Prop <= Set). *)
|
