From c408e819ce39b27f0842c84b1b24c585ac5b6086 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 22 Mar 2017 01:14:50 +0100 Subject: [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`. --- library/libnames.mli | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) (limited to 'library/libnames.mli') 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 -- cgit v1.2.3