17 files changed, 226 insertions, 12 deletions

diff --git a/test-suite/modules/Demo.v b/test-suite/modules/Demo.v
index 1f27fe1b..820fda17 100644
--- a/test-suite/modules/Demo.v
+++ b/test-suite/modules/Demo.v
@@ -52,4 +52,4 @@ Print N'''.x.
 
 Import N'''.
 
-Print t.
\ No newline at end of file
+Print t.
diff --git a/test-suite/modules/Nat.v b/test-suite/modules/Nat.v
index 57878a5f..d2116d21 100644
--- a/test-suite/modules/Nat.v
+++ b/test-suite/modules/Nat.v
@@ -16,4 +16,4 @@ Qed.
 
 Lemma le_antis : forall n m : nat, le n m -> le m n -> n = m.
    eauto with arith.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v
index 6198f29a..8ba8525c 100644
--- a/test-suite/modules/PO.v
+++ b/test-suite/modules/PO.v
@@ -54,4 +54,4 @@ Module NN := Pair Nat Nat.
 
 Lemma zz_min : forall p : NN.T, NN.le (0, 0) p.
   info auto with arith.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/test-suite/modules/SeveralWith.v b/test-suite/modules/SeveralWith.v
new file mode 100644
index 00000000..bbf72a76
--- /dev/null
+++ b/test-suite/modules/SeveralWith.v
@@ -0,0 +1,12 @@
+Module Type S.
+Parameter A : Type.
+End S.
+
+Module Type ES.
+Parameter A : Type.
+Parameter eq : A -> A -> Type.
+End ES.
+
+Module Make
+  (AX : S)
+  (X : ES with Definition A := AX.A with Definition eq := @eq AX.A).
diff --git a/test-suite/modules/Tescik.v b/test-suite/modules/Tescik.v
index 1d1b1e0a..ea495539 100644
--- a/test-suite/modules/Tescik.v
+++ b/test-suite/modules/Tescik.v
@@ -27,4 +27,4 @@ Module List (X: ELEM).
 
 End List.
 
-Module N := List Nat.
\ No newline at end of file
+Module N := List Nat.
diff --git a/test-suite/modules/WithDefUBinders.v b/test-suite/modules/WithDefUBinders.v
new file mode 100644
index 00000000..e6834551
--- /dev/null
+++ b/test-suite/modules/WithDefUBinders.v
@@ -0,0 +1,15 @@
+
+Set Universe Polymorphism.
+Module Type T.
+  Axiom foo@{u v|u < v} : Type@{v}.
+End T.
+
+Module M : T with Definition foo@{u v} := Type@{u} : Type@{v}.
+  Definition foo@{u v} := Type@{u} : Type@{v}.
+End M.
+
+Fail Module M' : T with Definition foo := Type.
+
+(* Without the binder expression we have to do trickery to get the
+   universes in the right order. *)
+Module M' : T with Definition foo := let t := Type in t.
diff --git a/test-suite/modules/cumpoly.v b/test-suite/modules/cumpoly.v
new file mode 100644
index 00000000..654b86cb
--- /dev/null
+++ b/test-suite/modules/cumpoly.v
@@ -0,0 +1,19 @@
+Set Universe Polymorphism.
+
+(** Check that variance subtyping is respected. The signature T is asking for
+    invariance, while M provide an irrelevant implementation, which is deemed
+    legit.
+
+    There is currently no way to go the other way around, so it's not possible
+    to generate a counter-example that should fail with the wrong subtyping.
+*)
+
+Module Type T.
+Parameter t@{i|Set <= i} : Type@{i}.
+Cumulative Inductive I@{i|Set <= i} : Type@{i} := C : t@{i} -> I.
+End T.
+
+Module M : T.
+Definition t@{i|Set <= i} : Type@{i} := nat.
+Cumulative Inductive I@{i|Set <= i} : Type@{i} := C : t@{i} -> I.
+End M.
diff --git a/test-suite/modules/grammar.v b/test-suite/modules/grammar.v
index 9657c685..11ad205e 100644
--- a/test-suite/modules/grammar.v
+++ b/test-suite/modules/grammar.v
@@ -12,4 +12,4 @@ Check (f 0 0).
 Check (f 0 0).
 Import M.
 Check (f 0 0).
