From 15999903f875f4b5dbb3d5240d2ca39acc3cd777 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 26 May 2014 13:58:56 +0200
Subject: - Fix in kernel conversion not folding the universe constraints
 correctly when comparing stacks. - Disallow Type i <= Prop/Set constraints,
 that would otherwise allow constraints that make a universe lower than Prop.
 - Fix stm/lemmas that was pushing constraints to the global context, it is
 done depending on the constant/variable polymorphic status now. - Adapt
 generalized rewriting in Type code to these fixes.

---
 test-suite/success/polymorphism.v | 22 +++++++++++++++++++++-
 1 file changed, 21 insertions(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 1ef2713e44..99284eb547 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -211,7 +211,27 @@ Polymorphic Definition id {A : Type} (a : A) : A := a.
 Definition typeid := (@id Type).
 
 
+Fail Check (Prop : Set).
+Fail Check (Set : Set).
+Check (Set : Type).
+Check (Prop : Type).
+Definition setType := $(let t := type of Set in exact t)$.
 
+Definition foo (A : Prop) := A.
+
+Fail Check foo Set.
+Check fun A => foo A.
+Fail Check fun A : Type => foo A.
+Check fun A : Prop => foo A.
+Fail Definition bar := fun A : Set => foo A.
+
+Fail Check (let A := Type in foo (id A)).
+
+Definition fooS (A : Set) := A.
+
+Check (let A := nat in fooS (id A)).
+Fail Check (let A := Set in fooS (id A)).
+Fail Check (let A := Prop in fooS (id A)).
 
 (* Some tests of sort-polymorphisme *)
 Section S.
@@ -227,7 +247,7 @@ End S.
 (*
 Check f nat nat : Set.
 *)
-Definition foo:= I nat nat : Set.
+Definition foo' := I nat nat.
 Print Universes. Print foo. Set Printing Universes. Print foo.
 
 (* Polymorphic axioms: *)
-- 
cgit v1.2.3