From 4a11dc25938f3f009e23f1e7c5fe01b2558928c3 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 27 Nov 2015 20:34:51 +0100
Subject: Univs: entirely disallow instantiation of polymorphic constants with
 Prop levels.

As they are typed assuming all variables are >= Set now, and this was
breaking an invariant in typing. Only one instance in the standard
library was used in Hurkens, which can be avoided easily. This also
avoids displaying unnecessary >= Set constraints everywhere.
---
 test-suite/bugs/closed/4287.v | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4287.v b/test-suite/bugs/closed/4287.v
index 0623cf5b84..43c9b51295 100644
--- a/test-suite/bugs/closed/4287.v
+++ b/test-suite/bugs/closed/4287.v
@@ -118,8 +118,6 @@ Definition setle (B : Type@{i}) :=
   let foo (A : Type@{j}) := A in foo B.
 
 Fail Check @setlt@{j Prop}.
-Check @setlt@{Prop j}.
-Check @setle@{Prop j}.
-
 Fail Definition foo := @setle@{j Prop}.
-Definition foo := @setle@{Prop j}.
+Check setlt@{Set i}.
+Check setlt@{Set j}.
\ No newline at end of file
-- 
cgit v1.2.3