Fix bugs and add an option for cumulativity

1 files changed, 32 insertions, 20 deletions

diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 3e90825ab..f57cbcc2b 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -316,26 +316,6 @@ Module Hurkens'.
 
 Polymorphic Record box (X : Type) (T := Type) : Type := wrap { unwrap : T }.
 
-Section test_letin_subtyping.
-  Universe i j k i' j' k'.
-  Constraint j < j'.
-
-  Context (W : Type) (X : box@{i j k} W).
-  Definition Y := X : box@{i' j' k'} W.
-
-  Universe i1 j1 k1 i2 j2 k2.
-  Constraint i1 < i2, k2 < k1.
-  Definition Z : box@{i1 j1 k1} W := {| unwrap := W |}.
-  Definition Z' : box@{i2 j2 k2} W := {| unwrap := W |}.
-  Lemma ZZ' : @eq (box@{i2 j2 k2} W) Z Z'.
-  Proof.
-    Set Printing All. Set Printing Universes.
-    cbv.
-    reflexivity.
-  Qed.
-
-End test_letin_subtyping.
-
 Definition unwrap' := fun (X : Type) (b : box X) => let (unw) := b in unw.
 
 Fail Definition bad : False := TypeNeqSmallType.paradox (unwrap' Type (wrap _
@@ -372,3 +352,35 @@ Module Anonymous.
   Check collapsethemiddle@{_ _}.
 
 End Anonymous.
+
+Module F.
+  Context {A B : Type}.
+  Definition foo : Type := B.
+End F.
+
+Set Universe Polymorphism.
+
+Record box (X : Type) (T := Type) : Type := wrap { unwrap : T }.
+
+Section test_letin_subtyping.
+  Universe i j k i' j' k'.
+  Constraint j < j'.
+
+  Context (W : Type) (X : box@{i j k} W).
+  Definition Y := X : box@{i' j' k'} W.
+
+  Universe i1 j1 k1 i2 j2 k2.
+  Constraint i1 < i2.
+  Constraint k2 < k1.
+  Context (V : Type).
+
+  Definition Z : box@{i1 j1 k1} V := {| unwrap := V |}.
+  Definition Z' : box@{i2 j2 k2} V := {| unwrap := V |}.
+  Lemma ZZ' : @eq (box@{i2 j2 k2} V) Z Z'.
+  Proof.
+    Set Printing All. Set Printing Universes.
+    cbv.
+    reflexivity.
+  Qed.
+
+End test_letin_subtyping.