Merge PR #864: Some cleanups after cumulativity for inductive types

2 files changed, 38 insertions, 3 deletions

diff --git a/test-suite/coqchk/cumulativity.v b/test-suite/coqchk/cumulativity.v
index a978f6b901..7906a5b15e 100644
--- a/test-suite/coqchk/cumulativity.v
+++ b/test-suite/coqchk/cumulativity.v
@@ -1,5 +1,5 @@
 Set Universe Polymorphism.
-Set Inductive Cumulativity.
+Set Polymorphic Inductive Cumulativity.
 Set Printing Universes.
 
 Inductive List (A: Type) := nil | cons : A -> List A -> List A.
diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v
index ebf817cfc5..0ee85712e2 100644
--- a/test-suite/success/cumulativity.v
+++ b/test-suite/success/cumulativity.v
@@ -1,5 +1,11 @@
+Polymorphic Cumulative Inductive T1 := t1 : T1.
+Fail Monomorphic Cumulative Inductive T2 := t2 : T2.
+
+Polymorphic Cumulative Record R1 := { r1 : T1 }.
+Fail Monomorphic Cumulative Inductive R2 := {r2 : T1}.
+
 Set Universe Polymorphism.
-Set Inductive Cumulativity.
+Set Polymorphic Inductive Cumulativity.
 Set Printing Universes.
 
 Inductive List (A: Type) := nil | cons : A -> List A -> List A.
@@ -62,4 +68,33 @@ End subtyping_test.
 
 Record A : Type := { a :> Type; }.
 
-Record B (X : A) : Type := { b : X; }.
\ No newline at end of file
+Record B (X : A) : Type := { b : X; }.
+
+NonCumulative Inductive NCList (A: Type)
+  := ncnil | nccons : A -> NCList A -> NCList A.
+
+Section NCListLift.
+  Universe i j.
+
+  Constraint i < j.
+
+  Fail Definition LiftNCL {A} : NCList@{i} A -> NCList@{j} A := fun x => x.
+
+End NCListLift.
+
+Inductive eq@{i} {A : Type@{i}} (x : A) : A -> Type@{i} := eq_refl : eq x x.
+
+Definition funext_type@{a b e} (A : Type@{a}) (B : A -> Type@{b})
+  := forall f g : (forall a, B a),
+    (forall x, eq@{e} (f x) (g x))
+    -> eq@{e} f g.
+
+Section down.
+  Universes a b e e'.
+  Constraint e' < e.
+  Lemma funext_down {A B}
+    : @funext_type@{a b e} A B -> @funext_type@{a b e'} A B.
+  Proof.
+    intros H f g Hfg. exact (H f g Hfg).
+  Defined.
+End down.