Merge PR #10885: Remove [in_section] arguments to Safe_typing functions

Reviewed-by: ejgallego
Reviewed-by: ppedrot

18 files changed, 59 insertions, 53 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 9b4d2e69ac..fc55720583 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -173,6 +173,8 @@ let is_initial senv =
   | [], NONE -> ModPath.equal senv.modpath ModPath.initial
   | _ -> false
 
+let sections_are_opened senv = not (Section.is_empty senv.sections)
+
 let delta_of_senv senv = senv.modresolver,senv.paramresolver
 
 let constant_of_delta_kn_senv senv kn =
@@ -587,10 +589,10 @@ type global_declaration =
 
 type exported_private_constant = Constant.t
 
-let add_constant_aux ~in_section senv (kn, cb) =
+let add_constant_aux senv (kn, cb) =
   let l = Constant.label kn in
   (* This is the only place where we hashcons the contents of a constant body *)
-  let cb = if in_section then cb else Declareops.hcons_const_body cb in
+  let cb = if sections_are_opened senv then cb else Declareops.hcons_const_body cb in
   let senv' = add_field (l,SFBconst cb) (C kn) senv in
   let senv'' = match cb.const_body with
     | Undef (Some lev) ->
@@ -799,7 +801,7 @@ let push_opaque_proof pf senv =
   let senv = { senv with env = Environ.set_opaque_tables senv.env otab } in
   senv, o
 
-let export_private_constants ~in_section ce senv =
+let export_private_constants ce senv =
   let exported, ce = export_side_effects senv.revstruct senv.env ce in
   let map senv (kn, c) = match c.const_body with
   | OpaqueDef p ->
@@ -815,10 +817,10 @@ let export_private_constants ~in_section ce senv =
   let senv, bodies = List.fold_left_map map senv exported in
   let exported = List.map (fun (kn, _) -> kn) exported in
   (* No delayed constants to declare *)
-  let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in
+  let senv = List.fold_left add_constant_aux senv bodies in
   (ce, exported), senv
 
-let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl senv : (Constant.t * a) * safe_environment =
+let add_constant (type a) ~(side_effect : a effect_entry) l decl senv : (Constant.t * a) * safe_environment =
   let kn = Constant.make2 senv.modpath l in
     let cb = 
       match decl with
@@ -852,14 +854,14 @@ let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl sen
     | Undef _ | Def _ | Primitive _ as body ->
       senv, { cb with const_body = body }, []
     in
-    let senv = add_constant_aux ~in_section senv (kn, cb) in
+    let senv = add_constant_aux senv (kn, cb) in
     add_constraints_list delayed_cst senv
   in
 
   let senv =
     match decl with
     | ConstantEntry (_,(Entries.PrimitiveEntry { Entries.prim_entry_content = CPrimitives.OT_type t; _ })) ->
-      if in_section then CErrors.anomaly (Pp.str "Primitive type not allowed in sections");
+      if sections_are_opened senv then CErrors.anomaly (Pp.str "Primitive type not allowed in sections");
       add_retroknowledge (Retroknowledge.Register_type(t,kn)) senv
     | _ -> senv
   in
@@ -1001,12 +1003,11 @@ let close_section senv =
   in
   let fold senv = function
   | `Definition (kn, cb) ->
-    let in_section = not (Section.is_empty senv.sections) in
     let info = cooking_info (Section.segment_of_constant env0 kn sections0) in
     let r = { Cooking.from = cb; info } in
     let cb = Term_typing.translate_recipe senv.env kn r in
     (* Delayed constants are already in the global environment *)
-    add_constant_aux ~in_section senv (kn, cb)
+    add_constant_aux senv (kn, cb)
   | `Inductive (ind, mib) ->
     let info = cooking_info (Section.segment_of_inductive env0 ind sections0) in
     let mie = Cooking.cook_inductive info mib in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index d97d61a72f..1b55293f1c 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -82,13 +82,13 @@ type global_declaration =
 
 type exported_private_constant = Constant.t
 
-val export_private_constants : in_section:bool ->
+val export_private_constants :
   private_constants Entries.proof_output ->
   (Constr.constr Univ.in_universe_context_set * exported_private_constant list) safe_transformer
 
 (** returns the main constant plus a certificate of its validity *)
 val add_constant :
