From fbe0b2645eab84012aec50e76d94e15a3fefe664 Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Fri, 7 Jul 2017 14:09:31 +0200
Subject: Issue error on monomorphic cumulative inductives

---
 test-suite/success/cumulativity.v | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v
index ebf817cfc5..604da2108e 100644
--- a/test-suite/success/cumulativity.v
+++ b/test-suite/success/cumulativity.v
@@ -1,3 +1,9 @@
+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 Printing Universes.
-- 
cgit v1.2.3


From 7f78827b3f8583a7c0e79a78266bc01a411ed818 Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Fri, 7 Jul 2017 14:26:05 +0200
Subject: Add test for NonCumulative inductives

---
 test-suite/success/cumulativity.v | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v
index 604da2108e..351d472a11 100644
--- a/test-suite/success/cumulativity.v
+++ b/test-suite/success/cumulativity.v
@@ -68,4 +68,16 @@ 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.
-- 
cgit v1.2.3


From 9f0abdf5d9f3dde45758c8b9fe0fbe86eef01ee2 Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Fri, 7 Jul 2017 15:41:41 +0200
Subject: Add Jason's example of fun-ext with cumulativity

---
 test-suite/success/cumulativity.v | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v
index 351d472a11..8854435cf3 100644
--- a/test-suite/success/cumulativity.v
+++ b/test-suite/success/cumulativity.v
@@ -81,3 +81,20 @@ Section NCListLift.
   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.
-- 
cgit v1.2.3


From 3b7e7f7738737475cb0f09130b0487c85906dd2b Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Fri, 28 Jul 2017 13:29:36 +0200
Subject: Change the option for cumulativity

---
 test-suite/coqchk/cumulativity.v  | 2 +-
 test-suite/success/cumulativity.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'test-suite')

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 8854435cf3..0ee85712e2 100644
--- a/test-suite/success/cumulativity.v
+++ b/test-suite/success/cumulativity.v
@@ -5,7 +5,7 @@ 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.
-- 
cgit v1.2.3