Move maps & sets indexed by GlobRef.t into the kernel

26 files changed, 216 insertions, 180 deletions

diff --git a/engine/namegen.ml b/engine/namegen.ml
index 978f33b683..2a59b914db 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -258,15 +258,15 @@ let restart_subscript id =
     forget_subscript id
 
 let visible_ids sigma (nenv, c) =
-  let accu = ref (Refset_env.empty, Int.Set.empty, Id.Set.empty) in
+  let accu = ref (GlobRef.Set_env.empty, Int.Set.empty, Id.Set.empty) in
   let rec visible_ids n c = match EConstr.kind sigma c with
   | Const _ | Ind _ | Construct _ | Var _ as c ->
     let (gseen, vseen, ids) = !accu in
     let g = global_of_constr c in
-    if not (Refset_env.mem g gseen) then
+    if not (GlobRef.Set_env.mem g gseen) then
       begin
       try
-      let gseen = Refset_env.add g gseen in
+      let gseen = GlobRef.Set_env.add g gseen in
       let short = shortest_qualid_of_global Id.Set.empty g in
       let dir, id = repr_qualid short in
       let ids = if DirPath.is_empty dir then Id.Set.add id ids else ids in
diff --git a/engine/univNames.ml b/engine/univNames.ml
index a688401741..e861913de2 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -10,7 +10,6 @@
 
 open Names
 open Univ
-open Globnames
 open Nametab
 
 
@@ -51,15 +50,15 @@ type universe_binders = Univ.Level.t Names.Id.Map.t
 
 let empty_binders = Id.Map.empty
 
-let universe_binders_table = Summary.ref Refmap.empty ~name:"universe binders"
+let universe_binders_table = Summary.ref GlobRef.Map.empty ~name:"universe binders"
 
 let universe_binders_of_global ref : universe_binders =
   try
-    let l = Refmap.find ref !universe_binders_table in l
+    let l = GlobRef.Map.find ref !universe_binders_table in l
   with Not_found -> Names.Id.Map.empty
 
 let cache_ubinder (_,(ref,l)) =
-  universe_binders_table := Refmap.add ref l !universe_binders_table
+  universe_binders_table := GlobRef.Map.add ref l !universe_binders_table
 
 let subst_ubinder (subst,(ref,l as orig)) =
   let ref' = fst (Globnames.subst_global subst ref) in
diff --git a/interp/impargs.ml b/interp/impargs.ml
index e542b818f6..3603367cf1 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -508,11 +508,11 @@ type implicit_discharge_request =
   | ImplInteractive of GlobRef.t * implicits_flags *
       implicit_interactive_request
 
-let implicits_table = Summary.ref Refmap.empty ~name:"implicits"
+let implicits_table = Summary.ref GlobRef.Map.empty ~name:"implicits"
 
 let implicits_of_global ref =
   try
-    let l = Refmap.find ref !implicits_table in
+    let l = GlobRef.Map.find ref !implicits_table in
     try
       let rename_l = Arguments_renaming.arguments_names ref in
       let rec rename implicits names = match implicits, names with
@@ -527,7 +527,7 @@ let implicits_of_global ref =
   with Not_found -> [DefaultImpArgs,[]]
 
 let cache_implicits_decl (ref,imps) =
-  implicits_table := Refmap.add ref imps !implicits_table
+  implicits_table := GlobRef.Map.add ref imps !implicits_table
 
 let load_implicits _ (_,(_,l)) = List.iter cache_implicits_decl l
 
diff --git a/interp/notation.ml b/interp/notation.ml
index 6b26f66100..a6a14efc87 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -264,7 +264,7 @@ type key =
   | Oth
 
 let key_compare k1 k2 = match k1, k2 with
-| RefKey gr1, RefKey gr2 -> RefOrdered.compare gr1 gr2
+| RefKey gr1, RefKey gr2 -> GlobRef.Ordered.compare gr1 gr2
 | RefKey _, Oth -> -1
 | Oth, RefKey _ -> 1
 | Oth, Oth -> 0
@@ -395,7 +395,7 @@ let prim_token_interp_infos =
 (* Table from global_reference to backtrack-able informations about
    prim_token uninterpretation (in particular uninterpreter unique id). *)
 let prim_token_uninterp_infos =
-  ref (Refmap.empty : (scope_name * prim_token_uid * bool) Refmap.t)
+  ref (GlobRef.Map.empty : (scope_name * prim_token_uid * bool) GlobRef.Map.t)
 
 let hashtbl_check_and_set allow_overwrite uid f h eq =
   match Hashtbl.find h uid with
@@ -441,7 +441,7 @@ let cache_prim_token_interpretation (_,infos) =
   prim_token_interp_infos :=
     String.Map.add sc (infos.pt_required,infos.pt_uid) !prim_token_interp_infos;
   List.iter (fun r -> prim_token_uninterp_infos :=
-                        Refmap.add r (sc,uid,infos.pt_in_match)
+                        GlobRef.Map.add r (sc,uid,infos.pt_in_match)
                           !prim_token_uninterp_infos)
             infos.pt_refs
 
@@ -783,7 +783,7 @@ let uninterp_prim_token c =
   | None -> raise Notation_ops.No_match
   | Some r ->
      try
-       let (sc,uid,_) = Refmap.find r !prim_token_uninterp_infos in
+       let (sc,uid,_) = GlobRef.Map.find r !prim_token_uninterp_infos in
        let uninterp = Hashtbl.find prim_token_uninterpreters uid in
        match InnerPrimToken.do_uninterp uninterp (AnyGlobConstr c) with
        | None -> raise Notation_ops.No_match
