3 files changed, 89 insertions, 0 deletions
diff --git a/test-suite/modules/pseudo_circular_with.v b/test-suite/modules/pseudo_circular_with.v
new file mode 100644
index 00000000..9e46d17e
--- /dev/null
+++ b/test-suite/modules/pseudo_circular_with.v
@@ -0,0 +1,6 @@
+Module Type S. End S.
+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
diff --git a/test-suite/modules/resolver.v b/test-suite/modules/resolver.v
new file mode 100644
index 00000000..dcfcc98d
--- /dev/null
+++ b/test-suite/modules/resolver.v
@@ -0,0 +1,37 @@
+Module Type TA.
+Parameter t : Set.
+End TA.
+
+Module Type TB.
+Declare Module A: TA.
+End TB.
+
+Module Type TC.
+Declare Module B : TB.
+End TC.
+
+Module Type TD.
+
+Declare Module B: TB .
+Declare Module C: TC
+   with Module B := B  .
+End TD.
+
+Module Type TE.
+Declare Module D : TD.
+End TE.
+
+Module Type TF.
+Declare Module E:  TE.
+End TF.
+
+Module G (D: TD).
+Module B' := D.C.B.
+End G.
+
+Module H  (F: TF).
+Module I := G(F.E.D).
+End H.
+
+Declare Module F:  TF.
+Module K := H(F).
diff --git a/test-suite/modules/subtyping.v b/test-suite/modules/subtyping.v
new file mode 100644
index 00000000..2df8e84e
--- /dev/null
+++ b/test-suite/modules/subtyping.v
@@ -0,0 +1,46 @@
+(* Non regression for bug #1302 *)
+
+(* With universe polymorphism for inductive types, subtyping of
+   inductive types needs a special treatment: the standard conversion
+   algorithm does not work as it only knows to deal with constraints of
+   the form alpha = beta or max(alphas, alphas+1) <= beta, while
+   subtyping of inductive types in Type generates constraints of the form
+   max(alphas, alphas+1) <= max(betas, betas+1).
+
+   These constraints are anyway valid by monotonicity of subtyping but we
+   have to detect it early enough to avoid breaking the standard
+   algorithm for constraints on algebraic universes. *)
+
+Module Type T.
+
+ Parameter A : Type (* Top.1 *) .
+
+ Inductive L : Type (* max(Top.1,1) *) := 
+ | L0
+ | L1 :  (A -> Prop) -> L.
+
+End T.
+
+Axiom Tp : Type (* Top.5 *) .
+
+Module TT : T. 
+
+ Definition A : Type (* Top.6 *) := Tp. (* generates Top.5 <= Top.6 *)
+
+ Inductive L : Type (* max(Top.6,1) *) := 
+ | L0
+ | L1 :  (A -> Prop) -> L.
+
+End TT. (* Generates Top.6 <= Top.1 (+ auxiliary constraints for L_rect) *)
+
+(* Note: Top.6 <= Top.1 is generated by subtyping on A; 
+   subtyping of L follows and has not to be checked *)
+
+
+
+(* The same bug as #1302 but for Definition *)
+(* Check that inferred algebraic universes in interfaces are considered *)
+
+Module Type U. Definition A := Type -> Type. End U.
+Module M:U. Definition A := Type -> Type. End M.
+