Merge PR #8871: [library] Move Nametab/Lib specific-names to Nametab

9 files changed, 136 insertions, 127 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index e01a99f731..d20775a0d7 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -139,7 +139,7 @@ let expand_sobjs (_,aobjs) = expand_aobjs aobjs
      Module M:SIG. ... End M. have the keep list empty.
 *)
 
-type module_objects = object_prefix * Lib.lib_objects * Lib.lib_objects
+type module_objects = Nametab.object_prefix * Lib.lib_objects * Lib.lib_objects
 
 module ModObjs :
  sig
@@ -185,7 +185,7 @@ let consistency_checks exists dir dirinfo =
         user_err ~hdr:"consistency_checks"
           (DirPath.print dir ++ str " should already exist!")
     in
-    assert (eq_global_dir_reference globref dirinfo)
+    assert (Nametab.GlobDirRef.equal globref dirinfo)
   else
     if Nametab.exists_dir dir then
       user_err ~hdr:"consistency_checks"
@@ -197,8 +197,8 @@ let compute_visibility exists i =
 (** Iterate some function [iter_objects] on all components of a module *)
 
 let do_module exists iter_objects i obj_dir obj_mp sobjs kobjs =
-  let prefix = { obj_dir ; obj_mp; obj_sec = DirPath.empty } in
-  let dirinfo = DirModule prefix in
+  let prefix = Nametab.{ obj_dir ; obj_mp; obj_sec = DirPath.empty } in
+  let dirinfo = Nametab.GlobDirRef.DirModule prefix in
   consistency_checks exists obj_dir dirinfo;
   Nametab.push_dir (compute_visibility exists i) obj_dir dirinfo;
   ModSubstObjs.set obj_mp sobjs;
