Newest version of (polyproj) doesn't know that Prop <= Set

HoTT / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

http://coq.inria.fr/

GNU Lesser General Public License v2.1

27 stars 5 forks source link

Newest version of (polyproj) doesn't know that Prop <= Set #97

Closed JasonGross closed 10 years ago

JasonGross commented 10 years ago

Set Printing Universes.
Inductive Empty : Set := .
(* Error: Universe inconsistency. Cannot enforce Prop <= Set). *)

JasonGross commented 10 years ago

Note: This only occurs with the -indices-matter flag.

JasonGross commented 10 years ago

Closed in newest version of trunk-polyproj.