Use kernel info from Global for Lib.sections_{depth,are_opened}

4 files changed, 12 insertions, 12 deletions

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/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