-  side_effect:'a effect_entry -> in_section:bool -> Label.t -> global_declaration ->
+  side_effect:'a effect_entry -> Label.t -> global_declaration ->
     (Constant.t * 'a) safe_transformer
 
 (** Adding an inductive type *)
@@ -138,6 +138,8 @@ val open_section : safe_transformer0
 
 val close_section : safe_transformer0
 
+val sections_are_opened : safe_environment -> bool
+
 (** Insertion of local declarations (Local or Variables) *)
 
 val push_named_assum : (Id.t * Constr.types) -> safe_transformer0
diff --git a/kernel/section.ml b/kernel/section.ml
index babd9fe7a1..a1242f0faf 100644
--- a/kernel/section.ml
+++ b/kernel/section.ml
@@ -43,6 +43,8 @@ let empty = []
 
 let is_empty = List.is_empty
 
+let depth = List.length
+
 let has_poly_univs = function
   | [] -> false
   | sec :: _ -> sec.has_poly_univs
diff --git a/kernel/section.mli b/kernel/section.mli
index 56b4d9ba8f..ec863b3b90 100644
--- a/kernel/section.mli
+++ b/kernel/section.mli
@@ -21,6 +21,9 @@ val empty : 'a t
 val is_empty : 'a t -> bool
 (** Checks whether there is no opened section *)
 
+val depth : 'a t -> int
+(** Number of nested sections (0 if no sections are open) *)
+
 (** {6 Manipulating sections} *)
 
 type section_entry =
diff --git a/library/global.ml b/library/global.ml
index c4685370d1..24cfc57f28 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -102,8 +102,8 @@ let typing_flags () = Environ.typing_flags (env ())
 let make_sprop_cumulative () = globalize0 Safe_typing.make_sprop_cumulative
 let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b)
 let sprop_allowed () = Environ.sprop_allowed (env())
-let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd)
-let add_constant ~side_effect ~in_section id d = globalize (Safe_typing.add_constant ~side_effect ~in_section (i2l id) d)
+let export_private_constants cd = globalize (Safe_typing.export_private_constants cd)
+let add_constant ~side_effect id d = globalize (Safe_typing.add_constant ~side_effect (i2l id) d)
 let add_mind id mie = globalize (Safe_typing.add_mind (i2l id) mie)
 let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl)
 let add_module id me inl = globalize (Safe_typing.add_module (i2l id) me inl)
@@ -111,6 +111,7 @@ let add_include me ismod inl = globalize (Safe_typing.add_include me ismod inl)
 
 let open_section () = globalize0 Safe_typing.open_section
 let close_section fs = globalize0_with_summary fs Safe_typing.close_section
+let sections_are_opened () = Safe_typing.sections_are_opened (safe_env())
 
 let start_module id = globalize (Safe_typing.start_module (i2l id))
 let start_modtype id = globalize (Safe_typing.start_modtype (i2l id))
diff --git a/library/global.mli b/library/global.mli
index c45bf65d84..d689771f0a 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -46,12 +46,12 @@ 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 ->
+val export_private_constants :
   Safe_typing.private_constants Entries.proof_output ->
   Constr.constr Univ.in_universe_context_set * Safe_typing.exported_private_constant list
 
 val add_constant :
-  side_effect:'a Safe_typing.effect_entry -> in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t * 'a
+  side_effect:'a Safe_typing.effect_entry -> Id.t -> Safe_typing.global_declaration -> Constant.t * 'a
 val add_mind :
   Id.t -> Entries.mutual_inductive_entry -> MutInd.t
 
@@ -80,6 +80,8 @@ 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. *)
 
+val sections_are_opened : unit -> bool
+
 (** Interactive modules and module types *)
 
 val start_module : Id.t -> ModPath.t
