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.

10 files changed, 407 insertions, 190 deletions

diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 66bac15e9a..20e742d7f8 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -49,4 +49,5 @@ Term_typing
 Subtyping
 Mod_typing
 Nativelibrary
+Section
 Safe_typing
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 783ce63b8c..8d34f3a34f 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -113,16 +113,9 @@ type library_info = DirPath.t * vodigest
 (** Functor and funsig parameters, most recent first *)
 type module_parameters = (MBId.t * module_type_body) list
 
-(** Sections can be nested with the proviso that no monomorphic section can be
-    opened inside a polymorphic one. The reverse is allowed. *)
-type sections = {
-  sec_poly : int;
-  sec_mono : int;
-}
-
 type safe_environment =
   { env : Environ.env;
-    sections : sections;
+    sections : Section.t;
     modpath : ModPath.t;
     modvariant : modvariant;
     modresolver : Mod_subst.delta_resolver;
@@ -150,11 +143,6 @@ let rec library_dp_of_senv senv =
   | SIG(_,senv) -> library_dp_of_senv senv
   | STRUCT(_,senv) -> library_dp_of_senv senv
 
-let empty_sections = {
-  sec_poly = 0;
-  sec_mono = 0;
-}
-
 let empty_environment =
   { env = Environ.empty_env;
     modpath = ModPath.initial;
@@ -164,7 +152,7 @@ let empty_environment =
     revstruct = [];
     modlabels = Label.Set.empty;
     objlabels = Label.Set.empty;
-    sections = empty_sections;
+    sections = Section.empty;
     future_cst = [];
     univ = Univ.ContextSet.empty;
     engagement = None;
@@ -331,11 +319,16 @@ let universes_of_private eff =
 let env_of_safe_env senv = senv.env
 let env_of_senv = env_of_safe_env
 
+let sections_of_safe_env senv = senv.sections
+
 type constraints_addition =
   | Now of Univ.ContextSet.t
   | Later of Univ.ContextSet.t Future.computation
 
 let push_context_set poly cst senv =
+  let () = if Section.is_polymorphic senv.sections && not (Univ.ContextSet.is_empty cst) then
+    CErrors.user_err (Pp.str "Cannot add global universe constraints inside a polymorphic section.")
+  in
   { senv with
     env = Environ.push_context_set ~strict:(not poly) cst senv.env;
     univ = Univ.ContextSet.union cst senv.univ }
@@ -399,11 +392,8 @@ let check_current_library dir senv = match senv.modvariant with
 
 (** When operating on modules, we're normally outside sections *)
 
-let is_empty_sections s =
-  Int.equal s.sec_poly 0 && Int.equal s.sec_mono 0
-
 let check_empty_context senv =
-  assert (Environ.empty_context senv.env && is_empty_sections senv.sections)
+  assert (Environ.empty_context senv.env && Section.is_empty senv.sections)
 
 (** When adding a parameter to the current module/modtype,
     it must have been freshly started *)
@@ -450,21 +440,30 @@ let safe_push_named d env =
     with Not_found -> () in
   Environ.push_named d env
 
-
 let push_named_def (id,de) senv =
-  let () = assert (not @@ is_empty_sections senv.sections) in
+  let sections = Section.push_local senv.sections in
   let c, r, typ = Term_typing.translate_local_def senv.env id de in
   let x = Context.make_annot id r in
   let env'' = safe_push_named (LocalDef (x, c, typ)) senv.env in
-  { senv with env = env'' }
+  { senv with sections; env = env'' }
 
 let push_named_assum (x,t) senv =
-  let () = assert (not @@ is_empty_sections senv.sections) in
+  let sections = Section.push_local senv.sections in
   let t, r = Term_typing.translate_local_assum senv.env t in
   let x = Context.make_annot x r in
   let env'' = safe_push_named (LocalAssum (x,t)) senv.env in
-    {senv with env=env''}
-
+  { senv with sections; env = env'' }
+
+let push_section_context (nas, ctx) senv =
+  let sections = Section.push_context (nas, ctx) senv.sections in
+  let senv = { senv with sections } in
+  let ctx = Univ.ContextSet.of_context ctx in
+  (* We check that the universes are fresh. FIXME: This should be done
+     implicitly, but we have to work around the API. *)
+  let () = assert (Univ.LSet.for_all (fun u -> not (Univ.LSet.mem u (fst senv.univ))) (fst ctx)) in
+  { senv with
+    env = Environ.push_context_set ~strict:false ctx senv.env;
+    univ = Univ.ContextSet.union ctx senv.univ }
 
 (** {6 Insertion of new declarations to current environment } *)
 
@@ -546,8 +545,19 @@ let add_field ?(is_include=false) ((l,sfb) as field) gn senv =
     | SFBmodule mb, M -> Modops.add_module mb senv.env
     | _ -> assert false
   in
+  let sections = match sfb, gn with
+  | SFBconst cb, C con ->
+    let poly = Declareops.constant_is_polymorphic cb in
+    Section.push_constant ~poly con senv.sections
+  | SFBmind mib, I mind ->
+    let poly = Declareops.inductive_is_polymorphic mib in
+    Section.push_inductive ~poly mind senv.sections
+  | _, (M | MT) -> senv.sections
+  | _ -> assert false
+  in
   { senv with
     env = env';
+    sections;
     revstruct = field :: senv.revstruct;
     modlabels = Label.Set.union mlabs senv.modlabels;
     objlabels = Label.Set.union olabs senv.objlabels }
@@ -924,26 +934,13 @@ let add_module l me inl senv =
 (** {6 Interactive sections *)
 
 let open_section ~poly senv =
-  let sections = senv.sections in
-  if poly then
-    let sections = { sections with sec_poly = sections.sec_poly + 1 } in
-    { senv with sections }
-  else if Int.equal sections.sec_poly 0 then
-    let sections = { sections with sec_mono = sections.sec_mono + 1 } in
-    { senv with sections }
-  else
-    CErrors.anomaly (Pp.str "Cannot open a monomorphic section inside a polymorphic one")
+  let sections = Section.open_section ~poly senv.sections in
+  { senv with sections }
 
 let close_section senv =
-  let sections = senv.sections in
-  if not (Int.equal sections.sec_poly 0) then
-    let sections = { sections with sec_poly = sections.sec_poly - 1 } in
-    { senv with sections }
-  else if not (Int.equal sections.sec_mono 0) then
-    let sections = { sections with sec_mono = sections.sec_mono - 1 } in
-    { senv with sections }
-  else
-    CErrors.anomaly (Pp.str "No open section")
+  (* TODO: implement me when discharging in kernel *)
+  let sections = Section.close_section senv.sections in
+  { senv with sections }
 
 (** {6 Starting / ending interactive modules and module types } *)
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 4eef43b193..10fedc2faf 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -33,6 +33,8 @@ val is_initial : safe_environment -> bool
 
 val env_of_safe_env : safe_environment -> Environ.env
 
+val sections_of_safe_env : safe_environment -> Section.t
+
 (** The safe_environment state monad *)
 
 type safe_transformer0 = safe_environment -> safe_environment
@@ -67,15 +69,6 @@ val join_safe_environment :
 val is_joined_environment : safe_environment -> bool
 (** {6 Enriching a safe environment } *)
 
-(** Insertion of local declarations (Local or Variables) *)
-
-val push_named_assum : (Id.t * Constr.types) -> safe_transformer0
-
-(** Returns the full universe context necessary to typecheck the definition
-  (futures are forced) *)
-val push_named_def :
-  Id.t * Entries.section_def_entry -> safe_transformer0
-
 (** Insertion of global axioms or definitions *)
 
 type 'a effect_entry =
@@ -146,6 +139,16 @@ val open_section : poly:bool -> safe_transformer0
 
 val close_section : safe_transformer0
 
+(** Insertion of local declarations (Local or Variables) *)
+
+val push_named_assum : (Id.t * Constr.types) -> safe_transformer0
+
+val push_named_def :
+  Id.t * Entries.section_def_entry -> safe_transformer0
+
+(** Add local universes to a polymorphic section *)
+val push_section_context : (Name.t array * Univ.UContext.t) -> safe_transformer0
+
 (** {6 Interactive module functions } *)
 
 val start_module : Label.t -> ModPath.t safe_transformer
diff --git a/kernel/section.ml b/kernel/section.ml
new file mode 100644
index 0000000000..12e9c2fd60
--- /dev/null
+++ b/kernel/section.ml
@@ -0,0 +1,250 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Util
+open Names
+open Univ
+
+module NamedDecl = Context.Named.Declaration
+
+type _ section_kind =
+| SecMono : [ `mono ] section_kind
+| SecPoly : [ `poly ] section_kind
+
+type _ section_universes =
+| SecMonoUniv : [ `mono ] section_universes
+| SecPolyUniv : Name.t array * UContext.t -> [ `poly ] section_universes
+
+type section_entry =
+| SecDefinition of Constant.t
+| SecInductive of MutInd.t
+
+type 'a entry_map = 'a Cmap.t * 'a Mindmap.t
+
+type 'a section = {
+  sec_context : int;
+  (** Length of the named context suffix that has been introduced locally *)
+  sec_universes : 'a section_universes;
+  (** Universes local to the section *)
+  sec_entries : section_entry list;
+  (** Definitions introduced in the section *)
+  sec_data : 'a section_universes entry_map;
+}
+
+(** Sections can be nested with the proviso that no monomorphic section can be
+    opened inside a polymorphic one. The reverse is allowed. *)
+type t = {
+  sec_poly : [ `poly ] section list;
+  sec_mono : [ `mono ] section list;
+}
+
+let empty = {
+  sec_poly = [];
+  sec_mono = [];
+}
+
+let is_empty s =
+  List.is_empty s.sec_poly && List.is_empty s.sec_mono
+
+let is_polymorphic s =
+  not (List.is_empty s.sec_poly)
+
+let find_emap e (cmap, imap) = match e with
+| SecDefinition con -> Cmap.find con cmap
+| SecInductive ind -> Mindmap.find ind imap
+
+let add_emap e v (cmap, imap) = match e with
+| SecDefinition con -> (Cmap.add con v cmap, imap)
+| SecInductive ind -> (cmap, Mindmap.add ind v imap)
+
+type on_sec = { on_sec : 'a. 'a section_kind -> 'a section -> 'a section }
+
+let on_last_section f { sec_poly; sec_mono } = match sec_poly, sec_mono with
+| [], [] -> CErrors.user_err (Pp.str "No opened section")
+| sec :: rem, _ ->
+  let sec_poly = f.on_sec SecPoly sec :: rem in
+  { sec_mono; sec_poly }
+| [], sec :: rem ->
+  let sec_mono = f.on_sec SecMono sec :: rem in
+  { sec_mono; sec_poly }
+
+type 'r with_sec = { with_sec : 'a. ('a section_kind * 'a section) option -> 'r }
+
+let with_last_section f { sec_poly; sec_mono } = match sec_poly, sec_mono with
+| [], [] -> f.with_sec None
+| sec :: _, _ -> f.with_sec (Some (SecPoly, sec))
+| [], sec :: _ -> f.with_sec (Some (SecMono, sec))
+
+let push_local s =
+  let on_sec _ sec = { sec with sec_context = sec.sec_context + 1 } in
+  on_last_section { on_sec } s
+
+let push_context (nas, ctx) s =
+  let on_sec (type a) (kind : a section_kind) (sec : a section) : a section = match kind with
+  | SecMono ->
+    CErrors.anomaly (Pp.str "Adding polymorphic constraints to monomorphic section")
+  | SecPoly ->
+    let SecPolyUniv (snas, sctx) = sec.sec_universes in
+    let sec_universes = SecPolyUniv (Array.append snas nas, UContext.union sctx ctx) in
+    { sec with sec_universes }
+  in
+  on_last_section { on_sec } s
+
+let open_section ~poly sections =
+  if poly then
+    let sec = {
+      sec_context = 0;
+      sec_universes = SecPolyUniv ([||], Univ.UContext.empty);
+      sec_entries = [];
+      sec_data = (Cmap.empty, Mindmap.empty);
+    } in
+    { sections with sec_poly = sec :: sections.sec_poly }
+  else if List.is_empty sections.sec_poly then
+    let sec = {
+      sec_context = 0;
+      sec_universes = SecMonoUniv;
+      sec_entries = [];
+      sec_data = (Cmap.empty, Mindmap.empty);
+    } in
+    { sections with sec_mono = sec :: sections.sec_mono }
+  else
+    CErrors.user_err (Pp.str "Cannot open a monomorphic section inside a polymorphic one")
+
+let close_section sections =
+  (* TODO: implement me correctly when discharging in kernel *)
+  match sections.sec_poly, sections.sec_mono with
+  | _sec :: psecs, _ ->
+    let sections = { sections with sec_poly = psecs } in
+    sections
+  | [], _sec :: msecs ->
+    let sections = { sections with sec_mono = msecs } in
+    sections
+  | [], [] ->
+    CErrors.user_err (Pp.str "No opened section.")
+
+let same_poly (type a) ~poly (knd : a section_kind) = match knd with
+| SecPoly -> poly
+| SecMono -> not poly
+
+let push_global ~poly e s =
+  if is_empty s then s
+  else
+    let on_sec knd sec =
+      if same_poly ~poly knd then { sec with
+        sec_entries = e :: sec.sec_entries;
+        sec_data = add_emap e sec.sec_universes sec.sec_data;
+      } else
+        CErrors.user_err (Pp.str "Cannot mix universe polymorphic and \
+          monomorphic declarations in sections.")
+    in
+    on_last_section { on_sec } s
+
+let push_constant ~poly con s = push_global ~poly (SecDefinition con) s
+
+let push_inductive ~poly ind s = push_global ~poly (SecInductive ind) s
+
+type abstr_info = {
+  abstr_ctx : Constr.named_context;
+  abstr_subst : Univ.Instance.t;
+  abstr_uctx : Univ.AUContext.t;
+}
+
+let empty_segment = {
+  abstr_ctx = [];
+  abstr_subst = Instance.empty;
+  abstr_uctx = AUContext.empty;
+}
+
+let extract_hyps sec vars hyps =
+  (* FIXME: this code is fishy. It is supposed to check that declared section
+     variables are an ordered subset of the ambient ones, but it doesn't check
+     e.g. uniqueness of naming nor convertibility of the section data. *)
+  let rec aux ids hyps = match ids, hyps with
+  | id :: ids, decl :: hyps when Names.Id.equal id (NamedDecl.get_id decl) ->
+    decl :: aux ids hyps
+  | _ :: ids, hyps ->
+    aux ids hyps
+  | [], _ -> []
+  in
+  let ids = List.map NamedDecl.get_id @@ List.firstn sec.sec_context vars in
+  aux ids hyps
+
+let section_segment_of_entry vars e hyps sections =
+  (* [vars] are the named hypotheses, [hyps] the subset that is declared by the
+    global *)
+  let with_sec (type a) (s : (a section_kind * a section) option) = match s with
+  | None ->
+    CErrors.user_err (Pp.str "No opened section.")
+  | Some (knd, sec) ->
+    let hyps = extract_hyps sec vars hyps in
+    let inst, auctx = match knd, find_emap e sec.sec_data with
+    | SecMono, SecMonoUniv ->
+      Instance.empty, AUContext.empty
+    | SecPoly, SecPolyUniv (nas, ctx) ->
+      Univ.abstract_universes nas ctx
+    in
+    {
+      abstr_ctx = hyps;
+      abstr_subst = inst;
+      abstr_uctx = auctx;
+    }
+  in
+  with_last_section { with_sec } sections
+
+let segment_of_constant env con s =
+  let body = Environ.lookup_constant con env in
+  let vars = Environ.named_context env in
+  section_segment_of_entry vars (SecDefinition con) body.Declarations.const_hyps s
+
+let segment_of_inductive env mind s =
+  let mib = Environ.lookup_mind mind env in
+  let vars = Environ.named_context env in
+  section_segment_of_entry vars (SecInductive mind) mib.Declarations.mind_hyps s
+
+let instance_from_variable_context =
+  List.rev %> List.filter NamedDecl.is_local_assum %> List.map NamedDecl.get_id %> Array.of_list
+
+let extract_worklist info =
+  let args = instance_from_variable_context info.abstr_ctx in
+  info.abstr_subst, args
+
+let replacement_context env s =
+  let with_sec sec = match sec with
+  | None -> CErrors.user_err (Pp.str "No opened section.")
+  | Some (_, sec) ->
+    let cmap, imap = sec.sec_data in
+    let cmap = Cmap.mapi (fun con _ -> extract_worklist @@ segment_of_constant env con s) cmap in
+    let imap = Mindmap.mapi (fun ind _ -> extract_worklist @@ segment_of_inductive env ind s) imap in
+    (cmap, imap)
+  in
+  with_last_section { with_sec } s
+
+let is_in_section env gr s =
+  let with_sec sec = match sec with
+  | None -> false
+  | Some (_, sec) ->
+    let open GlobRef in
+    match gr with
+    | VarRef id ->
+      let vars = List.firstn sec.sec_context (Environ.named_context env) in
+      List.exists (fun decl -> Id.equal id (NamedDecl.get_id decl)) vars
+    | ConstRef con ->
+      Cmap.mem con (fst sec.sec_data)
+    | IndRef (ind, _) | ConstructRef ((ind, _), _) ->
+      Mindmap.mem ind (snd sec.sec_data)
+  in
+  with_last_section { with_sec } s
+
+let is_polymorphic_univ u s =
+  let check sec =
+    let SecPolyUniv (_, uctx) = sec.sec_universes in
+    Array.mem u (Instance.to_array (UContext.instance uctx))
+  in
+  List.exists check s.sec_poly
diff --git a/kernel/section.mli b/kernel/section.mli
new file mode 100644
index 0000000000..4b23115ca2
--- /dev/null
+++ b/kernel/section.mli
@@ -0,0 +1,78 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Names
+open Univ
+
+(** Kernel implementation of sections. *)
+
+type t
+(** Type of sections *)
+
+val empty : t
+
+val is_empty : t -> bool
+(** Checks whether there is no opened section *)
+
+val is_polymorphic : t -> bool
+(** Checks whether last opened section is polymorphic *)
+
+(** {6 Manipulating sections} *)
+
+val open_section : poly:bool -> t -> t
+(** Open a new section with the provided universe polymorphic status. Sections
+    can be nested, with the proviso that polymorphic sections cannot appear
+    inside a monomorphic one. *)
+
+val close_section : t -> t
+
+(** {6 Extending sections} *)
+
+val push_local : t -> t
+(** Extend the current section with a local definition (cf. push_named). *)
+
+val push_context : Name.t array * UContext.t -> t -> t
+(** Extend the current section with a local universe context. Assumes that the
+    last opened section is polymorphic. *)
+
+val push_constant : poly:bool -> Constant.t -> t -> t
+(** Make the constant as having been defined in this section. *)
+
+val push_inductive : poly:bool -> MutInd.t -> t -> t
+(** Make the inductive block as having been defined in this section. *)
+
+(** {6 Retrieving section data} *)
+
+type abstr_info = private {
+  abstr_ctx : Constr.named_context;
+  (** Section variables of this prefix *)
+  abstr_subst : Univ.Instance.t;
+  (** Actual names of the abstracted variables *)
+  abstr_uctx : Univ.AUContext.t;
+  (** Universe quantification, same length as the substitution *)
+}
+(** Data needed to abstract over the section variable and universe hypotheses *)
+
+
+val empty_segment : abstr_info
+(** Nothing to abstract *)
+
+val segment_of_constant : Environ.env -> Constant.t -> t -> abstr_info
+(** Section segment at the time of the constant declaration *)
+
+val segment_of_inductive : Environ.env -> MutInd.t -> t -> abstr_info
+(** Section segment at the time of the inductive declaration *)
+
+val replacement_context : Environ.env -> t -> Opaqueproof.work_list
+(** Section segments of all declarations from this section. *)
+
+val is_in_section : Environ.env -> GlobRef.t -> t -> bool
+
+val is_polymorphic_univ : Level.t -> t -> bool
diff --git a/library/global.ml b/library/global.ml
index e51c147f6e..3d28178d7b 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -83,6 +83,7 @@ let i2l = Label.of_id
 
 let push_named_assum a = globalize0 (Safe_typing.push_named_assum a)
 let push_named_def d = globalize0 (Safe_typing.push_named_def d)
+let push_section_context c = globalize0 (Safe_typing.push_section_context c)
 let add_constraints c = globalize0 (Safe_typing.add_constraints c)
 let push_context_set b c = globalize0 (Safe_typing.push_context_set b c)
 
diff --git a/library/global.mli b/library/global.mli
index 9ac6b1f53c..b809e9b241 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -44,6 +44,7 @@ val sprop_allowed : unit -> bool
 
 val push_named_assum : (Id.t * Constr.types) -> unit
 val push_named_def   : (Id.t * Entries.section_def_entry) -> unit
+val push_section_context : (Name.t array * Univ.UContext.t) -> unit
 
 val export_private_constants : in_section:bool ->
   Safe_typing.private_constants Entries.proof_output ->
@@ -74,7 +75,11 @@ val add_include :
 (** Sections *)
 
 val open_section : poly:bool -> unit
+(** [poly] is true when the section should be universe polymorphic *)
+
 val close_section : Summary.frozen -> unit
+(** Close the section and reset the global state to the one at the time when
+    the section what opened. *)
 
 (** Interactive modules and module types *)
 
diff --git a/library/lib.ml b/library/lib.ml
index 367a84409b..1c6f82e8a6 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -410,87 +410,11 @@ let find_opening_node id =
    - the list of substitution to do at section closing
 *)
 
-type abstr_info = {
+type abstr_info = Section.abstr_info = private {
   abstr_ctx : Constr.named_context;
   abstr_subst : Univ.Instance.t;
   abstr_uctx : Univ.AUContext.t;
 }
-type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t
-
-type secentry =
-  | Variable of {
-      id:Names.Id.t;
-    }
-  | Context of Name.t array * Univ.UContext.t
-
-type section_data = {
-  sec_entry : secentry list;
-  sec_abstr : abstr_list;
-  sec_poly  : bool;
-}
-
-let empty_section_data ~poly = {
-  sec_entry = [];
-  sec_abstr = (Names.Cmap.empty,Names.Mindmap.empty);
-  sec_poly  = poly;
-}
-
-let sectab =
-  Summary.ref ([] : section_data list) ~name:"section-context"
-
-let check_same_poly p sec =
-  if p != sec.sec_poly then
-    user_err Pp.(str  "Cannot mix universe polymorphic and monomorphic declarations in sections.")
-
-let add_section ~poly () =
-  List.iter (fun tab -> check_same_poly poly tab) !sectab;
-  sectab := empty_section_data ~poly :: !sectab
-
-let add_section_variable ~name ~poly =
-  match !sectab with
-    | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
-    | s :: sl ->
-       List.iter (fun tab -> check_same_poly poly tab) !sectab;
-       let s = { s with sec_entry = Variable {id=name} :: s.sec_entry } in
-       sectab := s :: sl
-
-let add_section_context (nas, ctx) =
-  match !sectab with
-    | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
-    | s :: sl ->
-       check_same_poly true s;
-       let s = { s with sec_entry = Context (nas, ctx) :: s.sec_entry } in
-       sectab := s :: sl
-
-exception PolyFound (* make this a let exception once possible *)
-let is_polymorphic_univ u =
-  try
-    let open Univ in
-    List.iter (fun s ->
-      let vars = s.sec_entry in
-        List.iter (function
-            | Variable _ -> ()
-            | Context (_, univs) ->
-              if Array.mem u (Instance.to_array (UContext.instance univs)) then raise PolyFound
-          ) vars
-      ) !sectab;
-    false
-  with PolyFound -> true
-
-let extract_hyps poly (secs,ohyps) =
-  let rec aux = function
-    | (Variable {id}::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) ->
-      let l, r = aux (idl,hyps) in 
-      decl :: l, r
-    | (Variable _::idl,hyps) ->
-        let l, r = aux (idl,hyps) in
-          l, r
-    | (Context (nas, ctx) :: idl, hyps) ->
-      let () = assert poly in
-       let l, (snas, sctx) = aux (idl, hyps) in
-       l, (Array.append snas nas, Univ.UContext.union sctx ctx)
-    | [], _ -> [], ([||], Univ.UContext.empty)
-  in aux (secs,ohyps)
 
 let instance_from_variable_context =
   List.rev %> List.filter is_local_assum %> List.map NamedDecl.get_id %> Array.of_list
@@ -499,47 +423,21 @@ let extract_worklist info =
   let args = instance_from_variable_context info.abstr_ctx in
   info.abstr_subst, args
 
-let make_worklist (cmap, mmap) =
-  Cmap.map extract_worklist cmap, Mindmap.map extract_worklist mmap
-
-let add_section_replacement g poly hyps =
-  match !sectab with
-  | [] -> ()
-  | s :: sl ->
-    let () = check_same_poly poly s in
-    let sechyps, (nas, ctx) = extract_hyps s.sec_poly (s.sec_entry, hyps) in
-    let subst, ctx = Univ.abstract_universes nas ctx in
-    let info = {
-      abstr_ctx = sechyps;
-      abstr_subst = subst;
-      abstr_uctx = ctx;
-    } in
-    let s = { s with
-      sec_abstr = g info s.sec_abstr;
-    } in
-    sectab := s :: sl
-
-let add_section_kn ~poly kn =
-  let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in
-    add_section_replacement f poly
-
-let add_section_constant ~poly kn =
-  let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in
-    add_section_replacement f poly
-
-let replacement_context () = make_worklist (List.hd !sectab).sec_abstr
+let sections () = Safe_typing.sections_of_safe_env @@ Global.safe_env ()
+
+let is_polymorphic_univ u =
+  Section.is_polymorphic_univ u (sections ())
+
+let replacement_context () =
+  Section.replacement_context (Global.env ()) (sections ())
 
 let section_segment_of_constant con =
-  Names.Cmap.find con (fst (List.hd !sectab).sec_abstr)
+  Section.segment_of_constant (Global.env ()) con (sections ())
 
 let section_segment_of_mutual_inductive kn =
-  Names.Mindmap.find kn (snd (List.hd !sectab).sec_abstr)
+  Section.segment_of_inductive (Global.env ()) kn (sections ())
 
-let empty_segment = {
-  abstr_ctx = [];
-  abstr_subst = Univ.Instance.empty;
-  abstr_uctx = Univ.AUContext.empty;
-}
+let empty_segment = Section.empty_segment
 
 let section_segment_of_reference = let open GlobRef in function
 | ConstRef c -> section_segment_of_constant c
@@ -550,25 +448,20 @@ let section_segment_of_reference = let open GlobRef in function
 let variable_section_segment_of_reference gr =
   (section_segment_of_reference gr).abstr_ctx
 
+let is_in_section ref =
+  Section.is_in_section (Global.env ()) ref (sections ())
+
 let section_instance = let open GlobRef in function
   | VarRef id ->
-     let eq = function
-       | Variable {id=id'} -> Names.Id.equal id id'
-       | Context _ -> false
-     in
-     if List.exists eq (List.hd !sectab).sec_entry
-     then Univ.Instance.empty, [||]
-     else raise Not_found
+    if is_in_section (VarRef id) then (Univ.Instance.empty, [||])
+    else raise Not_found
   | ConstRef con ->
-    let data = Names.Cmap.find con (fst (List.hd !sectab).sec_abstr) in
+    let data = section_segment_of_constant con in
     extract_worklist data
   | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
-    let data = Names.Mindmap.find kn (snd (List.hd !sectab).sec_abstr) in
+    let data = section_segment_of_mutual_inductive kn in
     extract_worklist data
 
-let is_in_section ref =
-  try ignore (section_instance ref); true with Not_found -> false
-
 (*************)
 (* Sections. *)
 let open_section ~poly id =
@@ -582,9 +475,7 @@ let open_section ~poly id =
   add_entry (make_foname id) (OpenedSection (prefix, fs));
   (*Pushed for the lifetime of the section: removed by unfrozing the summary*)
   Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirOpenSection prefix));
-  lib_state := { !lib_state with path_prefix = prefix };
-  add_section ~poly ()
-
+  lib_state := { !lib_state with path_prefix = prefix }
 
 (* Restore lib_stk and summaries as before the section opening, and
    add a ClosedSection object. *)
diff --git a/library/lib.mli b/library/lib.mli
index db6df4395b..5ce601f2d3 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -163,7 +163,7 @@ val drop_objects : frozen -> frozen
 val init : unit -> unit
 
 (** {6 Section management for discharge } *)
-type abstr_info = private {
+type abstr_info = Section.abstr_info = private {
   abstr_ctx : Constr.named_context;
   (** Section variables of this prefix *)
   abstr_subst : Univ.Instance.t;
@@ -181,10 +181,6 @@ val variable_section_segment_of_reference : GlobRef.t -> Constr.named_context
 val section_instance : GlobRef.t -> Univ.Instance.t * Id.t array
 val is_in_section : GlobRef.t -> bool
 
-val add_section_variable : name:Id.t -> poly:bool -> unit
-val add_section_context : Name.t array * Univ.UContext.t -> unit
-val add_section_constant : poly:bool -> Constant.t -> Constr.named_context -> unit
-val add_section_kn : poly:bool -> MutInd.t -> Constr.named_context -> unit
 val replacement_context : unit -> Opaqueproof.work_list
 
 val is_polymorphic_univ : Univ.Level.t -> bool
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) =