2 files changed, 6 insertions, 7 deletions
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 99bb8440c..5facf2a80 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -78,7 +78,7 @@ and mk_clos_app_but f_map subs f args n =
     | None -> mk_atom (mkApp (f, args))
 
 let interp_map l t =
-  try Some(List.assoc_f eq_gr t l) with Not_found -> None
+  try Some(List.assoc_f GlobRef.equal t l) with Not_found -> None
 
 let protect_maps = ref String.Map.empty
 let add_map s m = protect_maps := String.Map.add s m !protect_maps
@@ -186,8 +186,8 @@ let dummy_goal env sigma =
     Goal.V82.mk_goal sigma (named_context_val env) EConstr.mkProp Evd.Store.empty in
   {Evd.it = gl; Evd.sigma = sigma}
 
-let constr_of v = match Value.to_constr v with
-  | Some c -> EConstr.Unsafe.to_constr c
+let constr_of evd v = match Value.to_constr v with
+  | Some c -> EConstr.to_constr evd c
   | None -> failwith "Ring.exec_tactic: anomaly"
 
 let tactic_res = ref [||]
@@ -221,8 +221,8 @@ let exec_tactic env evd n f args =
   (** Evaluate the whole result *)
   let gl = dummy_goal env evd in
   let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in
-  let evd, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in
-  let nf c = nf (constr_of c) in
+  let evd = Evd.minimize_universes (Refiner.project gls) in
+  let nf c = constr_of evd c in
   Array.map nf !tactic_res, Evd.universe_context_set evd
 
 let stdlib_modules =
diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli
index 1d1557b12..0e056a472 100644
--- a/plugins/setoid_ring/newring.mli
+++ b/plugins/setoid_ring/newring.mli
@@ -11,7 +11,6 @@
 open Names
 open EConstr
 open Libnames
-open Globnames
 open Constrexpr
 open Newring_ast
 
@@ -19,7 +18,7 @@ val protect_tac_in : string -> Id.t -> unit Proofview.tactic
 
 val protect_tac : string -> unit Proofview.tactic
 
-val closed_term : EConstr.constr -> global_reference list -> unit Proofview.tactic
+val closed_term : EConstr.constr -> GlobRef.t list -> unit Proofview.tactic
 
 val add_theory :
   Id.t ->