Merge PR #12107: Remove mod_constraints field of module body

Reviewed-by: ppedrot

16 files changed, 140 insertions, 136 deletions

diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 8fd81d43be..2f795ff8d9 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -77,7 +77,6 @@ let mk_mtb mp sign delta =
     mod_expr = ();
     mod_type = sign;
     mod_type_alg = None;
-    mod_constraints = Univ.ContextSet.empty;
     mod_delta = delta;
     mod_retroknowledge = ModTypeRK; }
 
diff --git a/checker/safe_checking.ml b/checker/safe_checking.ml
index 524ffbc022..b5beab532e 100644
--- a/checker/safe_checking.ml
+++ b/checker/safe_checking.ml
@@ -14,7 +14,7 @@ open Environ
 let import senv clib univs digest =
   let mb = Safe_typing.module_of_library clib in
   let env = Safe_typing.env_of_safe_env senv in
-  let env = push_context_set ~strict:true mb.mod_constraints env in
+  let env = push_context_set ~strict:true (Safe_typing.univs_of_library clib) env in
   let env = push_context_set ~strict:true univs env in
   let env = Modops.add_retroknowledge mb.mod_retroknowledge env in
   Mod_checking.check_module env mb.mod_mp mb;
diff --git a/checker/values.ml b/checker/values.ml
index 9bd381e4a9..76e3ab0d45 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -359,17 +359,17 @@ and v_impl =
 and v_noimpl = v_unit
 and v_module =
   Tuple ("module_body",
-         [|v_mp;v_impl;v_sign;Opt v_mexpr;v_context_set;v_resolver;v_retroknowledge|])
+         [|v_mp;v_impl;v_sign;Opt v_mexpr;v_resolver;v_retroknowledge|])
 and v_modtype =
   Tuple ("module_type_body",
-         [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_context_set;v_resolver;v_unit|])
+         [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_resolver;v_unit|])
 
 (** kernel/safe_typing *)
 
 let v_vodigest = Sum ("module_impl",0, [| [|String|]; [|String;String|] |])
 let v_deps = Array (v_tuple "dep" [|v_dp;v_vodigest|])
 let v_compiled_lib =
-  v_tuple "compiled" [|v_dp;v_module;v_deps;v_engagement;Any|]
+  v_tuple "compiled" [|v_dp;v_module;v_context_set;v_deps;v_engagement;Any|]
 
 (** Library objects *)
 
diff --git a/dev/ci/user-overlays/12107-SkySkimmer-no-mod-univs.sh b/dev/ci/user-overlays/12107-SkySkimmer-no-mod-univs.sh
new file mode 100644
index 0000000000..b5faabcfe1
--- /dev/null
+++ b/dev/ci/user-overlays/12107-SkySkimmer-no-mod-univs.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "12107" ] || [ "$CI_BRANCH" = "no-mod-univs" ]; then
+
+    elpi_CI_REF=no-mod-univs
+    elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
+
+fi
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 11d4120d7c..2f6a870c8a 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -295,8 +295,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 b347152c16..0ab99cab35 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -391,7 +391,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
 
@@ -400,7 +399,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
@@ -409,7 +407,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 cf01711fe7..d6d52dbc2b 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 4195f112ca..7a46538772 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 9fabb441d1..93337fca5d 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
@@ -564,8 +565,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
@@ -984,35 +984,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 } *)
 
@@ -1044,7 +1044,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)
@@ -1082,12 +1083,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
@@ -1127,15 +1128,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
@@ -1144,12 +1143,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 }
 
@@ -1161,11 +1159,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),
@@ -1179,7 +1177,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
@@ -1199,7 +1197,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
@@ -1221,6 +1219,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?*)
@@ -1249,7 +1249,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
     }
@@ -1262,6 +1261,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 }
@@ -1269,7 +1269,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;
@@ -1279,8 +1279,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 f5bd27ca12..b601279e87 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -194,6 +194,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
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 02383799a9..f7d78551d8 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -163,7 +163,8 @@ let expand_mexpr env mpo me =
 
 let expand_modtype env mp me =
   let inl = Some (Flags.get_inline_level()) in
-  Mod_typing.translate_modtype env mp inl ([],me)
+  let mtb, _cst = Mod_typing.translate_modtype env mp inl ([],me) in
+  mtb
 
 let no_delta = Mod_subst.empty_delta_resolver
 
diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml
index 438509e28a..50fa6052f6 100644
--- a/vernac/declaremods.ml
+++ b/vernac/declaremods.ml
@@ -651,26 +651,28 @@ let mk_params_entry args =
 
 let mk_funct_type env args seb0 =
   List.fold_left
