diff options
| author | Emilio Jesus Gallego Arias | 2018-10-26 10:24:18 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-26 13:59:23 +0200 |
| commit | dccaed2452e544308b46f0c73ffd4f542ef4c8c6 (patch) | |
| tree | 3f95a7253acf3f06682bd036bc6f647c0121a085 /library/libnames.mli | |
| parent | 27266c1f79e565a6a19da4c79fc1ce83f748e31c (diff) | |
[libobject] Move object_name next to object definition.
`object_name` is a particular choice of the implementation of
`Liboject`, thus it makes sense to tie it to that particular module.
This may prove useful in the future as we may want to modify object
naming.
Diffstat (limited to 'library/libnames.mli')
| -rw-r--r-- | library/libnames.mli | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/library/libnames.mli b/library/libnames.mli index 447eecbb5c..9d75ec6e40 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -88,12 +88,6 @@ val qualid_is_ident : qualid -> bool val qualid_path : qualid -> DirPath.t val qualid_basename : qualid -> Id.t -(** Both names are passed to objects: a "semantic" [kernel_name], which - can be substituted and a "syntactic" [full_path] which can be printed -*) - -type object_name = full_path * KerName.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 @@ -116,8 +110,6 @@ type object_prefix = { val eq_op : object_prefix -> object_prefix -> bool -val make_oname : object_prefix -> Id.t -> object_name - (** to this type are mapped [DirPath.t]'s in the nametab *) type global_dir_reference = | DirOpenModule of object_prefix |