@@ -924,7 +924,7 @@ let rec update_scopes cls scl = match cls, scl with
   | _, [] -> List.map find_scope_class_opt cls
   | cl :: cls, sco :: scl -> update_scope cl sco :: update_scopes cls scl
 
-let arguments_scope = ref Refmap.empty
+let arguments_scope = ref GlobRef.Map.empty
 
 type arguments_scope_discharge_request =
   | ArgsScopeAuto
@@ -934,7 +934,7 @@ type arguments_scope_discharge_request =
 let load_arguments_scope _ (_,(_,r,n,scl,cls)) =
   List.iter (Option.iter check_scope) scl;
   let initial_stamp = ScopeClassMap.empty in
-  arguments_scope := Refmap.add r (scl,cls,initial_stamp) !arguments_scope
+  arguments_scope := GlobRef.Map.add r (scl,cls,initial_stamp) !arguments_scope
 
 let cache_arguments_scope o =
   load_arguments_scope 1 o
@@ -1015,13 +1015,13 @@ let declare_arguments_scope local r scl =
 
 let find_arguments_scope r =
   try
-    let (scl,cls,stamp) = Refmap.find r !arguments_scope in
+    let (scl,cls,stamp) = GlobRef.Map.find r !arguments_scope in
     let cur_stamp = !scope_class_map in
     if stamp == cur_stamp then scl
     else
       (* Recent changes in the Bind Scope base, we re-compute the scopes *)
       let scl' = update_scopes cls scl in