-    (fun seb (arg_id,arg_t,arg_inl) ->
+    (fun (seb,cst) (arg_id,arg_t,arg_inl) ->
       let mp = MPbound arg_id in
-      let arg_t = Mod_typing.translate_modtype env mp arg_inl ([],arg_t) in
-      MoreFunctor(arg_id,arg_t,seb))
+      let arg_t, cst' = Mod_typing.translate_modtype env mp arg_inl ([],arg_t) in
+      MoreFunctor(arg_id,arg_t,seb), Univ.Constraint.union cst cst')
     seb0 args
 
 (** Prepare the module type list for check of subtypes *)
 
 let build_subtypes env mp args mtys =
-  let (cst, ans) = List.fold_left_map
-    (fun cst (m,ann) ->
+  let (ctx, ans) = List.fold_left_map
+    (fun ctx (m,ann) ->
        let inl = inl2intopt ann in
-       let mte, _, cst' = Modintern.interp_module_ast env Modintern.ModType m in
-       let env = Environ.push_context_set ~strict:true cst' env in
-       let cst = Univ.ContextSet.union cst cst' in
-       let mtb = Mod_typing.translate_modtype env mp inl ([],mte) in
-       cst, { mtb with mod_type = mk_funct_type env args mtb.mod_type })
+       let mte, _, ctx' = Modintern.interp_module_ast env Modintern.ModType m in
+       let env = Environ.push_context_set ~strict:true ctx' env in
+       let ctx = Univ.ContextSet.union ctx ctx' in
+       let mtb, cst = Mod_typing.translate_modtype env mp inl ([],mte) in
+       let mod_type, cst = mk_funct_type env args (mtb.mod_type,cst) in
+       let ctx = Univ.ContextSet.add_constraints cst ctx in
+       ctx, { mtb with mod_type })
     Univ.ContextSet.empty mtys
   in
-  (ans, cst)
+  (ans, ctx)
 
 
 (** {6 Current module information}
@@ -703,23 +705,23 @@ module RawModOps = struct
 
 let start_module export id args res fs =
   let mp = Global.start_module id in
-  let arg_entries_r, cst = intern_args args in
-  let () = Global.push_context_set ~strict:true cst in
+  let arg_entries_r, ctx = intern_args args in
+  let () = Global.push_context_set ~strict:true ctx in
   let env = Global.env () in
-  let res_entry_o, subtyps, cst = match res with
+  let res_entry_o, subtyps, ctx = match res with
     | Enforce (res,ann) ->
         let inl = inl2intopt ann in
-        let (mte, _, cst) = Modintern.interp_module_ast env Modintern.ModType res in
-        let env = Environ.push_context_set ~strict:true cst env in
+        let (mte, _, ctx) = Modintern.interp_module_ast env Modintern.ModType res in
+        let env = Environ.push_context_set ~strict:true ctx env in
         (* We check immediately that mte is well-formed *)
-        let _, _, _, cst' = Mod_typing.translate_mse env None inl mte in
-        let cst = Univ.ContextSet.union cst cst' in
-        Some (mte, inl), [], cst
+        let _, _, _, cst = Mod_typing.translate_mse env None inl mte in
+        let ctx = Univ.ContextSet.add_constraints cst ctx in
+        Some (mte, inl), [], ctx
     | Check resl ->
-      let typs, cst = build_subtypes env mp arg_entries_r resl in
-      None, typs, cst
+      let typs, ctx = build_subtypes env mp arg_entries_r resl in
+      None, typs, ctx
   in
-  let () = Global.push_context_set ~strict:true cst in
+  let () = Global.push_context_set ~strict:true ctx in
   openmod_info := { cur_typ = res_entry_o; cur_typs = subtyps };
   let prefix = Lib.start_module export id mp fs in
   Nametab.(push_dir (Until 1) (prefix.obj_dir) (GlobDirRef.DirOpenModule prefix));
@@ -763,37 +765,38 @@ let end_module () =
 
   mp
 
+(* TODO cleanup push universes directly to global env *)
 let declare_module id args res mexpr_o fs =
   (* We simulate the beginning of an interactive module,
      then we adds the module parameters to the global env. *)
   let mp = Global.start_module id in
-  let arg_entries_r, cst = intern_args args in
+  let arg_entries_r, ctx = intern_args args in
   let params = mk_params_entry arg_entries_r in
   let env = Global.env () in
-  let env = Environ.push_context_set ~strict:true cst env in
-  let mty_entry_o, subs, inl_res, cst' = match res with
+  let env = Environ.push_context_set ~strict:true ctx env in
+  let mty_entry_o, subs, inl_res, ctx' = match res with
     | Enforce (mty,ann) ->
         let inl = inl2intopt ann in
-        let (mte, _, cst) = Modintern.interp_module_ast env Modintern.ModType mty in
-        let env = Environ.push_context_set ~strict:true cst env in
+        let (mte, _, ctx) = Modintern.interp_module_ast env Modintern.ModType mty in
+        let env = Environ.push_context_set ~strict:true ctx env in
         (* We check immediately that mte is well-formed *)
-        let _, _, _, cst' = Mod_typing.translate_mse env None inl mte in
-        let cst = Univ.ContextSet.union cst cst' in
-        Some mte, [], inl, cst
+        let _, _, _, cst = Mod_typing.translate_mse env None inl mte in
+        let ctx = Univ.ContextSet.add_constraints cst ctx in
+        Some mte, [], inl, ctx
     | Check mtys ->
-      let typs, cst = build_subtypes env mp arg_entries_r mtys in
-      None, typs, default_inline (), cst
+      let typs, ctx = build_subtypes env mp arg_entries_r mtys in
+      None, typs, default_inline (), ctx
   in
-  let env = Environ.push_context_set ~strict:true cst' env in
-  let cst = Univ.ContextSet.union cst cst' in
-  let mexpr_entry_o, inl_expr, cst' = match mexpr_o with
+  let env = Environ.push_context_set ~strict:true ctx' env in
+  let ctx = Univ.ContextSet.union ctx ctx' in
+  let mexpr_entry_o, inl_expr, ctx' = match mexpr_o with
     | None -> None, default_inline (), Univ.ContextSet.empty
     | Some (mexpr,ann) ->
-      let (mte, _, cst) = Modintern.interp_module_ast env Modintern.Module mexpr in
-      Some mte, inl2intopt ann, cst
+      let (mte, _, ctx) = Modintern.interp_module_ast env Modintern.Module mexpr in
+      Some mte, inl2intopt ann, ctx
   in
-  let env = Environ.push_context_set ~strict:true cst' env in
-  let cst = Univ.ContextSet.union cst cst' in
+  let env = Environ.push_context_set ~strict:true ctx' env in
+  let ctx = Univ.ContextSet.union ctx ctx' in
   let entry = match mexpr_entry_o, mty_entry_o with
     | None, None -> assert false (* No body, no type ... *)
     | None, Some typ -> MType (params, typ)
@@ -812,7 +815,7 @@ let declare_module id args res mexpr_o fs =
   | None -> None
   | _ -> inl_res
   in
-  let () = Global.push_context_set ~strict:true cst in
+  let () = Global.push_context_set ~strict:true ctx in
   let mp_env,resolver = Global.add_module id entry inl in
 
   (* Name consistency check : kernel vs. library *)
@@ -864,20 +867,20 @@ let declare_modtype id args mtys (mty,ann) fs =
   (* We simulate the beginning of an interactive module,
      then we adds the module parameters to the global env. *)
   let mp = Global.start_modtype id in
-  let arg_entries_r, cst = intern_args args in
-  let () = Global.push_context_set ~strict:true cst in
+  let arg_entries_r, ctx = intern_args args in
+  let () = Global.push_context_set ~strict:true ctx in
   let params = mk_params_entry arg_entries_r in
   let env = Global.env () in
-  let mte, _, cst = Modintern.interp_module_ast env Modintern.ModType mty in
-  let () = Global.push_context_set ~strict:true cst in
+  let mte, _, ctx = Modintern.interp_module_ast env Modintern.ModType mty in
+  let () = Global.push_context_set ~strict:true ctx in
   let env = Global.env () in
   (* We check immediately that mte is well-formed *)
   let _, _, _, cst = Mod_typing.translate_mse env None inl mte in
-  let () = Global.push_context_set ~strict:true cst in
+  let () = Global.push_context_set ~strict:true (Univ.LSet.empty,cst) in
   let env = Global.env () in
   let entry = params, mte in
-  let sub_mty_l, cst = build_subtypes env mp arg_entries_r mtys in
-  let () = Global.push_context_set ~strict:true cst in
+  let sub_mty_l, ctx = build_subtypes env mp arg_entries_r mtys in
+  let () = Global.push_context_set ~strict:true ctx in
   let env = Global.env () in
   let sobjs = get_functor_sobjs false env inl entry in
   let subst = map_mp (get_module_path (snd entry)) mp empty_delta_resolver in