Imported Upstream version 8.5~beta3+dfsg

1 files changed, 9 insertions, 4 deletions

diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index db155e6c..58f3bcdf 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -311,15 +311,19 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
 		try 
 		  (* The environment with the expected universes plus equality 
 		     of the body instances with the expected instance *)
-		  let env = Environ.add_constraints cstrs env in
-		    (* Check that the given definition does not add any constraint over
-		       the expected ones, so that it can be used in place of the original. *)
+		  let ctxi = Univ.Instance.append inst1 inst2 in
+		  let ctx = Univ.UContext.make (ctxi, cstrs) in
+		  let env = Environ.push_context ctx env in
+		  (* Check that the given definition does not add any constraint over
+		     the expected ones, so that it can be used in place of 
+                     the original. *)
 		    if Univ.check_constraints ctx1 (Environ.universes env) then
 		      cstrs, env, inst2
 		    else error (IncompatibleConstraints ctx1)
 		with Univ.UniverseInconsistency incon -> 
 		  error (IncompatibleUniverses incon)
-	else cst, env, Univ.Instance.empty
+	else
+	  cst, env, Univ.Instance.empty
       in
       (* Now check types *)
       let typ1 = Typeops.type_of_constant_type env' cb1.const_type in
@@ -456,6 +460,7 @@ and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv =
 
 let check_subtypes env sup super =
   let env = add_module_type sup.mod_mp sup env in
+  let env = Environ.push_context_set ~strict:true super.mod_constraints env in
   check_modtypes Univ.Constraint.empty env
     (strengthen sup sup.mod_mp) super empty_subst
     (map_mp super.mod_mp sup.mod_mp sup.mod_delta) false