aboutsummaryrefslogtreecommitdiff
path: root/library/lib.ml
diff options
context:
space:
mode:
authorGaëtan Gilbert2019-10-13 16:32:15 +0200
committerGaëtan Gilbert2019-10-14 10:24:26 +0200
commitc3479eceb8e07b37570a80bca9937e3520c61024 (patch)
tree136a1773ad9b1bd1cdecd3db26ca0cc64f4516cf /library/lib.ml
parent26e8b5a545bcf2209d56494ccf4afe143f761fd7 (diff)
Use kernel info from Global for Lib.sections_{depth,are_opened}
Diffstat (limited to 'library/lib.ml')
-rw-r--r--library/lib.ml6
1 files changed, 3 insertions, 3 deletions
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 ())