From c3479eceb8e07b37570a80bca9937e3520c61024 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sun, 13 Oct 2019 16:32:15 +0200
Subject: Use kernel info from Global for Lib.sections_{depth,are_opened}

---
 library/lib.ml  | 6 +++---
 library/lib.mli | 1 +
 2 files changed, 4 insertions(+), 3 deletions(-)

(limited to 'library')

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 *)
-- 
cgit v1.2.3