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/setoid_ring/newring.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/setoid_ring')

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