From 4838fd47542018ba61cd096c93edf45b7ef68529 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 8 Aug 2019 13:48:57 +0200
Subject: Refine the API to declare section-local universes.

The section local universes are undoubtedly ordered, but the API was requiring
an unordered ContextSet. We also move the naming one level up.

Unfortunately, some callers are currently defining the same polymorphic
universes in a section several times, notably the "Variable" command. I had
to hack around this behaviour.
---
 tactics/declare.ml | 27 ++++++++++++++++++++++++---
 1 file changed, 24 insertions(+), 3 deletions(-)

(limited to 'tactics')

diff --git a/tactics/declare.ml b/tactics/declare.ml
index 3a02e5451a..2f9da373aa 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_context_set true ctx; Lib.add_section_context (nas, uctx))
   else
     Lib.add_anonymous_leaf (input_universe_context ctx)
 
@@ -632,9 +653,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
-- 
cgit v1.2.3


From 58a9de2acacb05291d87fe2b656728ae05d59df4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 29 Jul 2019 10:48:28 +0200
Subject: Move the Lib section data into the kernel.

Due to the redundancy with some other declaration-specific data from the
kernel, we also seize the opportunity to clean it up. Note also that
discharging is still performed outside of the kernel for now.
---
 tactics/declare.ml | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

(limited to 'tactics')

diff --git a/tactics/declare.ml b/tactics/declare.ml
index 2f9da373aa..208b8e28a7 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -63,7 +63,7 @@ let declare_universe_context ~poly ctx =
     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_context_set true ctx; Lib.add_section_context (nas, uctx))
+    Global.push_section_context (nas, uctx)
   else
     Lib.add_anonymous_leaf (input_universe_context ctx)
 
@@ -139,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) =
@@ -373,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;
@@ -422,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) =
-- 
cgit v1.2.3