-      arguments_scope := Refmap.add r (scl',cls,cur_stamp) !arguments_scope;
+      arguments_scope := GlobRef.Map.add r (scl',cls,cur_stamp) !arguments_scope;
       scl'
   with Not_found -> []
 
@@ -1350,7 +1350,7 @@ let init () =
   notations_key_table := KeyMap.empty;
   scope_class_map := initial_scope_class_map;
   prim_token_interp_infos := String.Map.empty;
-  prim_token_uninterp_infos := Refmap.empty
+  prim_token_uninterp_infos := GlobRef.Map.empty
 
 let _ =
   Summary.declare_summary "symbols"
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 071248f01f..edbdf1dbba 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -28,7 +28,7 @@ type key =
 (** TODO: share code from Notation *)
 
 let key_compare k1 k2 = match k1, k2 with
-| RefKey gr1, RefKey gr2 -> RefOrdered.compare gr1 gr2
+| RefKey gr1, RefKey gr2 -> GlobRef.Ordered.compare gr1 gr2
 | RefKey _, Oth -> -1
 | Oth, RefKey _ -> 1
 | Oth, Oth -> 0
diff --git a/kernel/names.ml b/kernel/names.ml
index e1d70e8111..933cefe993 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -935,7 +935,7 @@ end
 
 type projection = Projection.t
 
-module GlobRef = struct
+module GlobRefInternal = struct
 
   type t =
     | VarRef of variable           (** A reference to the section-context. *)
@@ -951,11 +951,84 @@ module GlobRef = struct
     | VarRef v1, VarRef v2 -> Id.equal v1 v2
     | (ConstRef _ | IndRef _ | ConstructRef _ | VarRef _), _ -> false
 
+  let global_eq_gen eq_cst eq_ind eq_cons x y =
+    x == y ||
+    match x, y with
+    | ConstRef cx, ConstRef cy -> eq_cst cx cy
+    | IndRef indx, IndRef indy -> eq_ind indx indy
+    | ConstructRef consx, ConstructRef consy -> eq_cons consx consy
+    | VarRef v1, VarRef v2 -> Id.equal v1 v2
+    | (VarRef _ | ConstRef _ | IndRef _ | ConstructRef _), _ -> false
+
+  let global_ord_gen ord_cst ord_ind ord_cons x y =
+    if x == y then 0
+    else match x, y with
+    | VarRef v1, VarRef v2 -> Id.compare v1 v2
+    | VarRef _, _ -> -1
+    | _, VarRef _ -> 1
+    | ConstRef cx, ConstRef cy -> ord_cst cx cy
+    | ConstRef _, _ -> -1
+    | _, ConstRef _ -> 1
+    | IndRef indx, IndRef indy -> ord_ind indx indy
+    | IndRef _, _ -> -1
+    | _ , IndRef _ -> 1
+    | ConstructRef consx, ConstructRef consy -> ord_cons consx consy
+
+  let global_hash_gen hash_cst hash_ind hash_cons gr =
+    let open Hashset.Combine in
+    match gr with
+    | ConstRef c -> combinesmall 1 (hash_cst c)
+    | IndRef i -> combinesmall 2 (hash_ind i)
+    | ConstructRef c -> combinesmall 3 (hash_cons c)
+    | VarRef id -> combinesmall 4 (Id.hash id)
+
+end
+
+module GlobRef = struct
+
+  type t = GlobRefInternal.t =
+    | VarRef of variable           (** A reference to the section-context. *)
+    | ConstRef of Constant.t       (** A reference to the environment. *)
+    | IndRef of inductive          (** A reference to an inductive type. *)
+    | ConstructRef of constructor  (** A reference to a constructor of an inductive type. *)
+
+  let equal = GlobRefInternal.equal
+
+  (* By default, [global_reference] are ordered on their canonical part *)
+
+  module Ordered = struct
+    open Constant.CanOrd
+    type t = GlobRefInternal.t
+    let compare gr1 gr2 =
+      GlobRefInternal.global_ord_gen compare ind_ord constructor_ord gr1 gr2
+    let equal gr1 gr2 = GlobRefInternal.global_eq_gen equal eq_ind eq_constructor gr1 gr2
+    let hash gr = GlobRefInternal.global_hash_gen hash ind_hash constructor_hash gr
+  end
+
+  module Ordered_env = struct
+    open Constant.UserOrd
+    type t = GlobRefInternal.t
+    let compare gr1 gr2 =
+      GlobRefInternal.global_ord_gen compare ind_user_ord constructor_user_ord gr1 gr2
+    let equal gr1 gr2 =
+      GlobRefInternal.global_eq_gen equal eq_user_ind eq_user_constructor gr1 gr2
+    let hash gr = GlobRefInternal.global_hash_gen hash ind_user_hash constructor_user_hash gr
+  end
+
+  module Map = HMap.Make(Ordered)
+  module Set = Map.Set
+
+  (* Alternative sets and maps indexed by the user part of the kernel names *)
+
+  module Map_env = HMap.Make(Ordered_env)
+  module Set_env = Map_env.Set
+
 end
 
 type global_reference = GlobRef.t
 [@@ocaml.deprecated "Alias for [GlobRef.t]"]
 
+
 type evaluable_global_reference =
   | EvalVarRef of Id.t
   | EvalConstRef of Constant.t
diff --git a/kernel/names.mli b/kernel/names.mli
index 1cdf5c2402..2ea8108734 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -645,6 +645,28 @@ module GlobRef : sig
 
   val equal : t -> t -> bool
 
+  module Ordered : sig
+    type nonrec t = t
+    val compare : t -> t -> int
+    val equal : t -> t -> bool
+    val hash : t -> int
+  end
+
+  module Ordered_env : sig
+    type nonrec t = t
+    val compare : t -> t -> int
+    val equal : t -> t -> bool
+    val hash : t -> int
+  end
+
+  module Set_env : CSig.SetS with type elt = t
+  module Map_env : Map.ExtS
+    with type key = t and module Set := Set_env
+
+  module Set : CSig.SetS with type elt = t
+  module Map : Map.ExtS
+    with type key = t and module Set := Set
+
 end
 
 type global_reference = GlobRef.t
diff --git a/library/coqlib.ml b/library/coqlib.ml
index 408e259196..36a9598f36 100644
--- a/library/coqlib.ml
+++ b/library/coqlib.ml
@@ -47,7 +47,7 @@ let gen_reference_in_modules locstr dirs s =
   let dirs = List.map make_dir dirs in
   let qualid = qualid_of_string s in
   let all = Nametab.locate_all qualid in
-  let all = List.sort_uniquize RefOrdered_env.compare all in
+  let all = List.sort_uniquize GlobRef.Ordered_env.compare all in
   let these = List.filter (has_suffix_in_dirs dirs) all in
   match these with
     | [x] -> x
diff --git a/library/globnames.ml b/library/globnames.ml
index 6383a1f8f6..6bbdd36489 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -87,65 +87,14 @@ let printable_constr_of_global = function
   | ConstructRef sp -> mkConstruct sp
   | IndRef sp -> mkInd sp
 
-let global_eq_gen eq_cst eq_ind eq_cons x y =
-  x == y ||
-  match x, y with
-  | ConstRef cx, ConstRef cy -> eq_cst cx cy
-  | IndRef indx, IndRef indy -> eq_ind indx indy
-  | ConstructRef consx, ConstructRef consy -> eq_cons consx consy
-  | VarRef v1, VarRef v2 -> Id.equal v1 v2
-  | (VarRef _ | ConstRef _ | IndRef _ | ConstructRef _), _ -> false
-
-let global_ord_gen ord_cst ord_ind ord_cons x y =
-  if x == y then 0
-  else match x, y with
-  | VarRef v1, VarRef v2 -> Id.compare v1 v2
-  | VarRef _, _ -> -1
-  | _, VarRef _ -> 1
-  | ConstRef cx, ConstRef cy -> ord_cst cx cy
-  | ConstRef _, _ -> -1
-  | _, ConstRef _ -> 1
-  | IndRef indx, IndRef indy -> ord_ind indx indy
-  | IndRef _, _ -> -1
-  | _ , IndRef _ -> 1
-  | ConstructRef consx, ConstructRef consy -> ord_cons consx consy
-
-let global_hash_gen hash_cst hash_ind hash_cons gr =
-  let open Hashset.Combine in
-  match gr with
-  | ConstRef c -> combinesmall 1 (hash_cst c)
-  | IndRef i -> combinesmall 2 (hash_ind i)
-  | ConstructRef c -> combinesmall 3 (hash_cons c)
-  | VarRef id -> combinesmall 4 (Id.hash id)
-
-(* By default, [global_reference] are ordered on their canonical part *)
-
-module RefOrdered = struct
-  open Constant.CanOrd
-  type t = global_reference
-  let compare gr1 gr2 =
-    global_ord_gen compare ind_ord constructor_ord gr1 gr2
-  let equal gr1 gr2 = global_eq_gen equal eq_ind eq_constructor gr1 gr2
-  let hash gr = global_hash_gen hash ind_hash constructor_hash gr
-end
-
-module RefOrdered_env = struct
-  open Constant.UserOrd
-  type t = global_reference
-  let compare gr1 gr2 =
-    global_ord_gen compare ind_user_ord constructor_user_ord gr1 gr2
-  let equal gr1 gr2 =
-    global_eq_gen equal eq_user_ind eq_user_constructor gr1 gr2
-  let hash gr = global_hash_gen hash ind_user_hash constructor_user_hash gr
-end
-
-module Refmap = HMap.Make(RefOrdered)
-module Refset = Refmap.Set
+module RefOrdered = Names.GlobRef.Ordered
+module RefOrdered_env = Names.GlobRef.Ordered_env
 
-(* Alternative sets and maps indexed by the user part of the kernel names *)
+module Refmap = Names.GlobRef.Map
+module Refset = Names.GlobRef.Set
 
-module Refmap_env = HMap.Make(RefOrdered_env)
-module Refset_env = Refmap_env.Set
+module Refmap_env = Names.GlobRef.Map_env
+module Refset_env = Names.GlobRef.Set_env
 
 (* Extended global references *)
 
@@ -164,14 +113,14 @@ module ExtRefOrdered = struct
   let equal x y =
     x == y ||
     match x, y with
-    | TrueGlobal rx, TrueGlobal ry -> RefOrdered_env.equal rx ry
+    | TrueGlobal rx, TrueGlobal ry -> GlobRef.Ordered_env.equal rx ry
     | SynDef knx, SynDef kny -> KerName.equal knx kny
     | (TrueGlobal _ | SynDef _), _ -> false
 
   let compare x y =
     if x == y then 0
     else match x, y with
-      | TrueGlobal rx, TrueGlobal ry -> RefOrdered_env.compare rx ry
+      | TrueGlobal rx, TrueGlobal ry -> GlobRef.Ordered_env.compare rx ry
       | SynDef knx, SynDef kny -> KerName.compare knx kny
       | TrueGlobal _, SynDef _ -> -1
       | SynDef _, TrueGlobal _ -> 1
@@ -179,7 +128,7 @@ module ExtRefOrdered = struct
   open Hashset.Combine
 
   let hash = function
-  | TrueGlobal gr -> combinesmall 1 (RefOrdered_env.hash gr)
+  | TrueGlobal gr -> combinesmall 1 (GlobRef.Ordered_env.hash gr)
   | SynDef kn -> combinesmall 2 (KerName.hash kn)
 
 end
diff --git a/library/globnames.mli b/library/globnames.mli
index 15fcd5bdd9..45ee069b06 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -8,7 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Util
 open Names
 open Constr
 open Mod_subst
@@ -49,27 +48,21 @@ val printable_constr_of_global : GlobRef.t -> constr
    raise [Not_found] if not a global reference *)
 val global_of_constr : constr -> GlobRef.t
 
-module RefOrdered : sig
-  type t = GlobRef.t
-  val compare : t -> t -> int
-  val equal : t -> t -> bool
-  val hash : t -> int
-end
+module RefOrdered = Names.GlobRef.Ordered
+[@@ocaml.deprecated "Use Names.GlobRef.Ordered"]
 
-module RefOrdered_env : sig
-  type t = GlobRef.t
-  val compare : t -> t -> int
-  val equal : t -> t -> bool
-  val hash : t -> int
-end
+module RefOrdered_env = Names.GlobRef.Ordered_env
+[@@ocaml.deprecated "Use Names.GlobRef.Ordered_env"]
 
-module Refset : CSig.SetS with type elt = GlobRef.t
-module Refmap : Map.ExtS
-  with type key = GlobRef.t and module Set := Refset
+module Refset = Names.GlobRef.Set
+[@@ocaml.deprecated "Use Names.GlobRef.Set"]
+module Refmap = Names.GlobRef.Map
+[@@ocaml.deprecated "Use Names.GlobRef.Map"]
 
-module Refset_env : CSig.SetS with type elt = GlobRef.t
-module Refmap_env : Map.ExtS
-  with type key = GlobRef.t and module Set := Refset_env
+module Refset_env = GlobRef.Set_env
+[@@ocaml.deprecated "Use Names.GlobRef.Set_env"]
+module Refmap_env = GlobRef.Map_env
+[@@ocaml.deprecated "Use Names.GlobRef.Map_env"]
 
 (** {6 Extended global references } *)
 
diff --git a/library/keys.ml b/library/keys.ml
index 3cadcb6472..a74d13c600 100644
--- a/library/keys.ml
+++ b/library/keys.ml
@@ -31,7 +31,7 @@ module KeyOrdered = struct
 
   let hash gr =
     match gr with
-    | KGlob gr -> 8 + RefOrdered.hash gr
+    | KGlob gr -> 8 + GlobRef.Ordered.hash gr
     | KLam -> 0
     | KLet -> 1
     | KProd -> 2
@@ -43,14 +43,14 @@ module KeyOrdered = struct
 
   let compare gr1 gr2 =
     match gr1, gr2 with
-    | KGlob gr1, KGlob gr2 -> RefOrdered.compare gr1 gr2
+    | KGlob gr1, KGlob gr2 -> GlobRef.Ordered.compare gr1 gr2
     | _, KGlob _ -> -1
     | KGlob _, _ -> 1
     | k, k' -> Int.compare (hash k) (hash k')
     
   let equal k1 k2 =
     match k1, k2 with