-Check (N.f 0 0).
\ No newline at end of file
+Check (N.f 0 0).
diff --git a/test-suite/modules/injection_discriminate_inversion.v b/test-suite/modules/injection_discriminate_inversion.v
index d4ac7b3a..8b5969dd 100644
--- a/test-suite/modules/injection_discriminate_inversion.v
+++ b/test-suite/modules/injection_discriminate_inversion.v
@@ -31,4 +31,4 @@ Goal forall x,  M.C x = M1.C 0 -> x = 0.
      par des modules differents
      *)
   inversion H. reflexivity.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/test-suite/modules/modeq.v b/test-suite/modules/modeq.v
index 1238ee9d..c8129eec 100644
--- a/test-suite/modules/modeq.v
+++ b/test-suite/modules/modeq.v
@@ -19,4 +19,4 @@ Module Z.
   Module N := M.
 End Z.
 
-Module A : SIG := Z.
\ No newline at end of file
+Module A : SIG := Z.
diff --git a/test-suite/modules/objects2.v b/test-suite/modules/objects2.v
index 220e2b36..0a6b1f06 100644
--- a/test-suite/modules/objects2.v
+++ b/test-suite/modules/objects2.v
@@ -2,7 +2,7 @@
    the logical objects in the environment
 *)
 
-(* Bug #1118 (simplified version), submitted by Evelyne Contejean
+(* BZ#1118 (simplified version), submitted by Evelyne Contejean
   (used to failed in pre-V8.1 trunk because of a call to lookup_mind
    for structure objects)
 *)
diff --git a/test-suite/modules/pliczek.v b/test-suite/modules/pliczek.v
index f806a7c4..51f5f400 100644
--- a/test-suite/modules/pliczek.v
+++ b/test-suite/modules/pliczek.v
@@ -1,3 +1,3 @@
 Require Export plik.
 
-Definition tutu (X : Set) := toto X.
\ No newline at end of file
+Definition tutu (X : Set) := toto X.
diff --git a/test-suite/modules/plik.v b/test-suite/modules/plik.v
index 50bfd960..c2f0fe3c 100644
--- a/test-suite/modules/plik.v
+++ b/test-suite/modules/plik.v
@@ -1,3 +1,3 @@
 Definition toto (x : Set) := x.
 
-(* <Warning> : Grammar is replaced by Notation *)
\ No newline at end of file
+(* <Warning> : Grammar is replaced by Notation *)
diff --git a/test-suite/modules/polymorphism.v b/test-suite/modules/polymorphism.v
new file mode 100644
index 00000000..63eaa382
--- /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 00000000..7e3327ee
--- /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.
diff --git a/test-suite/modules/pseudo_circular_with.v b/test-suite/modules/pseudo_circular_with.v
index 9e46d17e..6bf067fd 100644
--- a/test-suite/modules/pseudo_circular_with.v
+++ b/test-suite/modules/pseudo_circular_with.v
@@ -3,4 +3,4 @@ Module Type T. Declare Module M:S. End T.
 Module N:S. End N.
 
 Module NN:T. Module M:=N. End NN.
-Module Type U := T with Module M:=NN.
\ No newline at end of file
+Module Type U := T with Module M:=NN.
diff --git a/test-suite/modules/sig.v b/test-suite/modules/sig.v
index da5d25fa..fc936a51 100644
--- a/test-suite/modules/sig.v
+++ b/test-suite/modules/sig.v
@@ -26,4 +26,4 @@ Module Type SIG.
   Parameter x : T.
 End SIG.
 
-Module J : SIG := M.N.
\ No newline at end of file
+Module J : SIG := M.N.