[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.

9 files changed, 59 insertions, 49 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 *)
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 4619e049e0..96720e84d6 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -326,7 +326,7 @@ type locatable = Locatable : 'a locatable_info -> locatable
 
 type logical_name =
   | Term of GlobRef.t
-  | Dir of global_dir_reference
+  | Dir of Nametab.GlobDirRef.t
   | Syntactic of KerName.t
   | ModuleType of ModPath.t
   | Other : 'a * 'a locatable_info -> logical_name
@@ -367,7 +367,7 @@ let pr_located_qualid = function
   | Syntactic kn ->
       str "Notation" ++ spc () ++ pr_path (Nametab.path_of_syndef kn)
   | Dir dir ->
-      let s,dir = match dir with
+      let s,dir = let open Nametab.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
@@ -416,7 +416,7 @@ let locate_term qid =
 
 let locate_module qid =
   let all = Nametab.locate_extended_all_dir qid in
-  let map dir = match dir with
+  let map dir = let open Nametab.GlobDirRef in match dir with
   | DirModule { obj_mp ; _ } -> Some (Dir dir, Nametab.shortest_qualid_of_module obj_mp)
   | DirOpenModule _ -> Some (Dir dir, qid)
   | _ -> None
@@ -429,7 +429,7 @@ let locate_modtype qid =
   let modtypes = List.map map all in
   (** Don't forget the opened module types: they are not part of the same name tab. *)
   let all = Nametab.locate_extended_all_dir qid in
-  let map dir = match dir with
+  let map dir = let open Nametab.GlobDirRef in match dir with
   | DirOpenModtype _ -> Some (Dir dir, qid)
   | _ -> None
   in
@@ -788,7 +788,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 (DirModule { obj_dir; obj_mp; _ } ) -> print_module (printable_body obj_dir) obj_mp
+  | Dir (Nametab.GlobDirRef.DirModule { 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/printing/printmod.ml b/printing/printmod.ml
index 20e0a989f3..cc40c74998 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -223,7 +223,7 @@ let print_kn locals kn =
 let nametab_register_dir obj_mp =
   let id = mk_fake_top () in
   let obj_dir = DirPath.make [id] in
-  Nametab.push_dir (Nametab.Until 1) obj_dir (DirModule { obj_dir; obj_mp; obj_sec = DirPath.empty })
+  Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirModule { obj_dir; obj_mp; obj_sec = DirPath.empty }))
 
 (** Nota: the [global_reference] we register in the nametab below
     might differ from internal ones, since we cannot recreate here
@@ -402,6 +402,7 @@ let rec printable_body dir =
   let dir = pop_dirpath dir in
     DirPath.is_empty dir ||
     try
+      let open Nametab.GlobDirRef in
       match Nametab.locate_dir (qualid_of_dirpath dir) with
 	  DirOpenModtype _ -> false
 	| DirModule _ | DirOpenModule _ -> printable_body dir
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 1190d73258..088ba6552b 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -185,6 +185,7 @@ let print_modules () =
 
 let print_module qid =
   try
+    let open Nametab.GlobDirRef in
     let globdir = Nametab.locate_dir qid in
       match globdir with
           DirModule { obj_dir; obj_mp; _ } ->