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

10 files changed, 23 insertions, 17 deletions

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/lib.ml b/library/lib.ml
index 0d9efe2d5d..3f162682c3 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -132,10 +132,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 ())
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/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/tactics/declare.ml b/tactics/declare.ml
index c7c0766587..61321cd605 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -584,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/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