Merge PR #8436: Move maps & sets indexed by GlobRef.t into the kernel

5 files changed, 39 insertions, 38 deletions

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