[nametab] Move `object_prefix` to `Nametab`.

We move `object_prefix` to `Nametab`. This highlights the coupling of
`Lib` and `Nametab` wrt naming.

This also thins `Libname`, which IMHO is a good thing as we are
talking about "local, internal" naming here.

11 files changed, 93 insertions, 90 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index f4edbe36bb..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
@@ -197,7 +197,7 @@ 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 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;
@@ -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
@@ -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 762a2e0567..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,12 +549,12 @@ 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 (Until 1) obj_dir (GlobDirRef.DirOpenSection prefix));
   lib_state := { !lib_state with path_prefix = prefix };
@@ -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 d2c96d4163..87c4de42e8 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -162,17 +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;
-}
-
-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
-
 (* Default paths *)
 let default_library = Names.DirPath.initial (* = ["Top"] *)
 
diff --git a/library/libnames.mli b/library/libnames.mli
index 56368fd08c..9960603cbb 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -88,28 +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
-
 (** {6 ... } *)
 
 (** some preset paths *)
diff --git a/library/libobject.ml b/library/libobject.ml
index ea19fbb90b..c0766e6a91 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 7f94357a8b..4649c2ceb1 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -15,6 +15,17 @@ 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 =
diff --git a/library/nametab.mli b/library/nametab.mli
index b71bc77cbb..bc5fe8527f 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -57,6 +57,28 @@ 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 =
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 96720e84d6..5c13503560 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -367,7 +367,9 @@ let pr_located_qualid = function
   | Syntactic kn ->
       str "Notation" ++ spc () ++ pr_path (Nametab.path_of_syndef kn)
   | Dir dir ->
-      let s,dir = let open Nametab.GlobDirRef in match dir with
+      let s,dir =
+        let open Nametab in
+        let open GlobDirRef in match dir with
         | DirOpenModule { obj_dir ; _ } -> "Open Module", obj_dir
         | DirOpenModtype { obj_dir ; _ } -> "Open Module Type", obj_dir
         | DirOpenSection { obj_dir ; _ } -> "Open Section", obj_dir
@@ -417,7 +419,7 @@ let locate_term qid =
 let locate_module qid =
   let all = Nametab.locate_extended_all_dir qid in
   let map dir = let open Nametab.GlobDirRef in match dir with
-  | DirModule { obj_mp ; _ } -> Some (Dir dir, Nametab.shortest_qualid_of_module obj_mp)
+  | DirModule { Nametab.obj_mp ; _ } -> Some (Dir dir, Nametab.shortest_qualid_of_module obj_mp)
   | DirOpenModule _ -> Some (Dir dir, qid)
   | _ -> None
   in
@@ -634,7 +636,7 @@ let gallina_print_library_entry env sigma with_values ent =
         gallina_print_leaf_entry env sigma with_values (oname,lobj)
     | (oname,Lib.OpenedSection (dir,_)) ->
         Some (str " >>>>>>> Section " ++ pr_name oname)
-    | (_,Lib.CompilingLibrary { obj_dir; _ }) ->
+    | (_,Lib.CompilingLibrary { Nametab.obj_dir; _ }) ->
         Some (str " >>>>>>> Library " ++ DirPath.print obj_dir)
     | (oname,Lib.OpenedModule _) ->
 	Some (str " >>>>>>> Module " ++ pr_name oname)
@@ -759,7 +761,7 @@ let read_sec_context qid =
     with Not_found ->
       user_err ?loc:qid.loc ~hdr:"read_sec_context" (str "Unknown section.") in
   let rec get_cxt in_cxt = function
-    | (_,Lib.OpenedSection ({obj_dir;_},_) as hd)::rest ->
+    | (_,Lib.OpenedSection ({Nametab.obj_dir;_},_) as hd)::rest ->
         if DirPath.equal dir obj_dir then (hd::in_cxt) else get_cxt (hd::in_cxt) rest
     | [] -> []
     | hd::rest -> get_cxt (hd::in_cxt) rest
@@ -788,7 +790,7 @@ let print_any_name env sigma na udecl =
   | Term (ConstructRef ((sp,_),_)) -> print_inductive sp udecl
   | Term (VarRef sp) -> print_section_variable env sigma sp
   | Syntactic kn -> print_syntactic_def env kn
-  | Dir (Nametab.GlobDirRef.DirModule { obj_dir; obj_mp; _ } ) -> print_module (printable_body obj_dir) obj_mp
+  | Dir (Nametab.GlobDirRef.DirModule Nametab.{ obj_dir; obj_mp; _ } ) -> print_module (printable_body obj_dir) obj_mp
   | Dir _ -> mt ()
   | ModuleType mp -> print_modtype mp
   | Other (obj, info) -> info.print obj
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 088ba6552b..787134c173 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -188,7 +188,7 @@ let print_module qid =
     let open Nametab.GlobDirRef in
     let globdir = Nametab.locate_dir qid in
       match globdir with
-          DirModule { obj_dir; obj_mp; _ } ->
+          DirModule Nametab.{ obj_dir; obj_mp; _ } ->
           Printmod.print_module (Printmod.printable_body obj_dir) obj_mp
 	| _ -> raise Not_found
   with