diff --git a/library/lib.ml b/library/lib.ml
index 0d9efe2d5d..80b50b26d0 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -107,7 +107,6 @@ let segment_of_objects prefix =
 let initial_prefix = Nametab.{
   obj_dir = default_library;
   obj_mp  = ModPath.initial;
-  obj_sec = DirPath.empty;
 }
 
 type lib_state = {
@@ -132,10 +131,10 @@ let library_dp () =
 
 let cwd () = !lib_state.path_prefix.Nametab.obj_dir
 let current_mp () = !lib_state.path_prefix.Nametab.obj_mp
-let current_sections () = !lib_state.path_prefix.Nametab.obj_sec
+let current_sections () = Safe_typing.sections_of_safe_env (Global.safe_env())
 
-let sections_depth () = List.length (Names.DirPath.repr (current_sections ()))
-let sections_are_opened () = not (Names.DirPath.is_empty (current_sections ()))
+let sections_depth () = Section.depth (current_sections())
+let sections_are_opened = Global.sections_are_opened
 
 let cwd_except_section () =
   Libnames.pop_dirpath_n (sections_depth ()) (cwd ())
@@ -169,7 +168,6 @@ let pop_path_prefix () =
   let op = !lib_state.path_prefix in
   lib_state := { !lib_state
                  with path_prefix = Nametab.{ op with obj_dir = pop_dirpath op.obj_dir;
-                                                      obj_sec = pop_dirpath op.obj_sec;
                                             } }
 
 let find_entry_p p =
@@ -282,7 +280,7 @@ let current_mod_id () =
 
 let start_mod is_type export id mp fs =
   let dir = add_dirpath_suffix (!lib_state.path_prefix.Nametab.obj_dir) id in
-  let prefix = Nametab.{ obj_dir = dir; obj_mp = mp; obj_sec = Names.DirPath.empty } in
+  let prefix = Nametab.{ obj_dir = dir; obj_mp = mp; } in
   let exists =
     if is_type then Nametab.exists_cci (make_path id)
     else Nametab.exists_dir dir
@@ -330,9 +328,9 @@ let contents_after sp = let (after,_,_) = split_lib sp in after
 let start_compilation s mp =
   if !lib_state.comp_name != None then
     user_err Pp.(str "compilation unit is already started");
-  if not (Names.DirPath.is_empty (!lib_state.path_prefix.Nametab.obj_sec)) then
+  if Global.sections_are_opened () then (* XXX not sure if we need this check *)
     user_err Pp.(str "some sections are already opened");
-  let prefix = Nametab.{ obj_dir = s; obj_mp = mp; obj_sec = DirPath.empty } in
+  let prefix = Nametab.{ obj_dir = s; obj_mp = mp } in
   add_anonymous_entry (CompilingLibrary prefix);
   lib_state := { !lib_state with comp_name = Some s;
                                  path_prefix = prefix }
@@ -465,7 +463,7 @@ let open_section id =
   let () = Global.open_section () in
   let opp = !lib_state.path_prefix in
   let obj_dir = add_dirpath_suffix opp.Nametab.obj_dir id in
-  let prefix = Nametab.{ obj_dir; obj_mp = opp.obj_mp; obj_sec = add_dirpath_suffix opp.obj_sec id } in
+  let prefix = Nametab.{ obj_dir; obj_mp = opp.obj_mp; } in
   if Nametab.exists_dir obj_dir then
     user_err ~hdr:"open_section" (Id.print id ++ str " already exists.");
   let fs = Summary.freeze_summaries ~marshallable:false in
diff --git a/library/lib.mli b/library/lib.mli
index 59d77480e9..cef50a5f3b 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -95,6 +95,7 @@ val make_kn : Id.t -> KerName.t
 
 (** Are we inside an opened section *)
 val sections_are_opened : unit -> bool
+[@@ocaml.deprecated "Use Global.sections_are_opened"]
 val sections_depth : unit -> int
 
 (** Are we inside an opened module type *)
diff --git a/library/nametab.ml b/library/nametab.ml
index aed7d08ac1..8626ee1c59 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -18,12 +18,10 @@ open Globnames
 type object_prefix = {
   obj_dir : DirPath.t;
   obj_mp  : ModPath.t;
-  obj_sec : DirPath.t;
 }
 
 let eq_op op1 op2 =
   DirPath.equal op1.obj_dir op2.obj_dir &&
-  DirPath.equal op1.obj_sec op2.obj_sec &&
   ModPath.equal op1.obj_mp  op2.obj_mp
 
 (* to this type are mapped DirPath.t's in the nametab *)
diff --git a/library/nametab.mli b/library/nametab.mli
index 6ee22fc283..55458fe2c6 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -74,7 +74,6 @@ open Globnames
 type object_prefix = {
   obj_dir : DirPath.t;
   obj_mp  : ModPath.t;
-  obj_sec : DirPath.t;
 }
 
 val eq_op : object_prefix -> object_prefix -> bool
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 96a3d00dc2..be9259861a 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -380,7 +380,7 @@ let check_inside_module () =
     warn_extraction_inside_module ()
 
 let check_inside_section () =
-  if Lib.sections_are_opened () then
+  if Global.sections_are_opened () then
     err (str "You can't do that within a section." ++ fnl () ++
 	 str "Close it and try again.")
 
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 03921bca30..4cc6bc2052 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -213,7 +213,7 @@ let print_kn locals kn =
 let nametab_register_dir obj_mp =
   let id = mk_fake_top () in
   let obj_dir = DirPath.make [id] in
-  Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirModule { obj_dir; obj_mp; obj_sec = DirPath.empty }))
+  Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirModule { obj_dir; obj_mp; }))
 
 (** Nota: the [global_reference] we register in the nametab below
     might differ from internal ones, since we cannot recreate here
diff --git a/tactics/declare.ml b/tactics/declare.ml
index 3590146dfb..61321cd605 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -249,14 +249,13 @@ let is_unsafe_typing_flags () =
 
 let define_constant ~side_effect ~name cd =
   (* Logically define the constant and its subproofs, no libobject tampering *)
-  let in_section = Lib.sections_are_opened () in
   let export, decl, unsafe = match cd with
   | DefinitionEntry de ->
     (* We deal with side effects *)
     if not de.proof_entry_opaque then
       (* This globally defines the side-effects in the environment. *)
       let body, eff = Future.force de.proof_entry_body in
-      let body, export = Global.export_private_constants ~in_section (body, eff.Evd.seff_private) in
+      let body, export = Global.export_private_constants (body, eff.Evd.seff_private) in
       let export = get_roles export eff in
       let de = { de with proof_entry_body = Future.from_val (body, ()) } in
       let cd = Entries.DefinitionEntry (cast_proof_entry de) in
@@ -272,7 +271,7 @@ let define_constant ~side_effect ~name cd =
   | PrimitiveEntry e ->
     [], ConstantEntry (PureEntry, Entries.PrimitiveEntry e), false
   in
-  let kn, eff = Global.add_constant ~side_effect ~in_section name decl in
+  let kn, eff = Global.add_constant ~side_effect name decl in
   if unsafe || is_unsafe_typing_flags() then feedback_axiom();
   kn, eff, export
 
@@ -319,7 +318,7 @@ let declare_variable ~name ~kind d =
       (* The body should already have been forced upstream because it is a
          section-local definition, but it's not enforced by typing *)
       let (body, eff) = Future.force de.proof_entry_body in
-      let ((body, uctx), export) = Global.export_private_constants ~in_section:true (body, eff.Evd.seff_private) in
+      let ((body, uctx), export) = Global.export_private_constants (body, eff.Evd.seff_private) in
       let eff = get_roles export eff in
       let () = List.iter register_side_effect eff in
       let poly, univs = match de.proof_entry_universes with
@@ -585,7 +584,7 @@ let declare_univ_binders gr pl =
     Lib.add_anonymous_leaf (input_univ_names (QualifiedUniv l, univs))
 
 let do_universe ~poly l =
-  let in_section = Lib.sections_are_opened () in
+  let in_section = Global.sections_are_opened () in
   let () =
     if poly && not in_section then
       CErrors.user_err ~hdr:"Constraint"
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 5ba8b0ab3c..f9b73a59eb 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -287,7 +287,7 @@ let context ~poly l =
       name,b,t,impl)
       ctx
   in
-  if Lib.sections_are_opened ()
+  if Global.sections_are_opened ()
   then context_insection sigma ~poly ctx
   else context_nosection sigma ~poly ctx
 
diff --git a/vernac/comPrimitive.ml b/vernac/comPrimitive.ml
index 06fafddafb..b66ff876d3 100644
--- a/vernac/comPrimitive.ml
+++ b/vernac/comPrimitive.ml
@@ -9,7 +9,7 @@
 (************************************************************************)
 
 let do_primitive id prim typopt =
-  if Lib.sections_are_opened () then
+  if Global.sections_are_opened () then
     CErrors.user_err Pp.(str "Declaring a primitive is not allowed in sections.");
   if Dumpglob.dump () then Dumpglob.dump_definition id false "ax";
   let env = Global.env () in
diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml
index 58a7dff5fd..c7b68d18c2 100644
--- a/vernac/declaremods.ml
+++ b/vernac/declaremods.ml
@@ -211,7 +211,7 @@ let compute_visibility exists i =
 (** Iterate some function [iter_objects] on all components of a module *)
 
 let do_module exists iter_objects i obj_dir obj_mp sobjs kobjs =
-  let prefix = Nametab.{ obj_dir ; obj_mp; obj_sec = DirPath.empty } in
+  let prefix = Nametab.{ obj_dir ; obj_mp; } in
   let dirinfo = Nametab.GlobDirRef.DirModule prefix in
   consistency_checks exists obj_dir dirinfo;
   Nametab.push_dir (compute_visibility exists i) obj_dir dirinfo;
@@ -266,14 +266,14 @@ and load_objects i prefix objs =
 and load_include i ((sp,kn), aobjs) =
   let obj_dir = Libnames.dirpath sp in
   let obj_mp = KerName.modpath kn in
-  let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in
+  let prefix = Nametab.{ obj_dir; obj_mp; } in
   let o = expand_aobjs aobjs in
   load_objects i prefix o
 
 and load_keep i ((sp,kn),kobjs) =
   (* Invariant : seg isn't empty *)
   let obj_dir = dir_of_sp sp and obj_mp  = mp_of_kn kn in
-  let prefix = Nametab.{ obj_dir ; obj_mp; obj_sec = DirPath.empty } in
+  let prefix = Nametab.{ obj_dir ; obj_mp; } in
   let modobjs =
     try ModObjs.get obj_mp
     with Not_found -> assert false (* a substobjs should already be loaded *)
@@ -327,7 +327,7 @@ let rec open_object i (name, obj) =
   | KeepObject objs -> open_keep i (name, objs)
 
 and open_module i obj_dir obj_mp sobjs =
-  let prefix = Nametab.{ obj_dir ; obj_mp; obj_sec = DirPath.empty } in
+  let prefix = Nametab.{ obj_dir ; obj_mp; } in
   let dirinfo = Nametab.GlobDirRef.DirModule prefix in
   consistency_checks true obj_dir dirinfo;
   Nametab.push_dir (Nametab.Exactly i) obj_dir dirinfo;
@@ -353,7 +353,7 @@ and open_modtype i ((sp,kn),_) =
 and open_include i ((sp,kn), aobjs) =
   let obj_dir = Libnames.dirpath sp in
   let obj_mp = KerName.modpath kn in
-  let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in
+  let prefix = Nametab.{ obj_dir; obj_mp; } in
   let o = expand_aobjs aobjs in
   open_objects i prefix o
 
@@ -363,7 +363,7 @@ and open_export i mpl =
 
 and open_keep i ((sp,kn),kobjs) =
   let obj_dir = dir_of_sp sp and obj_mp = mp_of_kn kn in
-  let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in
+  let prefix = Nametab.{ obj_dir; obj_mp; } in
   open_objects i prefix kobjs
 
 let rec cache_object (name, obj) =
@@ -380,7 +380,7 @@ let rec cache_object (name, obj) =
 and cache_include ((sp,kn), aobjs) =
   let obj_dir = Libnames.dirpath sp in
   let obj_mp = KerName.modpath kn in
-  let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in
+  let prefix = Nametab.{ obj_dir; obj_mp; } in
   let o = expand_aobjs aobjs in
   load_objects 1 prefix o;
   open_objects 1 prefix o
diff --git a/vernac/locality.ml b/vernac/locality.ml
index f033d32874..5862f51b43 100644
--- a/vernac/locality.ml
+++ b/vernac/locality.ml
@@ -39,7 +39,7 @@ let enforce_locality_exp locality_flag discharge =
   match locality_flag, discharge with
   | Some b, NoDischarge -> Global (importability_of_bool b)
   | None, NoDischarge -> Global Declare.ImportDefaultBehavior
-  | None, DoDischarge when not (Lib.sections_are_opened ()) ->
+  | None, DoDischarge when not (Global.sections_are_opened ()) ->
      (* If a Let/Variable is defined outside a section, then we consider it as a local definition *)
      warn_local_declaration ();
      Global Declare.ImportNeedQualified
@@ -55,7 +55,7 @@ let enforce_locality locality_flag =
    Local in sections is the default, Local not in section forces non-export *)
 
 let make_section_locality =
-  function Some b -> b | None -> Lib.sections_are_opened ()
+  function Some b -> b | None -> Global.sections_are_opened ()
 
 let enforce_section_locality locality_flag =
   make_section_locality locality_flag
@@ -68,7 +68,7 @@ let enforce_section_locality locality_flag =
 
 let make_module_locality = function
   | Some false ->
-      if Lib.sections_are_opened () then
+      if Global.sections_are_opened () then
 	CErrors.user_err Pp.(str
 	  "This command does not support the Global option in sections.");
       false
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 4734ce1fb9..430cee62c2 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -810,14 +810,14 @@ let vernac_combined_scheme lid l =
  Indschemes.do_combined_scheme lid l
 
 let vernac_universe ~poly l =
-  if poly && not (Lib.sections_are_opened ()) then
+  if poly && not (Global.sections_are_opened ()) then
     user_err ~hdr:"vernac_universe"
 		 (str"Polymorphic universes can only be declared inside sections, " ++
 		  str "use Monomorphic Universe instead");
   Declare.do_universe ~poly l
 
 let vernac_constraint ~poly l =
-  if poly && not (Lib.sections_are_opened ()) then
+  if poly && not (Global.sections_are_opened ()) then
     user_err ~hdr:"vernac_constraint"
 		 (str"Polymorphic universe constraints can only be declared"
 		  ++ str " inside sections, use Monomorphic Constraint instead");
@@ -837,7 +837,7 @@ let vernac_import export refl =
 let vernac_declare_module export {loc;v=id} binders_ast mty_ast =
   (* We check the state of the system (in section, in module type)
      and what module information is supplied *)
-  if Lib.sections_are_opened () then
+  if Global.sections_are_opened () then
     user_err Pp.(str "Modules and Module Types are not allowed inside sections.");
   let binders_ast = List.map
    (fun (export,idl,ty) ->
@@ -852,7 +852,7 @@ let vernac_declare_module export {loc;v=id} binders_ast mty_ast =
 let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mty_ast_o mexpr_ast_l =
   (* We check the state of the system (in section, in module type)
      and what module information is supplied *)
-  if Lib.sections_are_opened () then
+  if Global.sections_are_opened () then
     user_err Pp.(str "Modules and Module Types are not allowed inside sections.");
   match mexpr_ast_l with
     | [] ->
@@ -893,7 +893,7 @@ let vernac_end_module export {loc;v=id} =
   Option.iter (fun export -> vernac_import export [qualid_of_ident ?loc id]) export
 
 let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l =
-  if Lib.sections_are_opened () then
+  if Global.sections_are_opened () then
     user_err Pp.(str "Modules and Module Types are not allowed inside sections.");
 
   match mty_ast_l with
@@ -969,7 +969,7 @@ let warn_require_in_section =
     (fun () -> strbrk "Use of “Require” inside a section is deprecated.")
 
 let vernac_require from import qidl =
-  if Lib.sections_are_opened () then warn_require_in_section ();
+  if Global.sections_are_opened () then warn_require_in_section ();
   let root = match from with
   | None -> None
   | Some from ->
@@ -2098,7 +2098,7 @@ let vernac_register qid r =
   | RegisterCoqlib n ->
     let ns, id = Libnames.repr_qualid n in
     if DirPath.equal (dirpath_of_string "kernel") ns then begin
-      if Lib.sections_are_opened () then
+      if Global.sections_are_opened () then
         user_err Pp.(str "Registering a kernel type is not allowed in sections");
       let pind = match Id.to_string id with
         | "ind_bool" -> CPrimitives.PIT_bool