From 8fafc201699e3d6c80e39bbadf2e6a5ba6425036 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Fri, 7 Sep 2018 17:17:19 +0200
Subject: Move maps & sets indexed by GlobRef.t into the kernel

---
 plugins/extraction/extract_env.ml |  6 +++---
 plugins/extraction/table.ml       | 16 ++++++++--------
 2 files changed, 11 insertions(+), 11 deletions(-)

(limited to 'plugins/extraction')

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 *)
 
-- 
cgit v1.2.3