From 7a4e7dfbaa8dc3fa92931c4bfa39d268940e08f8 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 16 Apr 2020 23:06:35 +0200
Subject: Remove mod_constraints field of module body

---
 kernel/declarations.ml |  2 --
 kernel/declareops.ml   |  3 ---
 kernel/environ.ml      |  3 +++
 kernel/environ.mli     |  2 ++
 kernel/mod_typing.ml   | 71 ++++++++++++++++++++++++--------------------------
 kernel/mod_typing.mli  |  8 +++---
 kernel/modops.ml       |  3 +--
 kernel/safe_typing.ml  | 66 +++++++++++++++++++++++-----------------------
 kernel/safe_typing.mli |  1 +
 kernel/subtyping.ml    |  2 --
 10 files changed, 78 insertions(+), 83 deletions(-)

(limited to 'kernel')

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 244cd2865d..d5f219b55f 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -293,8 +293,6 @@ and 'a generic_module_body =
     mod_expr : 'a; (** implementation *)
     mod_type : module_signature; (** expanded type *)
     mod_type_alg : module_expression option; (** algebraic type *)
-    mod_constraints : Univ.ContextSet.t; (**
-      set of all universes constraints in the module  *)
     mod_delta : Mod_subst.delta_resolver; (**
       quotiented set of equivalent constants and inductive names *)
     mod_retroknowledge : 'a module_retroknowledge }
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 20dc21900c..0cd5dea53d 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -390,7 +390,6 @@ and hcons_generic_module_body :
   let expr' = hcons_impl mb.mod_expr in
   let type' = hcons_module_signature mb.mod_type in
   let type_alg' = mb.mod_type_alg in
-  let constraints' = Univ.hcons_universe_context_set mb.mod_constraints in
   let delta' = mb.mod_delta in
   let retroknowledge' = mb.mod_retroknowledge in
 
@@ -399,7 +398,6 @@ and hcons_generic_module_body :
     mb.mod_expr == expr' &&
     mb.mod_type == type' &&
     mb.mod_type_alg == type_alg' &&
-    mb.mod_constraints == constraints' &&
     mb.mod_delta == delta' &&
     mb.mod_retroknowledge == retroknowledge'
   then mb
@@ -408,7 +406,6 @@ and hcons_generic_module_body :
     mod_expr = expr';
     mod_type = type';
     mod_type_alg = type_alg';
-    mod_constraints = constraints';
     mod_delta = delta';
     mod_retroknowledge = retroknowledge';
   }
diff --git a/kernel/environ.ml b/kernel/environ.ml
index de8692ff21..93f1b051ab 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -279,6 +279,9 @@ let indices_matter env = env.env_typing_flags.indices_matter
 let universes env = env.env_stratification.env_universes
 let universes_lbound env = env.env_stratification.env_universes_lbound
 
+let set_universes g env =
+  {env with env_stratification = {env.env_stratification with env_universes=g}}
+
 let set_universes_lbound env lbound =
   let env_stratification = { env.env_stratification with env_universes_lbound = lbound } in
   { env with env_stratification }
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 25ecdfd852..9e35e2f608 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -102,6 +102,8 @@ val rel_context   : env -> Constr.rel_context
 val named_context : env -> Constr.named_context
 val named_context_val : env -> named_context_val
 
+val set_universes : UGraph.t -> env -> env
+
 val opaque_tables : env -> Opaqueproof.opaquetab
 val set_opaque_tables : env -> Opaqueproof.opaquetab -> env
 
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 76e2a584bd..44b010204b 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -23,7 +23,7 @@ open Modops
 open Mod_subst
 
 type 'alg translation =
-  module_signature * 'alg * delta_resolver * Univ.ContextSet.t
+  module_signature * 'alg * delta_resolver * Univ.Constraint.t
 
 let rec mp_from_mexpr = function
   | MEident mp -> mp
@@ -54,8 +54,6 @@ let rec rebuild_mp mp l =
   | []-> mp
   | i::r -> rebuild_mp (MPdot(mp,Label.of_id i)) r
 
-let (+++) = Univ.ContextSet.union
-
 let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
   let lab,idl = match idl with
     | [] -> assert false
@@ -173,10 +171,10 @@ let rec check_with_mod env struc (idl,mp1) mp equiv =
         | Abstract ->
           let mtb_old = module_type_of_module old in
           let chk_cst = Subtyping.check_subtypes env' mtb_mp1 mtb_old in
