Merge PR #870: Prepare De Bruijn universe abstractions, Episode I: Kernel

3 files changed, 174 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/5641.v b/test-suite/bugs/closed/5641.v
new file mode 100644
index 000000000..9f3246f33
--- /dev/null
+++ b/test-suite/bugs/closed/5641.v
@@ -0,0 +1,6 @@
+Set Universe Polymorphism.
+
+Definition foo@{i j} (A : Type@{i}) : Type@{j}.
+Proof.
+abstract (exact ltac:(abstract (exact A))).
+Defined.
diff --git a/test-suite/modules/polymorphism.v b/test-suite/modules/polymorphism.v
new file mode 100644
index 000000000..63eaa382d
--- /dev/null
+++ b/test-suite/modules/polymorphism.v
@@ -0,0 +1,81 @@
+Set Universe Polymorphism.
+
+(** Tests for module subtyping of polymorphic terms *)
+
+Module Type S.
+
+Section Foo.
+
+Universes i j.
+Constraint i <= j.
+
+Parameter foo : Type@{i} -> Type@{j}.
+
+End Foo.
+
+End S.
+
+(** Same constraints *)
+
+Module OK_1.
+
+Definition foo@{i j} (A : Type@{i}) : Type@{j} := A.
+
+End OK_1.
+
+Module OK_1_Test : S := OK_1.
+
+(** More general constraints *)
+
+Module OK_2.
+
+Inductive X@{i} : Type@{i} :=.
+Definition foo@{i j} (A : Type@{i}) : Type@{j} := X@{j}.
+
+End OK_2.
+
+Module OK_2_Test : S := OK_2.
+
+(** Wrong instance length *)
+
+Module KO_1.
+
+Definition foo@{i} (A : Type@{i}) : Type@{i} := A.
+
+End KO_1.
+
+Fail Module KO_Test_1 : S := KO_1.
+
+(** Less general constraints *)
+
+Module KO_2.
+
+Section Foo.
+
+Universe i j.
+Constraint i < j.
+
+Definition foo (A : Type@{i}) : Type@{j} := A.
+
+End Foo.
+
+End KO_2.
+
+Fail Module KO_Test_2 : S := KO_2.
+
+(** Less general constraints *)
+
+Module KO_3.
+
+Section Foo.
+
+Universe i j.
+Constraint i = j.
+
+Definition foo (A : Type@{i}) : Type@{j} := A.
+
+End Foo.
+
+End KO_3.
+
+Fail Module KO_Test_3 : S := KO_3.
diff --git a/test-suite/modules/polymorphism2.v b/test-suite/modules/polymorphism2.v
new file mode 100644
index 000000000..7e3327eee
--- /dev/null
+++ b/test-suite/modules/polymorphism2.v
@@ -0,0 +1,87 @@
+Set Universe Polymorphism.
+
+(** Tests for module subtyping of polymorphic terms *)
+
+Module Type S.
+
+Section Foo.
+
+Universes i j.
+Constraint i <= j.
+
+Inductive foo : Type@{i} -> Type@{j} :=.
+
+End Foo.
+
+End S.
+
+(** Same constraints *)
+
+Module OK_1.
+
+Section Foo.
+
+Universes i j.
+Constraint i <= j.
+
+Inductive foo : Type@{i} -> Type@{j} :=.
+
+End Foo.
+
+End OK_1.
+
+Module OK_1_Test : S := OK_1.
+
+(** More general constraints *)
+
+Module OK_2.
+
+Inductive foo@{i j} : Type@{i} -> Type@{j} :=.
+
+End OK_2.
+
+Module OK_2_Test : S := OK_2.
+
+(** Wrong instance length *)
+
+Module KO_1.
+
+Inductive foo@{i} : Type@{i} -> Type@{i} :=.
+
+End KO_1.
+
+Fail Module KO_Test_1 : S := KO_1.
+
+(** Less general constraints *)
+
+Module KO_2.
+
+Section Foo.
+
+Universe i j.
+Constraint i < j.
+
+Inductive foo : Type@{i} -> Type@{j} :=.
+
+End Foo.
+
+End KO_2.
+
+Fail Module KO_Test_2 : S := KO_2.
+
+(** Less general constraints *)
+
+Module KO_3.
+
+Section Foo.
+
+Universe i j.
+Constraint i = j.
+
+Inductive foo : Type@{i} -> Type@{j} :=.
+
+End Foo.
+
+End KO_3.
+
+Fail Module KO_Test_3 : S := KO_3.