From f34dcb97406611704c93970ea623d6a8587e5ba8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 26 Jun 2020 12:43:23 +0200
Subject: Moving the remaining Refiner functions to Tacmach.

---
 plugins/setoid_ring/newring.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/setoid_ring')

diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index e7c75e029e..878f7a834e 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -201,7 +201,7 @@ 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 = Evd.minimize_universes (Refiner.project gls) in
+  let evd = Evd.minimize_universes gls.Evd.sigma in
   let nf c = constr_of evd c in
   Array.map nf !tactic_res, Evd.universe_context_set evd
 
-- 
cgit v1.2.3