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

3 files changed, 13 insertions, 13 deletions

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