diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/lib.ml | 6 | ||||
| -rw-r--r-- | library/lib.mli | 1 |
2 files changed, 4 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 ()) 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 *) |