@@ -239,19 +239,19 @@ let cache_keep _ = anomaly (Pp.str "This module should not be cached!")
 let load_keep i ((sp,kn),kobjs) =
   (* Invariant : seg isn't empty *)
   let obj_dir = dir_of_sp sp and obj_mp  = mp_of_kn kn in
-  let prefix = { obj_dir ; obj_mp; obj_sec = DirPath.empty } in
+  let prefix = Nametab.{ obj_dir ; obj_mp; obj_sec = DirPath.empty } in
   let prefix',sobjs,kobjs0 =
     try ModObjs.get obj_mp
     with Not_found -> assert false (* a substobjs should already be loaded *)
   in
-  assert (eq_op prefix' prefix);
+  assert Nametab.(eq_op prefix' prefix);
   assert (List.is_empty kobjs0);
   ModObjs.set obj_mp (prefix,sobjs,kobjs);
   Lib.load_objects i prefix kobjs
 
 let open_keep i ((sp,kn),kobjs) =
   let obj_dir = dir_of_sp sp and obj_mp = mp_of_kn kn in
-  let prefix = { obj_dir; obj_mp; obj_sec = DirPath.empty } in
+  let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in
   Lib.open_objects i prefix kobjs
 
 let in_modkeep : Lib.lib_objects -> obj =
@@ -302,7 +302,7 @@ let (in_modtype : substitutive_objects -> obj),
 let do_include do_load do_open i ((sp,kn),aobjs) =
   let obj_dir = Libnames.dirpath sp in
   let obj_mp = KerName.modpath kn in
-  let prefix = { obj_dir; obj_mp; obj_sec = DirPath.empty } in
+  let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in
   let o = expand_aobjs aobjs in
   if do_load then Lib.load_objects i prefix o;
   if do_open then Lib.open_objects i prefix o
@@ -605,7 +605,7 @@ let start_module interp_modast export id args res fs =
   let () = Global.push_context_set true cst in
   openmod_info := { cur_typ = res_entry_o; cur_typs = subtyps };
   let prefix = Lib.start_module export id mp fs in
-  Nametab.push_dir (Nametab.Until 1) (prefix.obj_dir) (DirOpenModule prefix);
+  Nametab.(push_dir (Until 1) (prefix.obj_dir) (GlobDirRef.DirOpenModule prefix));
   mp
 
 let end_module () =
@@ -723,7 +723,7 @@ let start_modtype interp_modast id args mtys fs =
   let () = Global.push_context_set true cst in
   openmodtype_info := sub_mty_l;
   let prefix = Lib.start_modtype id mp fs in
-  Nametab.push_dir (Nametab.Until 1) (prefix.obj_dir) (DirOpenModtype prefix);
+  Nametab.(push_dir (Until 1) (prefix.obj_dir) (GlobDirRef.DirOpenModtype prefix));
   mp
 
 let end_modtype () =
@@ -977,7 +977,7 @@ let iter_all_segments f =
     | "INCLUDE" ->
       let objs = expand_aobjs (out_include obj) in
       List.iter (apply_obj prefix) objs
-    | _ -> f (make_oname prefix id) obj
+    | _ -> f (Lib.make_oname prefix id) obj
   in
   let apply_mod_obj _ (prefix,substobjs,keepobjs) =
     List.iter (apply_obj prefix) substobjs;
diff --git a/library/lib.ml b/library/lib.ml
index 1acc8fd8fd..690a4fd53d 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -22,11 +22,16 @@ module NamedDecl = Context.Named.Declaration
 type is_type = bool (* Module Type or just Module *)
 type export = bool option (* None for a Module Type *)
 
+(* let make_oname (dirpath,(mp,dir)) id = *)
+let make_oname Nametab.{ obj_dir; obj_mp } id =
+  Names.(make_path obj_dir id, KerName.make obj_mp (Label.of_id id))
+
+(* let make_oname (dirpath,(mp,dir)) id = *)
 type node =
   | Leaf of obj
-  | CompilingLibrary of object_prefix
-  | OpenedModule of is_type * export * object_prefix * Summary.frozen
-  | OpenedSection of object_prefix * Summary.frozen
+  | CompilingLibrary of Nametab.object_prefix
+  | OpenedModule of is_type * export * Nametab.object_prefix * Summary.frozen
+  | OpenedSection of Nametab.object_prefix * Summary.frozen
 
 type library_entry = object_name * node
 
@@ -89,7 +94,7 @@ let segment_of_objects prefix =
    sections, but on the contrary there are many constructions of section
    paths based on the library path. *)
 
-let initial_prefix = {
+let initial_prefix = Nametab.{
   obj_dir = default_library;
   obj_mp  = ModPath.initial;
   obj_sec = DirPath.empty;
@@ -98,7 +103,7 @@ let initial_prefix = {
 type lib_state = {
   comp_name   : DirPath.t option;
   lib_stk     : library_segment;
-  path_prefix : object_prefix;
+  path_prefix : Nametab.object_prefix;
 }
 
 let initial_lib_state = {
@@ -115,9 +120,9 @@ let library_dp () =
 (* [path_prefix] is a pair of absolute dirpath and a pair of current
    module path and relative section path *)
 
-let cwd () = !lib_state.path_prefix.obj_dir
-let current_mp () = !lib_state.path_prefix.obj_mp
-let current_sections () = !lib_state.path_prefix.obj_sec
+let cwd () = !lib_state.path_prefix.Nametab.obj_dir
+let current_mp () = !lib_state.path_prefix.Nametab.obj_mp
+let current_sections () = !lib_state.path_prefix.Nametab.obj_sec
 
 let sections_depth () = List.length (Names.DirPath.repr (current_sections ()))
 let sections_are_opened () = not (Names.DirPath.is_empty (current_sections ()))
@@ -138,7 +143,7 @@ let make_kn id =
   let mp = current_mp () in
   Names.KerName.make mp (Names.Label.of_id id)
 
-let make_oname id = Libobject.make_oname !lib_state.path_prefix id
+let make_foname id = make_oname !lib_state.path_prefix id
 
 let recalc_path_prefix () =
   let rec recalc = function
@@ -153,9 +158,9 @@ let recalc_path_prefix () =
 let pop_path_prefix () =
   let op = !lib_state.path_prefix in
   lib_state := { !lib_state
-                 with path_prefix = { op with obj_dir = pop_dirpath op.obj_dir;
-                                              obj_sec = pop_dirpath op.obj_sec;
-                                    } }
+                 with path_prefix = Nametab.{ op with obj_dir = pop_dirpath op.obj_dir;
+                                                      obj_sec = pop_dirpath op.obj_sec;
+                                            } }
 
 let find_entry_p p =
   let rec find = function
@@ -214,24 +219,24 @@ let anonymous_id =
   fun () -> incr n; Names.Id.of_string ("_" ^ (string_of_int !n))
 
 let add_anonymous_entry node =
-  add_entry (make_oname (anonymous_id ())) node
+  add_entry (make_foname (anonymous_id ())) node
 
 let add_leaf id obj =
   if ModPath.equal (current_mp ()) ModPath.initial then
     user_err Pp.(str "No session module started (use -top dir)");
-  let oname = make_oname id in
+  let oname = make_foname id in
   cache_object (oname,obj);
   add_entry oname (Leaf obj);
   oname
 
 let add_discharged_leaf id obj =
-  let oname = make_oname id in
+  let oname = make_foname id in
   let newobj = rebuild_object obj in
   cache_object (oname,newobj);
   add_entry oname (Leaf newobj)
 
 let add_leaves id objs =
-  let oname = make_oname id in
+  let oname = make_foname id in
   let add_obj obj =
     add_entry oname (Leaf obj);
     load_object 1 (oname,obj)
@@ -241,7 +246,7 @@ let add_leaves id objs =
 
 let add_anonymous_leaf ?(cache_first = true) obj =
   let id = anonymous_id () in
-  let oname = make_oname id in
+  let oname = make_foname id in
   if cache_first then begin
     cache_object (oname,obj);
     add_entry oname (Leaf obj)
@@ -269,15 +274,15 @@ let current_mod_id () =
 
 
 let start_mod is_type export id mp fs =
-  let dir = add_dirpath_suffix (!lib_state.path_prefix.obj_dir) id in
-  let prefix = { obj_dir = dir; obj_mp = mp; obj_sec = Names.DirPath.empty } in
+  let dir = add_dirpath_suffix (!lib_state.path_prefix.Nametab.obj_dir) id in
+  let prefix = Nametab.{ obj_dir = dir; obj_mp = mp; obj_sec = Names.DirPath.empty } in
   let exists =
     if is_type then Nametab.exists_cci (make_path id)
     else Nametab.exists_module dir
   in
   if exists then
     user_err ~hdr:"open_module" (Id.print id ++ str " already exists");
-  add_entry (make_oname id) (OpenedModule (is_type,export,prefix,fs));
+  add_entry (make_foname id) (OpenedModule (is_type,export,prefix,fs));
   lib_state := { !lib_state with path_prefix = prefix} ;
   prefix
 
@@ -318,9 +323,9 @@ let contents_after sp = let (after,_,_) = split_lib sp in after
 let start_compilation s mp =
   if !lib_state.comp_name != None then
     user_err Pp.(str "compilation unit is already started");
-  if not (Names.DirPath.is_empty (!lib_state.path_prefix.obj_sec)) then
+  if not (Names.DirPath.is_empty (!lib_state.path_prefix.Nametab.obj_sec)) then
     user_err Pp.(str "some sections are already opened");
-  let prefix = Libnames.{ obj_dir = s; obj_mp = mp; obj_sec = DirPath.empty } in
+  let prefix = Nametab.{ obj_dir = s; obj_mp = mp; obj_sec = DirPath.empty } in
   add_anonymous_entry (CompilingLibrary prefix);
   lib_state := { !lib_state with comp_name = Some s;
                                  path_prefix = prefix }
@@ -544,14 +549,14 @@ let is_in_section ref =
 (* Sections. *)
 let open_section id =
   let opp = !lib_state.path_prefix in
-  let obj_dir = add_dirpath_suffix opp.obj_dir id in
-  let prefix = { obj_dir; obj_mp = opp.obj_mp; obj_sec = add_dirpath_suffix opp.obj_sec id } in
+  let obj_dir = add_dirpath_suffix opp.Nametab.obj_dir id in
+  let prefix = Nametab.{ obj_dir; obj_mp = opp.obj_mp; obj_sec = add_dirpath_suffix opp.obj_sec id } in
   if Nametab.exists_section obj_dir then
     user_err ~hdr:"open_section" (Id.print id ++ str " already exists.");
   let fs = Summary.freeze_summaries ~marshallable:`No in
-  add_entry (make_oname id) (OpenedSection (prefix, fs));
+  add_entry (make_foname id) (OpenedSection (prefix, fs));
   (*Pushed for the lifetime of the section: removed by unfrozing the summary*)
-  Nametab.push_dir (Nametab.Until 1) obj_dir (DirOpenSection prefix);
+  Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirOpenSection prefix));
   lib_state := { !lib_state with path_prefix = prefix };
   add_section ()
 
@@ -611,7 +616,7 @@ let init () =
 (* Misc *)
 
 let mp_of_global = function
-  | VarRef id -> !lib_state.path_prefix.obj_mp
+  | VarRef id -> !lib_state.path_prefix.Nametab.obj_mp
   | ConstRef cst -> Names.Constant.modpath cst
   | IndRef ind -> Names.ind_modpath ind
   | ConstructRef constr -> Names.constr_modpath constr
diff --git a/library/lib.mli b/library/lib.mli
index c6c6a307d4..d1b4977dd5 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -19,11 +19,13 @@ open Names
 type is_type = bool (* Module Type or just Module *)
 type export = bool option (* None for a Module Type *)
 
+val make_oname : Nametab.object_prefix -> Names.Id.t -> Libobject.object_name
+
 type node =
   | Leaf of Libobject.obj
-  | CompilingLibrary of Libnames.object_prefix
-  | OpenedModule of is_type * export * Libnames.object_prefix * Summary.frozen
-  | OpenedSection of Libnames.object_prefix * Summary.frozen
+  | CompilingLibrary of Nametab.object_prefix
+  | OpenedModule of is_type * export * Nametab.object_prefix * Summary.frozen
+  | OpenedSection of Nametab.object_prefix * Summary.frozen
 
 type library_segment = (Libobject.object_name * node) list
 
@@ -31,10 +33,10 @@ type lib_objects = (Id.t * Libobject.obj) list
 
 (** {6 Object iteration functions. } *)
 
-val open_objects : int -> Libnames.object_prefix -> lib_objects -> unit
-val load_objects : int -> Libnames.object_prefix -> lib_objects -> unit
+val open_objects : int -> Nametab.object_prefix -> lib_objects -> unit
+val load_objects : int -> Nametab.object_prefix -> lib_objects -> unit
 val subst_objects : Mod_subst.substitution -> lib_objects -> lib_objects
-(*val load_and_subst_objects : int -> Libnames.object_prefix -> Mod_subst.substitution -> lib_objects -> lib_objects*)
+(*val load_and_subst_objects : int -> Libnames.Nametab.object_prefix -> Mod_subst.substitution -> lib_objects -> lib_objects*)
 
 (** [classify_segment seg] verifies that there are no OpenedThings,
    clears ClosedSections and FrozenStates and divides Leafs according
@@ -46,7 +48,7 @@ val classify_segment :
 
 (** [segment_of_objects prefix objs] forms a list of Leafs *)
 val segment_of_objects :
-  Libnames.object_prefix -> lib_objects -> library_segment
+  Nametab.object_prefix -> lib_objects -> library_segment
 
 
 (** {6 ... } *)
@@ -105,20 +107,20 @@ val find_opening_node : Id.t -> node
 
 val start_module :
   export -> module_ident -> ModPath.t ->
-  Summary.frozen -> Libnames.object_prefix
+  Summary.frozen -> Nametab.object_prefix
 
 val start_modtype :
   module_ident -> ModPath.t ->
-  Summary.frozen -> Libnames.object_prefix
+  Summary.frozen -> Nametab.object_prefix
 
 val end_module :
   unit ->
-  Libobject.object_name * Libnames.object_prefix *
+  Libobject.object_name * Nametab.object_prefix *
     Summary.frozen * library_segment
 
 val end_modtype :
   unit ->
-  Libobject.object_name * Libnames.object_prefix *
+  Libobject.object_name * Nametab.object_prefix *
     Summary.frozen * library_segment
 
 (** {6 Compilation units } *)
@@ -126,7 +128,7 @@ val end_modtype :
 val start_compilation : DirPath.t -> ModPath.t -> unit
 val end_compilation_checks : DirPath.t -> Libobject.object_name
 val end_compilation :
-  Libobject.object_name-> Libnames.object_prefix * library_segment
+  Libobject.object_name-> Nametab.object_prefix * library_segment
 
 (** The function [library_dp] returns the [DirPath.t] of the current
    compiling library (or [default_library]) *)
diff --git a/library/libnames.ml b/library/libnames.ml
index f6fc5ed4b7..87c4de42e8 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -162,31 +162,6 @@ let qualid_basename qid =
 let qualid_path qid =
   qid.CAst.v.dirpath
 
-type object_prefix = {
-  obj_dir : DirPath.t;
-  obj_mp  : ModPath.t;
-  obj_sec : DirPath.t;
-}
-
-(* to this type are mapped DirPath.t's in the nametab *)
-type global_dir_reference =
-  | DirOpenModule of object_prefix
-  | DirOpenModtype of object_prefix
-  | DirOpenSection of object_prefix
-  | DirModule of object_prefix
-
-let eq_op op1 op2 =
-  DirPath.equal op1.obj_dir op2.obj_dir &&
-  DirPath.equal op1.obj_sec op2.obj_sec &&
-  ModPath.equal op1.obj_mp  op2.obj_mp
-
-let eq_global_dir_reference r1 r2 = match r1, r2 with
-| DirOpenModule op1, DirOpenModule op2 -> eq_op op1 op2
-| DirOpenModtype op1, DirOpenModtype op2 -> eq_op op1 op2
-| DirOpenSection op1, DirOpenSection op2 -> eq_op op1 op2
-| DirModule op1, DirModule op2 -> eq_op op1 op2
-| _ -> false
-
 (* Default paths *)
 let default_library = Names.DirPath.initial (* = ["Top"] *)
 
diff --git a/library/libnames.mli b/library/libnames.mli
index 9d75ec6e40..9960603cbb 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -88,38 +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
-
-(** to this type are mapped [DirPath.t]'s in the nametab *)
-type global_dir_reference =
-  | DirOpenModule of object_prefix
-  | DirOpenModtype of object_prefix
-  | DirOpenSection of object_prefix
-  | DirModule of object_prefix
-
-val eq_global_dir_reference : 
-  global_dir_reference -> global_dir_reference -> bool
-
 (** {6 ... } *)
 
 (** some preset paths *)
diff --git a/library/libobject.ml b/library/libobject.ml
index 43934304c2..c153e9a09a 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -8,7 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Libnames
 open Pp
 
 module Dyn = Dyn.Make ()
@@ -18,10 +17,6 @@ type 'a substitutivity =
 
 type object_name = Libnames.full_path * Names.KerName.t
 
-(* let make_oname (dirpath,(mp,dir)) id = *)
-let make_oname { obj_dir; obj_mp } id =
-  Names.(make_path obj_dir id, KerName.make obj_mp (Label.of_id id))
-
 type 'a object_declaration = {
   object_name : string;
   cache_function : object_name * 'a -> unit;
diff --git a/library/libobject.mli b/library/libobject.mli
index c53537e654..32ffc5b79e 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -71,7 +71,6 @@ type 'a substitutivity =
 *)
 
 type object_name = full_path * Names.KerName.t
-val make_oname : object_prefix -> Names.Id.t -> object_name
 
 type 'a object_declaration = {
   object_name : string;
diff --git a/library/nametab.ml b/library/nametab.ml
index 029d850504..e29c7b2960 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -15,6 +15,39 @@ open Names
 open Libnames
 open Globnames
 
+type object_prefix = {
+  obj_dir : DirPath.t;
+  obj_mp  : ModPath.t;
+  obj_sec : DirPath.t;
+}
+
+let eq_op op1 op2 =
+  DirPath.equal op1.obj_dir op2.obj_dir &&
+  DirPath.equal op1.obj_sec op2.obj_sec &&
+  ModPath.equal op1.obj_mp  op2.obj_mp
+
+(* to this type are mapped DirPath.t's in the nametab *)
+module GlobDirRef = struct
+  type t =
+    | DirOpenModule of object_prefix
+    | DirOpenModtype of object_prefix
+    | DirOpenSection of object_prefix
+    | DirModule of object_prefix
+
+  let equal r1 r2 = match r1, r2 with
+    | DirOpenModule op1, DirOpenModule op2 -> eq_op op1 op2
+    | DirOpenModtype op1, DirOpenModtype op2 -> eq_op op1 op2
+    | DirOpenSection op1, DirOpenSection op2 -> eq_op op1 op2
+    | DirModule op1, DirModule op2 -> eq_op op1 op2
+    | _ -> false
+
+end
+
+type global_dir_reference = GlobDirRef.t
+[@@ocaml.deprecated "Use [GlobDirRef.t]"]
+
+let eq_global_dir_reference = GlobDirRef.equal
+[@@ocaml.deprecated "Use [GlobDirRef.equal]"]
 
 exception GlobalizationError of qualid
 
@@ -307,13 +340,7 @@ struct
     | id :: l -> (id, l)
 end
 
-module GlobDir =
-struct
-  type t = global_dir_reference
-  let equal = eq_global_dir_reference
-end
-
-module DirTab = Make(DirPath')(GlobDir)
+module DirTab = Make(DirPath')(GlobDirRef)
 
 (* If we have a (closed) module M having a submodule N, than N does not
    have the entry in [the_dirtab]. *)
@@ -402,7 +429,7 @@ let push_modtype vis sp kn =
 let push_dir vis dir dir_ref =
   the_dirtab := DirTab.push vis dir dir_ref !the_dirtab;
   match dir_ref with
-  | DirModule { obj_mp; _ } -> the_modrevtab := MPmap.add obj_mp dir !the_modrevtab
+  | GlobDirRef.DirModule { obj_mp; _ } -> the_modrevtab := MPmap.add obj_mp dir !the_modrevtab
   | _ -> ()
 
 (* This is for global universe names *)
@@ -436,17 +463,17 @@ let locate_dir qid = DirTab.locate qid !the_dirtab
 
 let locate_module qid =
   match locate_dir qid with
-    | DirModule { obj_mp ; _} -> obj_mp
+    | GlobDirRef.DirModule { obj_mp ; _} -> obj_mp
     | _ -> raise Not_found
 
 let full_name_module qid =
   match locate_dir qid with
-    | DirModule { obj_dir ; _} -> obj_dir
+    | GlobDirRef.DirModule { obj_dir ; _} -> obj_dir
     | _ -> raise Not_found
 
 let locate_section qid =
   match locate_dir qid with
-    | DirOpenSection { obj_dir; _ } -> obj_dir
+    | GlobDirRef.DirOpenSection { obj_dir; _ } -> obj_dir
     | _ -> raise Not_found
 
 let locate_all qid =
diff --git a/library/nametab.mli b/library/nametab.mli
index 1e479b200b..24af07619d 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -57,6 +57,44 @@ open Globnames
 
 *)
 
+(** 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
+
+(** to this type are mapped [DirPath.t]'s in the nametab *)
+module GlobDirRef : sig
+  type t =
+    | DirOpenModule of object_prefix
+    | DirOpenModtype of object_prefix
+    | DirOpenSection of object_prefix
+    | DirModule of object_prefix
+  val equal : t -> t -> bool
+end
+
+type global_dir_reference = GlobDirRef.t
+[@@ocaml.deprecated "Use [GlobDirRef.t]"]
+
+val eq_global_dir_reference :
+  GlobDirRef.t -> GlobDirRef.t -> bool
+[@@ocaml.deprecated "Use [GlobDirRef.equal]"]
 
 exception GlobalizationError of qualid
 
@@ -79,7 +117,7 @@ val map_visibility : (int -> int) -> visibility -> visibility
 
 val push : visibility -> full_path -> GlobRef.t -> unit
 val push_modtype : visibility -> full_path -> ModPath.t -> unit
-val push_dir : visibility -> DirPath.t -> global_dir_reference -> unit
+val push_dir : visibility -> DirPath.t -> GlobDirRef.t -> unit
 val push_syndef : visibility -> full_path -> syndef_name -> unit
 
 type universe_id = DirPath.t * int
@@ -98,7 +136,7 @@ val locate_extended : qualid -> extended_global_reference
 val locate_constant : qualid -> Constant.t
 val locate_syndef : qualid -> syndef_name
 val locate_modtype : qualid -> ModPath.t
-val locate_dir : qualid -> global_dir_reference
+val locate_dir : qualid -> GlobDirRef.t
 val locate_module : qualid -> ModPath.t
 val locate_section : qualid -> DirPath.t
 val locate_universe : qualid -> universe_id
@@ -115,7 +153,7 @@ val global_inductive : qualid -> inductive
 
 val locate_all : qualid -> GlobRef.t list
 val locate_extended_all : qualid -> extended_global_reference list
-val locate_extended_all_dir : qualid -> global_dir_reference list
+val locate_extended_all_dir : qualid -> GlobDirRef.t list
 val locate_extended_all_modtype : qualid -> ModPath.t list
 
 (** Experimental completion support, API is _unstable_ *)