Add ExtRefMap/Set to globnames

3 files changed, 14 insertions, 8 deletions

diff --git a/library/globnames.ml b/library/globnames.ml
index 9126a467bf..5dbc8db647 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -117,3 +117,6 @@ module ExtRefOrdered = struct
   | SynDef kn -> combinesmall 2 (KerName.hash kn)
 
 end
+
+module ExtRefMap = HMap.Make(ExtRefOrdered)
+module ExtRefSet = ExtRefMap.Set
diff --git a/library/globnames.mli b/library/globnames.mli
index fb1583e16c..f5ed3a3ec7 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -61,3 +61,8 @@ module ExtRefOrdered : sig
   val equal : t -> t -> bool
   val hash : t -> int
 end
+
+module ExtRefSet : CSig.SetS with type elt = extended_global_reference
+module ExtRefMap : CMap.ExtS
+  with type key = extended_global_reference
+   and module Set := ExtRefSet
diff --git a/library/nametab.ml b/library/nametab.ml
index 523fe8af50..d9b4dc9122 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -352,10 +352,8 @@ let the_univtab = Summary.ref ~name:"univtab" (UnivTab.empty : univtab)
 (* Reversed name tables ***************************************************)
 
 (* This table translates extended_global_references back to section paths *)
-module Globrevtab = HMap.Make(ExtRefOrdered)
-
-type globrevtab = full_path Globrevtab.t
-let the_globrevtab = Summary.ref ~name:"globrevtab" (Globrevtab.empty : globrevtab)
+type globrevtab = full_path ExtRefMap.t
+let the_globrevtab = Summary.ref ~name:"globrevtab" (ExtRefMap.empty : globrevtab)
 
 
 type mprevtab = DirPath.t MPmap.t
@@ -386,7 +384,7 @@ let push_xref visibility sp xref =
   match visibility with
     | Until _ ->
         the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab;
-        the_globrevtab := Globrevtab.add xref sp !the_globrevtab
+        the_globrevtab := ExtRefMap.add xref sp !the_globrevtab
     | _ ->
         begin
           if ExtRefTab.exists sp !the_ccitab then
@@ -520,7 +518,7 @@ let path_of_global ref =
   let open GlobRef in
   match ref with
     | VarRef id -> make_path DirPath.empty id
-    | _ -> Globrevtab.find (TrueGlobal ref) !the_globrevtab
+    | _ -> ExtRefMap.find (TrueGlobal ref) !the_globrevtab
 
 let dirpath_of_global ref =
   fst (repr_path (path_of_global ref))
@@ -529,7 +527,7 @@ let basename_of_global ref =
   snd (repr_path (path_of_global ref))
 
 let path_of_syndef kn =
-  Globrevtab.find (SynDef kn) !the_globrevtab
+  ExtRefMap.find (SynDef kn) !the_globrevtab
 
 let dirpath_of_module mp =
   MPmap.find mp !the_modrevtab
@@ -547,7 +545,7 @@ let shortest_qualid_of_global ?loc ctx ref =
   match ref with
     | VarRef id -> make_qualid ?loc DirPath.empty id
     | _ ->
-        let sp = Globrevtab.find (TrueGlobal ref) !the_globrevtab in
+        let sp = ExtRefMap.find (TrueGlobal ref) !the_globrevtab in
         ExtRefTab.shortest_qualid ?loc ctx sp !the_ccitab
 
 let shortest_qualid_of_syndef ?loc ctx kn =