-          Univ.ContextSet.add_constraints chk_cst old.mod_constraints
+          chk_cst
         | Algebraic (NoFunctor (MEident(mp'))) ->
           check_modpath_equiv env' mp1 mp';
-          old.mod_constraints
+          Univ.Constraint.empty
         | _ -> error_generative_module_expected lab
       in
       let mp' = MPdot (mp,lab) in
@@ -185,7 +183,7 @@ let rec check_with_mod env struc (idl,mp1) mp equiv =
         { new_mb with
           mod_mp = mp';
           mod_expr = Algebraic (NoFunctor (MEident mp1));
-          mod_constraints = cst }
+        }
       in
       let new_equiv = add_delta_resolver equiv new_mb.mod_delta in
       (* we propagate the new equality in the rest of the signature
@@ -219,7 +217,7 @@ let rec check_with_mod env struc (idl,mp1) mp equiv =
       | Algebraic (NoFunctor (MEident mp0)) ->
         let mpnew = rebuild_mp mp0 idl in
         check_modpath_equiv env' mpnew mp;
-        before@(lab,spec)::after, equiv, Univ.ContextSet.empty
+        before@(lab,spec)::after, equiv, Univ.Constraint.empty
       | _ -> error_generative_module_expected lab
       end
   with
@@ -231,11 +229,11 @@ let check_with env mp (sign,alg,reso,cst) = function
     let struc = destr_nofunctor sign in
     let struc', c', cst' = check_with_def env struc (idl, (c, ctx)) mp reso in
     let wd' = WithDef (idl, (c', ctx)) in
-    NoFunctor struc', MEwith (alg,wd'), reso, Univ.ContextSet.add_constraints cst' cst
+    NoFunctor struc', MEwith (alg,wd'), reso, Univ.Constraint.union cst' cst
   |WithMod(idl,mp1) as wd ->
     let struc = destr_nofunctor sign in
     let struc',reso',cst' = check_with_mod env struc (idl,mp1) mp reso in
-    NoFunctor struc', MEwith (alg,wd), reso', cst+++cst'
+    NoFunctor struc', MEwith (alg,wd), reso', Univ.Constraint.union cst' cst
 
 let translate_apply env inl (sign,alg,reso,cst1) mp1 mkalg =
   let farg_id, farg_b, fbody_b = destr_functor sign in
@@ -247,7 +245,7 @@ let translate_apply env inl (sign,alg,reso,cst1) mp1 mkalg =
   let body = subst_signature subst fbody_b in
   let alg' = mkalg alg mp1 in
   let reso' = subst_codom_delta_resolver subst reso in