-    | KGlob gr1, KGlob gr2 -> RefOrdered.equal gr1 gr2
+    | KGlob gr1, KGlob gr2 -> GlobRef.Ordered.equal gr1 gr2
     | _, KGlob _ -> false
     | KGlob _, _ -> false
     | k, k' -> k == k'
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 4ede11b5c9..5d3115d8d7 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -710,10 +710,10 @@ let structure_for_compute env sg c =
   init false false ~compute:true;
   let ast, mlt = Extraction.extract_constr env sg c in
   let ast = Mlutil.normalize ast in
-  let refs = ref Refset.empty in
-  let add_ref r = refs := Refset.add r !refs in
+  let refs = ref GlobRef.Set.empty in
+  let add_ref r = refs := GlobRef.Set.add r !refs in
   let () = ast_iter_references add_ref add_ref add_ref ast in
-  let refs = Refset.elements !refs in
+  let refs = GlobRef.Set.elements !refs in
   let struc = optimize_struct (refs,[]) (mono_environment refs []) in
   (flatten_structure struc), ast, mlt
 
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index c3f4cfe654..e05e82af6f 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -30,8 +30,8 @@ let capitalize = String.capitalize
 (** Sets and maps for [global_reference] that use the "user" [kernel_name]
     instead of the canonical one *)
 
