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

5 files changed, 15 insertions, 15 deletions

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