-  body,alg',reso', Univ.ContextSet.add_constraints cst2 cst1
+  body,alg',reso', Univ.Constraint.union cst2 cst1
 
 (** Translation of a module struct entry :
     - We translate to a module when a [module_path] is given,
@@ -266,7 +264,7 @@ let rec translate_mse env mpo inl = function
         let mt = lookup_modtype mp1 env in
         module_body_of_type mt.mod_mp mt
     in
-    mb.mod_type, me, mb.mod_delta, Univ.ContextSet.empty
+    mb.mod_type, me, mb.mod_delta, Univ.Constraint.empty
   |MEapply (fe,mp1) ->
     translate_apply env inl (translate_mse env mpo inl fe) mp1 mk_alg_app
   |MEwith(me, with_decl) ->
@@ -274,17 +272,16 @@ let rec translate_mse env mpo inl = function
     let mp = mp_from_mexpr me in
     check_with env mp (translate_mse env None inl me) with_decl
 
-let mk_mod mp e ty cst reso =
+let mk_mod mp e ty reso =
   { mod_mp = mp;
     mod_expr = e;
     mod_type = ty;
     mod_type_alg = None;
-    mod_constraints = cst;
     mod_delta = reso;
     mod_retroknowledge = ModBodyRK []; }
 
-let mk_modtype mp ty cst reso =
-  let mb = mk_mod mp Abstract ty cst reso in
+let mk_modtype mp ty reso =
+  let mb = mk_mod mp Abstract ty reso in
   { mb with mod_expr = (); mod_retroknowledge = ModTypeRK }
 
 let rec translate_mse_funct env mpo inl mse = function
@@ -293,45 +290,45 @@ let rec translate_mse_funct env mpo inl mse = function
     sign, NoFunctor alg, reso, cst
   |(mbid, ty) :: params ->
     let mp_id = MPbound mbid in
-    let mtb = translate_modtype env mp_id inl ([],ty) in
+    let mtb, cst = translate_modtype env mp_id inl ([],ty) in
     let env' = add_module_type mp_id mtb env in
-    let sign,alg,reso,cst = translate_mse_funct env' mpo inl mse params in
+    let sign,alg,reso,cst' = translate_mse_funct env' mpo inl mse params in
     let alg' = MoreFunctor (mbid,mtb,alg) in
-    MoreFunctor (mbid, mtb, sign), alg',reso, cst +++ mtb.mod_constraints
+    MoreFunctor (mbid, mtb, sign), alg',reso, Univ.Constraint.union cst cst'
 
 and translate_modtype env mp inl (params,mte) =
   let sign,alg,reso,cst = translate_mse_funct env None inl mte params in
-  let mtb = mk_modtype (mp_from_mexpr mte) sign cst reso in
+  let mtb = mk_modtype (mp_from_mexpr mte) sign reso in
   let mtb' = subst_modtype_and_resolver mtb mp in
-  { mtb' with mod_type_alg = Some alg }
+  { mtb' with mod_type_alg = Some alg }, cst
 
 (** [finalize_module] :
     from an already-translated (or interactive) implementation and
     an (optional) signature entry, produces a final [module_body] *)
 
-let finalize_module env mp (sign,alg,reso,cst) restype = match restype with
-  |None ->
+let finalize_module env mp (sign,alg,reso,cst1) restype = match restype with
+  | None ->
     let impl = match alg with Some e -> Algebraic e | None -> FullStruct in
-    mk_mod mp impl sign cst reso
-  |Some (params_mte,inl) ->
-    let res_mtb = translate_modtype env mp inl params_mte in
-    let auto_mtb = mk_modtype mp sign Univ.ContextSet.empty reso in
-    let cst' = Subtyping.check_subtypes env auto_mtb res_mtb in
+    mk_mod mp impl sign reso, cst1
+  | Some (params_mte,inl) ->
+    let res_mtb, cst2 = translate_modtype env mp inl params_mte in
+    let auto_mtb = mk_modtype mp sign reso in
+    let cst3 = Subtyping.check_subtypes env auto_mtb res_mtb in
     let impl = match alg with Some e -> Algebraic e | None -> Struct sign in
     { res_mtb with
       mod_mp = mp;
       mod_expr = impl;
       mod_retroknowledge = ModBodyRK [];
-      (** cst from module body typing,
-          cst' from subtyping,
-          constraints from module type. *)
-      mod_constraints =
-        Univ.ContextSet.add_constraints cst' (cst +++ res_mtb.mod_constraints) }
+    },
+    (** cst from module body typing,
+        cst' from subtyping,
+        constraints from module type. *)
+    Univ.Constraint.(union cst1 (union cst2 cst3))
 
 let translate_module env mp inl = function
   |MType (params,ty) ->
-    let mtb = translate_modtype env mp inl (params,ty) in
-    module_body_of_type mp mtb
+    let mtb, cst = translate_modtype env mp inl (params,ty) in
+    module_body_of_type mp mtb, cst
   |MExpr (params,mse,oty) ->
     let (sg,alg,reso,cst) = translate_mse_funct env (Some mp) inl mse params in
     let restype = Option.map (fun ty -> ((params,ty),inl)) oty in
@@ -364,7 +361,7 @@ let rec translate_mse_inclmod env mp inl = function
   |MEident mp1 ->
     let mb = strengthen_and_subst_mb (lookup_module mp1 env) mp true in
     let sign = clean_bounded_mod_expr mb.mod_type in
-    sign,(),mb.mod_delta,Univ.ContextSet.empty
+    sign,(),mb.mod_delta,Univ.Constraint.empty
   |MEapply (fe,arg) ->
     let ftrans = translate_mse_inclmod env mp inl fe in
     translate_apply env inl ftrans arg (fun _ _ -> ())
@@ -375,6 +372,6 @@ let translate_mse_incl is_mod env mp inl me =
     let () = forbid_incl_signed_functor env me in
     translate_mse_inclmod env mp inl me
   else
-    let mtb = translate_modtype env mp inl ([],me) in
+    let mtb, cst = translate_modtype env mp inl ([],me) in
     let sign = clean_bounded_mod_expr mtb.mod_type in
-    sign,(),mtb.mod_delta,mtb.mod_constraints
+    sign, (), mtb.mod_delta, cst
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index fd5421aefe..94a4b17df3 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -23,13 +23,13 @@ open Names
 *)
 
 val translate_module :
-  env -> ModPath.t -> inline -> module_entry -> module_body
+  env -> ModPath.t -> inline -> module_entry -> module_body * Univ.Constraint.t
 
 (** [translate_modtype] produces a [module_type_body] whose [mod_type_alg]
     cannot be [None] (and of course [mod_expr] is [Abstract]). *)
 
 val translate_modtype :
-  env -> ModPath.t -> inline -> module_type_entry -> module_type_body
+  env -> ModPath.t -> inline -> module_type_entry -> module_type_body * Univ.Constraint.t
 
 (** Low-level function for translating a module struct entry :
     - We translate to a module when a [ModPath.t] is given,
@@ -39,7 +39,7 @@ val translate_modtype :
       the extraction. *)
 
 type 'alg translation =
-  module_signature * 'alg * delta_resolver * Univ.ContextSet.t
+  module_signature * 'alg * delta_resolver * Univ.Constraint.t
 
 val translate_mse :
   env -> ModPath.t option -> inline -> module_struct_entry ->
@@ -51,7 +51,7 @@ val translate_mse :
 val finalize_module :
   env -> ModPath.t -> (module_expression option) translation ->
   (module_type_entry * inline) option ->
-  module_body
+  module_body * Univ.Constraint.t
 
 (** [translate_mse_incl] translate the mse of a module or
     module type given to an Include *)
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 301af328e4..77ef38dfd5 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -225,8 +225,7 @@ and subst_body : 'a. _ -> _ -> (_ -> 'a -> 'a) -> _ -> 'a generic_module_body ->
      && retro==retro' && delta'==mb.mod_delta
   then mb
   else
-    { mb with
-      mod_mp = mp';
+    { mod_mp = mp';
       mod_expr = me';
       mod_type = ty';
       mod_type_alg = aty';
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 58b516dfdd..3b70aba884 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -116,6 +116,7 @@ type module_parameters = (MBId.t * module_type_body) list
 type compiled_library = {
   comp_name : DirPath.t;
   comp_mod : module_body;
+  comp_univs : Univ.ContextSet.t;
   comp_deps : library_info array;
   comp_enga : engagement;
   comp_natsymbs : Nativevalues.symbols
@@ -566,8 +567,7 @@ let constraints_of_sfb sfb =
   match sfb with
   | SFBconst cb -> globalize_constant_universes cb
   | SFBmind mib -> globalize_mind_universes mib
-  | SFBmodtype mtb -> [mtb.mod_constraints]
-  | SFBmodule mb -> [mb.mod_constraints]
+  | SFBmodtype _ | SFBmodule _ -> []
 
 let add_retroknowledge pttc senv =
   { senv with
@@ -986,35 +986,35 @@ let add_mind l mie senv =
 
 let add_modtype l params_mte inl senv =
   let mp = MPdot(senv.modpath, l) in
-  let mtb = Mod_typing.translate_modtype senv.env mp inl params_mte  in
+  let mtb, cst = Mod_typing.translate_modtype senv.env mp inl params_mte  in
+  let senv = push_context_set ~strict:true (Univ.LSet.empty,cst) senv in
   let mtb = Declareops.hcons_module_type mtb in
-  let senv' = add_field (l,SFBmodtype mtb) MT senv in
-  mp, senv'
+  let senv = add_field (l,SFBmodtype mtb) MT senv in
+  mp, senv
 
 (** full_add_module adds module with universes and constraints *)
 
 let full_add_module mb senv =
-  let senv = add_constraints (Now mb.mod_constraints) senv in
   let dp = ModPath.dp mb.mod_mp in
   let linkinfo = Nativecode.link_info_of_dirpath dp in
   { senv with env = Modops.add_linked_module mb linkinfo senv.env }
 
 let full_add_module_type mp mt senv =
-  let senv = add_constraints (Now mt.mod_constraints) senv in
   { senv with env = Modops.add_module_type mp mt senv.env }
 
 (** Insertion of modules *)
 
 let add_module l me inl senv =
   let mp = MPdot(senv.modpath, l) in
-  let mb = Mod_typing.translate_module senv.env mp inl me in
+  let mb, cst = Mod_typing.translate_module senv.env mp inl me in
+  let senv = push_context_set ~strict:true (Univ.LSet.empty,cst) senv in
   let mb = Declareops.hcons_module_body mb in
-  let senv' = add_field (l,SFBmodule mb) M senv in
-  let senv'' =
-    if Modops.is_functor mb.mod_type then senv'
-    else update_resolver (Mod_subst.add_delta_resolver mb.mod_delta) senv'
+  let senv = add_field (l,SFBmodule mb) M senv in
+  let senv =
+    if Modops.is_functor mb.mod_type then senv
+    else update_resolver (Mod_subst.add_delta_resolver mb.mod_delta) senv
   in
-  (mp,mb.mod_delta),senv''
+  (mp,mb.mod_delta),senv
 
 (** {6 Starting / ending interactive modules and module types } *)
 
@@ -1046,7 +1046,8 @@ let start_modtype l senv =
 let add_module_parameter mbid mte inl senv =
   let () = check_empty_struct senv in
   let mp = MPbound mbid in
-  let mtb = Mod_typing.translate_modtype senv.env mp inl ([],mte) in
+  let mtb, cst = Mod_typing.translate_modtype senv.env mp inl ([],mte) in
+  let senv = push_context_set ~strict:true (Univ.LSet.empty,cst) senv in
   let senv = full_add_module_type mp mtb senv in
   let new_variant = match senv.modvariant with
     | STRUCT (params,oldenv) -> STRUCT ((mbid,mtb) :: params, oldenv)
@@ -1084,12 +1085,12 @@ let functorize_module params mb =
 let build_module_body params restype senv =
   let struc = NoFunctor (List.rev senv.revstruct) in
   let restype' = Option.map (fun (ty,inl) -> (([],ty),inl)) restype in
-  let mb =
+  let mb, cst =
     Mod_typing.finalize_module senv.env senv.modpath
-      (struc,None,senv.modresolver,senv.univ) restype'
+      (struc,None,senv.modresolver,Univ.Constraint.empty) restype'
   in
   let mb' = functorize_module params mb in
-  { mb' with mod_retroknowledge = ModBodyRK senv.local_retroknowledge }
+  { mb' with mod_retroknowledge = ModBodyRK senv.local_retroknowledge }, cst
 
 (** Returning back to the old pre-interactive-module environment,
     with one extra component and some updated fields
@@ -1129,15 +1130,13 @@ let end_module l restype senv =
   let () = check_current_label l mp in
   let () = check_empty_context senv in
   let mbids = List.rev_map fst params in
-  let mb = build_module_body params restype senv in
+  let mb, cst = build_module_body params restype senv in
+  let senv = push_context_set ~strict:true (Univ.LSet.empty,cst) senv in
   let newenv = Environ.set_opaque_tables oldsenv.env (Environ.opaque_tables senv.env) in
   let newenv = Environ.set_native_symbols newenv senv.env.Environ.native_symbols in
   let newenv = set_engagement_opt newenv senv.engagement in
-  let senv'=
-    propagate_loads { senv with
-      env = newenv;
-      univ = Univ.ContextSet.union senv.univ mb.mod_constraints} in
-  let newenv = Environ.push_context_set ~strict:true mb.mod_constraints senv'.env in
+  let newenv = Environ.set_universes (Environ.universes senv.env) newenv in
+  let senv' = propagate_loads { senv with env = newenv } in
   let newenv = Modops.add_module mb newenv in
   let newresolver =
     if Modops.is_functor mb.mod_type then oldsenv.modresolver
@@ -1146,12 +1145,11 @@ let end_module l restype senv =
   (mp,mbids,mb.mod_delta),
   propagate_senv (l,SFBmodule mb) newenv newresolver senv' oldsenv
 
-let build_mtb mp sign cst delta =
+let build_mtb mp sign delta =
   { mod_mp = mp;
     mod_expr = ();
     mod_type = sign;
     mod_type_alg = None;
-    mod_constraints = cst;
     mod_delta = delta;
     mod_retroknowledge = ModTypeRK }
 
@@ -1163,11 +1161,11 @@ let end_modtype l senv =
   let mbids = List.rev_map fst params in
   let newenv = Environ.set_opaque_tables oldsenv.env (Environ.opaque_tables senv.env) in
   let newenv = Environ.set_native_symbols newenv senv.env.Environ.native_symbols in
-  let newenv = Environ.push_context_set ~strict:true senv.univ newenv in
   let newenv = set_engagement_opt newenv senv.engagement in
+  let newenv = Environ.set_universes (Environ.universes senv.env) newenv in
   let senv' = propagate_loads {senv with env=newenv} in
   let auto_tb = functorize params (NoFunctor (List.rev senv.revstruct)) in
-  let mtb = build_mtb mp auto_tb senv'.univ senv.modresolver in
+  let mtb = build_mtb mp auto_tb senv.modresolver in
   let newenv = Environ.add_modtype mtb senv'.env in
   let newresolver = oldsenv.modresolver in
   (mp,mbids),
@@ -1181,7 +1179,7 @@ let add_include me is_module inl senv =
   let sign,(),resolver,cst =
     translate_mse_incl is_module senv.env mp_sup inl me
   in
-  let senv = add_constraints (Now cst) senv in
+  let senv = push_context_set ~strict:true (Univ.LSet.empty,cst) senv in
   (* Include Self support  *)
   let rec compute_sign sign mb resolver senv =
     match sign with
@@ -1201,7 +1199,7 @@ let add_include me is_module inl senv =
   in
   let resolver,str,senv =
     let struc = NoFunctor (List.rev senv.revstruct) in
-    let mtb = build_mtb mp_sup struc Univ.ContextSet.empty senv.modresolver in
+    let mtb = build_mtb mp_sup struc senv.modresolver in
     compute_sign sign mtb resolver senv
   in
   let senv = update_resolver (Mod_subst.add_delta_resolver resolver) senv
@@ -1223,6 +1221,8 @@ let add_include me is_module inl senv =
 
 let module_of_library lib = lib.comp_mod
 
+let univs_of_library lib = lib.comp_univs
+
 type native_library = Nativecode.global list
 
 (** FIXME: MS: remove?*)
@@ -1251,7 +1251,6 @@ let export ?except ~output_native_objects senv dir =
       mod_expr = FullStruct;
       mod_type = str;
       mod_type_alg = None;
-      mod_constraints = senv.univ;
       mod_delta = senv.modresolver;
       mod_retroknowledge = ModBodyRK senv.local_retroknowledge
     }
@@ -1264,6 +1263,7 @@ let export ?except ~output_native_objects senv dir =
   let lib = {
     comp_name = dir;
     comp_mod = mb;
+    comp_univs = senv.univ;
     comp_deps = Array.of_list (DPmap.bindings senv.required);
     comp_enga = Environ.engagement senv.env;
     comp_natsymbs = symbols }
@@ -1271,7 +1271,7 @@ let export ?except ~output_native_objects senv dir =
   mp, lib, ast
 
 (* cst are the constraints that were computed by the vi2vo step and hence are
- * not part of the mb.mod_constraints field (but morally should be) *)
+ * not part of the [lib.comp_univs] field (but morally should be) *)
 let import lib cst vodigest senv =
   check_required senv.required lib.comp_deps;
   check_engagement senv.env lib.comp_enga;
@@ -1281,8 +1281,8 @@ let import lib cst vodigest senv =
   let mp = MPfile lib.comp_name in
   let mb = lib.comp_mod in
   let env = Environ.push_context_set ~strict:true
-                                     (Univ.ContextSet.union mb.mod_constraints cst)
-                                     senv.env
+      (Univ.ContextSet.union lib.comp_univs cst)
+      senv.env
   in
   let env =
     let linkinfo = Nativecode.link_info_of_dirpath lib.comp_name in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index b42746a882..58a583e169 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -195,6 +195,7 @@ type compiled_library
 type native_library = Nativecode.global list
 
 val module_of_library : compiled_library -> Declarations.module_body
+val univs_of_library : compiled_library -> Univ.ContextSet.t
 
 val start_library : DirPath.t -> ModPath.t safe_transformer
 
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 3f81a62956..28baa82666 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -336,7 +336,6 @@ and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv =
              mod_expr = Abstract;
              mod_type = subst_signature subst1 body_t1;
              mod_type_alg = None;
-             mod_constraints = mtb1.mod_constraints;
              mod_retroknowledge = ModBodyRK [];
              mod_delta = mtb1.mod_delta} env
         in
@@ -347,7 +346,6 @@ 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
-- 
cgit v1.2.3