aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/libnames.mli
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-03-22 01:14:50 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-11-29 14:59:29 +0100
commitc408e819ce39b27f0842c84b1b24c585ac5b6086 (patch)
treea3dac227a23d098e70c7d74bd719f93f3cc6724c /library/libnames.mli
parent437f20f0a1c2717cd7baae52e2ab20750dd9d4fb (diff)
[lib] [api] Introduce record for `object_prefix`
This is a minor cleanup adding a record in a try to structure the state living in `Lib`.
Diffstat (limited to 'library/libnames.mli')
-rw-r--r--library/libnames.mli20
1 files changed, 19 insertions, 1 deletions
diff --git a/library/libnames.mli b/library/libnames.mli
index ed01163ee..71f542240 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