Merge PR #6244: [lib] [api] Introduce record for `object_prefix`

1 files changed, 19 insertions, 1 deletions

diff --git a/library/libnames.mli b/library/libnames.mli
index ed01163ee7..71f5422404 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -94,7 +94,25 @@ val qualid_of_ident : Id.t -> qualid
 
 type object_name = full_path * KerName.t
 
-type object_prefix = DirPath.t * (ModPath.t * DirPath.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