[nametab] Move `object_prefix` to `Nametab`.

We move `object_prefix` to `Nametab`. This highlights the coupling of
`Lib` and `Nametab` wrt naming.

This also thins `Libname`, which IMHO is a good thing as we are
talking about "local, internal" naming here.

1 files changed, 0 insertions, 22 deletions

diff --git a/library/libnames.mli b/library/libnames.mli
index 56368fd08c..9960603cbb 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -88,28 +88,6 @@ val qualid_is_ident : qualid -> bool
 val qualid_path : qualid -> DirPath.t
 val qualid_basename : qualid -> Id.t
 
-(** Object prefix morally contains the "prefix" naming of an object to
-   be stored by [library], where [obj_dir] is the "absolute" path,
-   [obj_mp] is the current "module" prefix and [obj_sec] is the
-   "section" prefix.
-
-    Thus, for an object living inside [Module A. Section B.] the
-   prefix would be:
-
-    [ { obj_dir = "A.B"; obj_mp = "A"; obj_sec = "B" } ]
-
-    Note that both [obj_dir] and [obj_sec] are "paths" that is to say,
-   as opposed to [obj_mp] which is a single module name.
-
- *)
-type object_prefix = {
-  obj_dir : DirPath.t;
-  obj_mp  : ModPath.t;
-  obj_sec : DirPath.t;
-}
-
-val eq_op : object_prefix -> object_prefix -> bool
-
 (** {6 ... } *)
 
 (** some preset paths *)