Merge PR #12107: Remove mod_constraints field of module body

Reviewed-by: ppedrot

1 files changed, 33 insertions, 33 deletions

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