-module Refmap' = Refmap_env
-module Refset' = Refset_env
+module Refmap' = GlobRef.Map_env
+module Refset' = GlobRef.Set_env
 
 (*S Utilities about [module_path] and [kernel_names] and [global_reference] *)
 
@@ -213,12 +213,12 @@ let is_recursor = function
 
 (* NB: here, working modulo name equivalence is ok *)
 
-let projs = ref (Refmap.empty : (inductive*int) Refmap.t)
-let init_projs () = projs := Refmap.empty
-let add_projection n kn ip = projs := Refmap.add (ConstRef kn) (ip,n) !projs
-let is_projection r = Refmap.mem r !projs
-let projection_arity r = snd (Refmap.find r !projs)
-let projection_info r = Refmap.find r !projs
+let projs = ref (GlobRef.Map.empty : (inductive*int) GlobRef.Map.t)
+let init_projs () = projs := GlobRef.Map.empty
+let add_projection n kn ip = projs := GlobRef.Map.add (ConstRef kn) (ip,n) !projs
+let is_projection r = GlobRef.Map.mem r !projs
+let projection_arity r = snd (GlobRef.Map.find r !projs)
+let projection_info r = GlobRef.Map.find r !projs
 
 (*s Table of used axioms *)
 
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 85f4939560..286021d68e 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -38,7 +38,7 @@ let compare_gr id1 id2 =
   if id1==id2 then 0 else
     if id1==dummy_id then 1
     else if id2==dummy_id then -1
-    else Globnames.RefOrdered.compare id1 id2
+    else GlobRef.Ordered.compare id1 id2
 
 module OrderedInstance=
 struct
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 2a527da9be..5958fe8203 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -62,7 +62,7 @@ module Hitem=
 struct
   type t = h_item
   let compare (id1,co1) (id2,co2)=
-    let c = Globnames.RefOrdered.compare id1 id2 in
+    let c = GlobRef.Ordered.compare id1 id2 in
     if c = 0 then
       let cmp (i1, c1) (i2, c2) =
         let c = Int.compare i1 i2 in
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index a736eec5e7..b05e1e85b7 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -99,7 +99,7 @@ let protect_tac_in map id =
 let rec closed_under sigma cset t =
   try
     let (gr, _) = Termops.global_of_constr sigma t in
-    Refset_env.mem gr cset
+    GlobRef.Set_env.mem gr cset
   with Not_found ->
     match EConstr.kind sigma t with
     | Cast(c,_,_) -> closed_under sigma cset c
@@ -111,7 +111,7 @@ let closed_term args _ = match args with
   let t = Option.get (Value.to_constr t) in
   let l = List.map (fun c -> Value.cast (Genarg.topwit Stdarg.wit_ref) c) (Option.get (Value.to_list l)) in
   Proofview.tclEVARMAP >>= fun sigma ->
-  let cs = List.fold_right Refset_env.add l Refset_env.empty in
+  let cs = List.fold_right GlobRef.Set_env.add l GlobRef.Set_env.empty in
   if closed_under sigma cs t then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (mt())
 | _ -> assert false
 
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index 9d4badc60a..b8958ca944 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -21,7 +21,7 @@ module NamedDecl = Context.Named.Declaration
 (*i*)
 
 let name_table =
-  Summary.ref (Refmap.empty : Name.t list Refmap.t)
+  Summary.ref (GlobRef.Map.empty : Name.t list GlobRef.Map.t)
     ~name:"rename-arguments"
 
 type req =
@@ -29,7 +29,7 @@ type req =
   | ReqGlobal of GlobRef.t * Name.t list
 
 let load_rename_args _ (_, (_, (r, names))) =
-  name_table := Refmap.add r names !name_table
+  name_table := GlobRef.Map.add r names !name_table
 
 let cache_rename_args o = load_rename_args 1 o
 
@@ -68,7 +68,7 @@ let rename_arguments local r names =
   let req = if local then ReqLocal else ReqGlobal (r, names) in
   Lib.add_anonymous_leaf (inRenameArgs (req, (r, names)))       
 
