[nametab] Move global_dir_reference to Nametab

This type is "private" to the Nametab, which manages it. It thus makes
sense IMHO to live there.

6 files changed, 51 insertions, 43 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index e01a99f731..f4edbe36bb 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -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"
@@ -198,7 +198,7 @@ let compute_visibility exists i =
 
 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 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;
@@ -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 () =
diff --git a/library/lib.ml b/library/lib.ml
index 1acc8fd8fd..762a2e0567 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -551,7 +551,7 @@ let open_section id =
   let fs = Summary.freeze_summaries ~marshallable:`No in
   add_entry (make_oname 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 ()
 
diff --git a/library/libnames.ml b/library/libnames.ml
index f6fc5ed4b7..d2c96d4163 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -168,25 +168,11 @@ type object_prefix = {
   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..56368fd08c 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -110,16 +110,6 @@ type object_prefix = {
 
 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/nametab.ml b/library/nametab.ml
index 06ace373c3..7f94357a8b 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -15,6 +15,28 @@ open Names
 open Libnames
 open Globnames
 
+(* 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
 
@@ -295,13 +317,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]. *)
@@ -390,7 +406,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 *)
@@ -424,17 +440,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 1c3322bfb1..b71bc77cbb 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -57,6 +57,22 @@ open Globnames
 
 *)
 
+(** 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 +95,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 +114,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 +131,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
 
 (** Mapping a full path to a global reference *)