Imported Upstream version 8.5~beta1+dfsg

1 files changed, 19 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/HoTT_coq_035.v b/test-suite/bugs/closed/HoTT_coq_035.v
new file mode 100644
index 00000000..4ad2fc02
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_035.v
@@ -0,0 +1,19 @@
+Fail Check Prop : Prop. (* Prop:Prop
+     : Prop *)
+Fail Check Set : Prop. (* Set:Prop
+     : Prop *)
+Fail Check ((bool -> Prop) : Prop). (* bool -> Prop:Prop
+     : Prop *)
+Axiom proof_irrelevance : forall (P : Prop) (p1 p2 : P), p1 = p2.
+Check ((True : Prop) : Set). (* (True:Prop):Set
+     : Set *)
+Goal (forall (v : Type) (f1 f0 : v -> Prop),
+        @eq (v -> Prop) f0 f1).
+intros.
+Fail apply proof_irrelevance.
+admit.
+Defined. (* Unnamed_thm is defined *)
+Set Printing Universes.
+Check ((True : Prop) : Set). (* Toplevel input, characters 0-28:
+Error: Universe inconsistency (cannot enforce Prop <= Set because Set
+< Prop). *)