-let arguments_names r = Refmap.find r !name_table
+let arguments_names r = GlobRef.Map.find r !name_table
 
 let rec rename_prod c = function 
   | [] -> c
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 332ecd2c91..94da51626f 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -38,7 +38,7 @@ type cl_info_typ = {
 
 type coe_typ = GlobRef.t
 
-module CoeTypMap = Refmap_env
+module CoeTypMap = GlobRef.Map_env
 
 type coe_info_typ = {
   coe_value : GlobRef.t;
@@ -118,7 +118,7 @@ let coercion_tab =
   ref (CoeTypMap.empty : coe_info_typ CoeTypMap.t)
 
 let coercions_in_scope =
-  ref Refset_env.empty
+  ref GlobRef.Set_env.empty
 
 module ClPairOrd =
 struct
@@ -450,7 +450,7 @@ let load_coercion _ o =
 
 let set_coercion_in_scope (_, c) =
   let r = c.coercion_type in
-  coercions_in_scope := Refset_env.add r !coercions_in_scope
+  coercions_in_scope := GlobRef.Set_env.add r !coercions_in_scope
 
 let open_coercion i o =
   if Int.equal i 1 then begin
@@ -545,7 +545,7 @@ let coercion_of_reference r =
 module CoercionPrinting =
   struct
     type t = coe_typ
-    let compare = RefOrdered.compare
+    let compare = GlobRef.Ordered.compare
     let encode = coercion_of_reference
     let subst = subst_coe_typ
     let printer x = pr_global_env Id.Set.empty x
@@ -565,4 +565,4 @@ let hide_coercion coe =
   else None
 
 let is_coercion_in_scope r =
-  Refset_env.mem r !coercions_in_scope
+  GlobRef.Set_env.mem r !coercions_in_scope
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 2f861c117b..bd41e61b34 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -192,11 +192,11 @@ let rec assoc_pat a = function
 
 
 let object_table =
-  Summary.ref (Refmap.empty : ((cs_pattern * constr) * obj_typ) list Refmap.t)
+  Summary.ref (GlobRef.Map.empty : ((cs_pattern * constr) * obj_typ) list GlobRef.Map.t)
     ~name:"record-canonical-structs"
 
 let canonical_projections () =
-  Refmap.fold (fun x -> List.fold_right (fun ((y,_),c) acc -> ((x,y),c)::acc))
+  GlobRef.Map.fold (fun x -> List.fold_right (fun ((y,_),c) acc -> ((x,y),c)::acc))
     !object_table []
 
 let keep_true_projections projs kinds =
@@ -289,11 +289,11 @@ let warn_redundant_canonical_projection =
 let add_canonical_structure warn o =
     let lo = compute_canonical_projections warn o in
     List.iter (fun ((proj,(cs_pat,_ as pat)),s) ->
-      let l = try Refmap.find proj !object_table with Not_found -> [] in
+      let l = try GlobRef.Map.find proj !object_table with Not_found -> [] in
       let ocs = try Some (assoc_pat cs_pat l)
       with Not_found -> None
       in match ocs with
-        | None -> object_table := Refmap.add proj ((pat,s)::l) !object_table;
+        | None -> object_table := GlobRef.Map.add proj ((pat,s)::l) !object_table;
         | Some (c, cs) ->
               let old_can_s = (Termops.print_constr (EConstr.of_constr cs.o_DEF))
               and new_can_s = (Termops.print_constr (EConstr.of_constr s.o_DEF)) in
@@ -372,18 +372,18 @@ let declare_canonical_structure ref =
   add_canonical_structure (check_and_decompose_canonical_structure ref)
 
 let lookup_canonical_conversion (proj,pat) =
-  assoc_pat pat (Refmap.find proj !object_table)
+  assoc_pat pat (GlobRef.Map.find proj !object_table)
 
 let decompose_projection sigma c args =
   match EConstr.kind sigma c with
   | Const (c, u) ->
      let n = find_projection_nparams (ConstRef c) in
      (** Check if there is some canonical projection attached to this structure *)
-     let _ = Refmap.find (ConstRef c) !object_table in
+     let _ = GlobRef.Map.find (ConstRef c) !object_table in
      let arg = Stack.nth args n in
      arg
   | Proj (p, c) ->
-     let _ = Refmap.find (ConstRef (Projection.constant p)) !object_table in
+     let _ = GlobRef.Map.find (ConstRef (Projection.constant p)) !object_table in
      c
   | _ -> raise Not_found
 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index f133eb9963..f4c8a6cd66 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -88,6 +88,7 @@ let set_reduction_effect x funkey =
 (** Machinery to custom the behavior of the reduction *)
 module ReductionBehaviour = struct
   open Globnames
+  open Names
   open Libobject
 
   type t = {
@@ -97,7 +98,7 @@ module ReductionBehaviour = struct
   }
 
   let table =
-    Summary.ref (Refmap.empty : t Refmap.t) ~name:"reductionbehaviour"
+    Summary.ref (GlobRef.Map.empty : t GlobRef.Map.t) ~name:"reductionbehaviour"
 
   type flag = [ `ReductionDontExposeCase | `ReductionNeverUnfold ]
   type req =
@@ -105,7 +106,7 @@ module ReductionBehaviour = struct
     | ReqGlobal of GlobRef.t * (int list * int * flag list)
 
   let load _ (_,(_,(r, b))) =
-    table := Refmap.add r b !table
+    table := GlobRef.Map.add r b !table
 
   let cache o = load 1 o
 
@@ -160,7 +161,7 @@ module ReductionBehaviour = struct
 
   let get r =
     try
-      let b = Refmap.find r !table in
+      let b = GlobRef.Map.find r !table in
       let flags =
 	if Int.equal b.b_nargs max_int then [`ReductionNeverUnfold]
 	else if b.b_dont_expose_case then [`ReductionDontExposeCase] else [] in
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index efb3c339ac..55d9838bbb 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -88,7 +88,7 @@ type typeclass = {
   cl_unique : bool;
 }
 
-type typeclasses = typeclass Refmap.t
+type typeclasses = typeclass GlobRef.Map.t
 
 type instance = {
   is_class: GlobRef.t;
@@ -99,7 +99,7 @@ type instance = {
   is_impl: GlobRef.t;
 }
 
-type instances = (instance Refmap.t) Refmap.t
+type instances = (instance GlobRef.Map.t) GlobRef.Map.t
 
 let instance_impl is = is.is_impl
 
@@ -121,8 +121,8 @@ let new_instance cl info glob impl =
  * states management
  *)
 
-let classes : typeclasses ref = Summary.ref Refmap.empty ~name:"classes"
-let instances : instances ref = Summary.ref Refmap.empty ~name:"instances"
+let classes : typeclasses ref = Summary.ref GlobRef.Map.empty ~name:"classes"
+let instances : instances ref = Summary.ref GlobRef.Map.empty ~name:"instances"
 
 let typeclass_univ_instance (cl, u) =
   assert (Univ.AUContext.size cl.cl_univs == Univ.Instance.length u);
@@ -131,7 +131,7 @@ let typeclass_univ_instance (cl, u) =
       cl_props = subst_ctx cl.cl_props}
 
 let class_info c =
-  try Refmap.find c !classes
+  try GlobRef.Map.find c !classes
   with Not_found -> not_a_class (Global.env()) (EConstr.of_constr (printable_constr_of_global c))
 
 let global_class_of_constr env sigma c =
@@ -154,7 +154,7 @@ let class_of_constr sigma c =
 
 let is_class_constr sigma c = 
   try let gr, u = Termops.global_of_constr sigma c in
-	Refmap.mem gr !classes
+    GlobRef.Map.mem gr !classes
   with Not_found -> false
 
 let rec is_class_type evd c =
@@ -172,7 +172,7 @@ let is_class_evar evd evi =
  *)
 
 let load_class (_, cl) =
-  classes := Refmap.add cl.cl_impl cl !classes
+  classes := GlobRef.Map.add cl.cl_impl cl !classes
 
 let cache_class = load_class
 
@@ -336,17 +336,17 @@ type instance_action =
 
 let load_instance inst = 
   let insts = 
-    try Refmap.find inst.is_class !instances
-    with Not_found -> Refmap.empty in
-  let insts = Refmap.add inst.is_impl inst insts in
-  instances := Refmap.add inst.is_class insts !instances
+    try GlobRef.Map.find inst.is_class !instances
+    with Not_found -> GlobRef.Map.empty in
+  let insts = GlobRef.Map.add inst.is_impl inst insts in
+  instances := GlobRef.Map.add inst.is_class insts !instances
 
 let remove_instance inst =
   let insts = 
-    try Refmap.find inst.is_class !instances
+    try GlobRef.Map.find inst.is_class !instances
     with Not_found -> assert false in
-  let insts = Refmap.remove inst.is_impl insts in
-  instances := Refmap.add inst.is_class insts !instances
+  let insts = GlobRef.Map.remove inst.is_impl insts in
+  instances := GlobRef.Map.add inst.is_class insts !instances
 
 let cache_instance (_, (action, i)) =
   match action with 
@@ -464,23 +464,23 @@ let instance_constructor (cl,u) args =
           (term, applist (mkConstU cst, pars))
       | _ -> assert false
 
-let typeclasses () = Refmap.fold (fun _ l c -> l :: c) !classes []
+let typeclasses () = GlobRef.Map.fold (fun _ l c -> l :: c) !classes []
 
-let cmap_elements c = Refmap.fold (fun k v acc -> v :: acc) c []
+let cmap_elements c = GlobRef.Map.fold (fun k v acc -> v :: acc) c []
 
 let instances_of c =
-  try cmap_elements (Refmap.find c.cl_impl !instances) with Not_found -> []
+  try cmap_elements (GlobRef.Map.find c.cl_impl !instances) with Not_found -> []
 
 let all_instances () = 
-  Refmap.fold (fun k v acc ->
-    Refmap.fold (fun k v acc -> v :: acc) v acc)
+  GlobRef.Map.fold (fun k v acc ->
+    GlobRef.Map.fold (fun k v acc -> v :: acc) v acc)
     !instances []
 
 let instances r = 
   let cl = class_info r in instances_of cl    
 
 let is_class gr = 
-  Refmap.exists (fun _ v -> GlobRef.equal v.cl_impl gr) !classes
+  GlobRef.Map.exists (fun _ v -> GlobRef.equal v.cl_impl gr) !classes
 
 let is_instance = function
   | ConstRef c ->
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index aca7f6c65e..bfee0422e7 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -28,7 +28,7 @@ type term_label =
 | SortLabel
 
 let compare_term_label t1 t2 = match t1, t2 with
-| GRLabel gr1, GRLabel gr2 -> RefOrdered.compare gr1 gr2
+| GRLabel gr1, GRLabel gr2 -> GlobRef.Ordered.compare gr1 gr2
 | _ -> Pervasives.compare t1 t2 (** OK *)
 
 type 'res lookup_res = 'res Dn.lookup_res = Label of 'res | Nothing | Everything
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 43a450ea71..dce1a1bef6 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -288,7 +288,7 @@ let lookup_tacs sigma concl st se =
   let sl' = List.stable_sort pri_order_int l' in
   List.merge pri_order_int se.sentry_nopat sl'
 
-module Constr_map = Map.Make(RefOrdered)
+module Constr_map = Map.Make(GlobRef.Ordered)
 
 let is_transparent_gr (ids, csts) = function
   | VarRef id -> Id.Pred.mem id ids
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index 8bdcc63215..03d2a17eee 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -100,7 +100,7 @@ struct
   | DRel, _ -> -1 | _, DRel -> 1
   | DSort, DSort -> 0
   | DSort, _ -> -1 | _, DSort -> 1
-  | DRef gr1, DRef gr2 -> RefOrdered.compare gr1 gr2
+  | DRef gr1, DRef gr2 -> GlobRef.Ordered.compare gr1 gr2
   | DRef _, _ -> -1 | _, DRef _ -> 1
 
   | DCtx (tl1, tr1), DCtx (tl2, tr2)
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index e5d2382e46..0bcd3c64eb 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -213,25 +213,25 @@ let rec traverse current ctx accu t = match Constr.kind t with
 
 and traverse_object ?inhabits (curr, data, ax2ty) body obj =
   let data, ax2ty =
-    let already_in = Refmap_env.mem obj data in
+    let already_in = GlobRef.Map_env.mem obj data in
     match body () with
     | None ->
         let data =
-          if not already_in then Refmap_env.add obj Refset_env.empty data else data in
+          if not already_in then GlobRef.Map_env.add obj GlobRef.Set_env.empty data else data in
         let ax2ty =
           if Option.is_empty inhabits then ax2ty else
           let ty = Option.get inhabits in
-          try let l = Refmap_env.find obj ax2ty in Refmap_env.add obj (ty::l) ax2ty 
-          with Not_found -> Refmap_env.add obj [ty] ax2ty in
+          try let l = GlobRef.Map_env.find obj ax2ty in GlobRef.Map_env.add obj (ty::l) ax2ty
+          with Not_found -> GlobRef.Map_env.add obj [ty] ax2ty in
         data, ax2ty
     | Some body ->
       if already_in then data, ax2ty else
       let contents,data,ax2ty =
         traverse (label_of obj) Context.Rel.empty
-                 (Refset_env.empty,data,ax2ty) body in
-      Refmap_env.add obj contents data, ax2ty
+                 (GlobRef.Set_env.empty,data,ax2ty) body in
+      GlobRef.Map_env.add obj contents data, ax2ty
   in
-  (Refset_env.add obj curr, data, ax2ty)
+  (GlobRef.Set_env.add obj curr, data, ax2ty)
 
 (** Collects the references occurring in the declaration of mutual inductive
     definitions. All the constructors and names of a mutual inductive
@@ -244,14 +244,14 @@ and traverse_inductive (curr, data, ax2ty) mind obj =
    (* Invariant : I_0 \in data iff I_i \in data iff c_ij \in data
       where I_0, I_1, ... are in the same mutual definition and c_ij
       are all their constructors. *)
-   if Refmap_env.mem firstind_ref data then data, ax2ty else
+   if GlobRef.Map_env.mem firstind_ref data then data, ax2ty else
      let mib = lookup_mind mind in
      (* Collects references of parameters *)
      let param_ctx = mib.mind_params_ctxt in
      let nparam = List.length param_ctx in
      let accu =
        traverse_context label Context.Rel.empty
-                        (Refset_env.empty, data, ax2ty) param_ctx
+                        (GlobRef.Set_env.empty, data, ax2ty) param_ctx
      in
      (* Build the context of all arities *)
      let arities_ctx =
@@ -283,14 +283,14 @@ and traverse_inductive (curr, data, ax2ty) mind obj =
      (* Maps all these dependencies to inductives and constructors*)
      let data = Array.fold_left_i (fun n data oib ->
        let ind = (mind, n) in
-       let data = Refmap_env.add (IndRef ind) contents data in
+       let data = GlobRef.Map_env.add (IndRef ind) contents data in
        Array.fold_left_i (fun k data _ ->
-         Refmap_env.add (ConstructRef (ind, k+1)) contents data
+         GlobRef.Map_env.add (ConstructRef (ind, k+1)) contents data
        ) data oib.mind_consnames) data mib.mind_packets
      in
      data, ax2ty
   in
-  (Refset_env.add obj curr, data, ax2ty)
+  (GlobRef.Set_env.add obj curr, data, ax2ty)
 
 (** Collects references in a rel_context. *)
 and traverse_context current ctx accu ctxt =
@@ -307,7 +307,7 @@ and traverse_context current ctx accu ctxt =
 
 let traverse current t =
   let () = modcache := MPmap.empty in
-  traverse current Context.Rel.empty (Refset_env.empty, Refmap_env.empty, Refmap_env.empty) t
+  traverse current Context.Rel.empty (GlobRef.Set_env.empty, GlobRef.Map_env.empty, GlobRef.Map_env.empty) t
 
 (** Hopefully bullet-proof function to recover the type of a constant. It just
     ignores all the universe stuff. There are many issues that can arise when
@@ -330,12 +330,12 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
       let accu =
         if cb.const_typing_flags.check_guarded then accu
         else
-          let l = try Refmap_env.find obj ax2ty with Not_found -> [] in
+          let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
           ContextObjectMap.add (Axiom (Guarded kn, l)) Constr.mkProp accu
       in
     if not (Declareops.constant_has_body cb) || not cb.const_typing_flags.check_universes then
       let t = type_of_constant cb in
-      let l = try Refmap_env.find obj ax2ty with Not_found -> [] in
+      let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
       ContextObjectMap.add (Axiom (Constant kn,l)) t accu
     else if add_opaque && (Declareops.is_opaque cb || not (Cpred.mem kn knst)) then
       let t = type_of_constant cb in
@@ -350,7 +350,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
       if mind.mind_typing_flags.check_guarded then
         accu
       else
-        let l = try Refmap_env.find obj ax2ty with Not_found -> [] in
+        let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
         ContextObjectMap.add (Axiom (Positive m, l)) Constr.mkProp accu
   in
-  Refmap_env.fold fold graph ContextObjectMap.empty
+  GlobRef.Map_env.fold fold graph ContextObjectMap.empty
diff --git a/vernac/assumptions.mli b/vernac/assumptions.mli
index 751e79d89c..aead345d8c 100644
--- a/vernac/assumptions.mli
+++ b/vernac/assumptions.mli
@@ -10,7 +10,6 @@
 
 open Names
 open Constr
-open Globnames
 open Printer
 
 (** Collects all the objects on which a term directly relies, bypassing kernel
@@ -22,8 +21,8 @@ open Printer
 *)
 val traverse :
   Label.t -> constr ->
-    (Refset_env.t * Refset_env.t Refmap_env.t *
-     (Label.t * Constr.rel_context * types) list Refmap_env.t)
+    (GlobRef.Set_env.t * GlobRef.Set_env.t GlobRef.Map_env.t *
+     (Label.t * Constr.rel_context * types) list GlobRef.Map_env.t)
 
 (** Collects all the assumptions (optionally including opaque definitions)
    on which a term relies (together with their type). The above warning of