From d6898781f9cd52ac36a4891d7b169ddab7b8af50 Mon Sep 17 00:00:00 2001
From: Amin Timany <amintimany@gmail.com>
Date: Tue, 2 May 2017 19:53:05 +0200
Subject: Correct coqchk reduction

---
 test-suite/coqchk/cumulativity.v | 52 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 52 insertions(+)
 create mode 100644 test-suite/coqchk/cumulativity.v

(limited to 'test-suite/coqchk')

diff --git a/test-suite/coqchk/cumulativity.v b/test-suite/coqchk/cumulativity.v
new file mode 100644
index 000000000..5d245aaa5
--- /dev/null
+++ b/test-suite/coqchk/cumulativity.v
@@ -0,0 +1,52 @@
+Set Universe Polymorphism.
+Set Ind Cumulativity.
+Set Printing Universes.
+
+Inductive List (A: Type) := nil | cons : A -> List A -> List A.
+
+Section ListLift.
+  Universe i j.
+
+  Constraint i < j.
+
+  Definition LiftL {A} : List@{i} A -> List@{j} A := fun x => x.
+
+End ListLift.
+
+Lemma LiftL_Lem A (l : List A) : l = LiftL l.
+Proof. reflexivity. Qed.
+
+Section ListLower.
+  Universe i j.
+
+  Constraint i < j.
+
+  Definition LowerL {A : Type@{i}} : List@{j} A -> List@{i} A := fun x => x.
+
+End ListLower.
+
+Lemma LowerL_Lem@{i j} (A : Type@{j}) (l : List@{i} A) : l = LowerL l.
+Proof. reflexivity. Qed.
+
+Inductive Tp := tp : Type -> Tp.
+
+Section TpLift.
+  Universe i j.
+
+  Constraint i < j.
+
+  Definition LiftTp : Tp@{i} -> Tp@{j} := fun x => x.
+
+End TpLift.
+
+Lemma LiftC_Lem (t : Tp) : LiftTp t = t.
+Proof. reflexivity. Qed.
+
+Section TpLower.
+  Universe i j.
+
+  Constraint i < j.
+
+  Fail Definition LowerTp : Tp@{j} -> Tp@{i} := fun x => x.
+
+End TpLower.
\ No newline at end of file
-- 
cgit v1.2.3