diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/lib.ml | 4 | ||||
| -rw-r--r-- | library/lib.mli | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/library/lib.ml b/library/lib.ml index bc01c4776d..ca054c8d6c 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -624,12 +624,12 @@ let reset_initial () = (* Misc *) -let library_part ref = +let remove_section_part ref = let sp = Nametab.sp_of_global ref in let dir,_ = repr_path sp in match ref with | VarRef id -> - anomaly "library_part not supported on local variables" + anomaly "remove_section_part not supported on local variables" | _ -> if is_dirpath_prefix_of dir (cwd ()) then (* Not yet (fully) discharged *) diff --git a/library/lib.mli b/library/lib.mli index 500d01e2cd..6552cda6a8 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -122,7 +122,7 @@ val end_compilation : dir_path -> object_prefix * library_segment val library_dp : unit -> dir_path (* Extract the library part of a name even if in a section *) -val library_part : global_reference -> dir_path +val remove_section_part : global_reference -> dir_path (*s Sections *) |