Merge PR #10664: Putting sections libstack inside the kernel

Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: gares
Reviewed-by: maximedenes

1 files changed, 24 insertions, 8 deletions

diff --git a/tactics/declare.ml b/tactics/declare.ml
index 3a02e5451a..208b8e28a7 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -40,9 +40,30 @@ let input_universe_context : Univ.ContextSet.t -> Libobject.obj =
     ~cache:(fun (na, uctx) -> Global.push_context_set false uctx)
     ~discharge:(fun (_, x) -> Some x)
 
+let name_instance inst =
+  let map lvl = match Univ.Level.name lvl with
+    | None -> (* Having Prop/Set/Var as section universes makes no sense *)
+      assert false
+    | Some na ->
+      try
+        let qid = Nametab.shortest_qualid_of_universe na in
+        Name (Libnames.qualid_basename qid)
+      with Not_found ->
+        (* Best-effort naming from the string representation of the level.
+           See univNames.ml for a similar hack. *)
+        Name (Id.of_string_soft (Univ.Level.to_string lvl))
+  in
+  Array.map map (Univ.Instance.to_array inst)
+
 let declare_universe_context ~poly ctx =
   if poly then
-    (Global.push_context_set true ctx; Lib.add_section_context ctx)
+    (* FIXME: some upper layers declare universes several times, we hack around
+      by checking whether the universes already exist. *)
+    let (univs, cstr) = ctx in
+    let univs = Univ.LSet.filter (fun u -> not (Lib.is_polymorphic_univ u)) univs in
+    let uctx = Univ.ContextSet.to_context (univs, cstr) in
+    let nas = name_instance (Univ.UContext.instance uctx) in
+    Global.push_section_context (nas, uctx)
   else
     Lib.add_anonymous_leaf (input_universe_context ctx)
 
@@ -118,8 +139,6 @@ let cache_constant ((sp,kn), obj) =
   in
   assert (Constant.equal kn' (Constant.make1 kn));
   Nametab.push (Nametab.Until 1) sp (GlobRef.ConstRef (Constant.make1 kn));
-  let cst = Global.lookup_constant kn' in
-  add_section_constant ~poly:(Declareops.constant_is_polymorphic cst) kn' cst.const_hyps;
   Dumpglob.add_constant_kind (Constant.make1 kn) obj.cst_kind
 
 let discharge_constant ((sp, kn), obj) =
@@ -352,7 +371,6 @@ let declare_variable ~name ~kind d =
       poly
   in
   Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty name) (GlobRef.VarRef name);
-  add_section_variable ~name ~poly;
   Decls.(add_variable_data name {opaque;kind});
   add_anonymous_leaf (inVariable ());
   Impargs.declare_var_implicits ~impl name;
@@ -401,8 +419,6 @@ let cache_inductive ((sp,kn),mie) =
   let id = Libnames.basename sp in
   let kn' = Global.add_mind id mie in
   assert (MutInd.equal kn' (MutInd.make1 kn));
-  let mind = Global.lookup_mind kn' in
-  add_section_kn ~poly:(Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps;
   List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names
 
 let discharge_inductive ((sp,kn),mie) =
@@ -632,9 +648,9 @@ let do_universe ~poly l =
   let ctx = List.fold_left (fun ctx (_,qid) -> Univ.LSet.add (Univ.Level.make qid) ctx)
       Univ.LSet.empty l, Univ.Constraint.empty
   in
-  let () = declare_universe_context ~poly ctx in
   let src = if poly then BoundUniv else UnqualifiedUniv in
-  Lib.add_anonymous_leaf (input_univ_names (src, l))
+  let () = Lib.add_anonymous_leaf (input_univ_names (src, l)) in
+  declare_universe_context ~poly ctx
 
 let do_constraint ~poly l =
   let open Univ in