From e5b355107d985d7efe2976b9eee9b6c182e25f24 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 26 Jun 2020 12:36:43 +0200
Subject: Remove Refiner.refiner.

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

(limited to 'plugins/funind')

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 2151ad7873..9b578d4697 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -43,7 +43,7 @@ let finish_proof dynamic_infos g =
 
 let refine c =
   Proofview.V82.of_tactic
-    (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr c))
+    (Logic.refiner ~check:true EConstr.Unsafe.(to_constr c))
 
 let thin l = Proofview.V82.of_tactic (Tactics.clear l)
 let eq_constr sigma u v = EConstr.eq_constr_nounivs sigma u v
-- 
cgit v1.2.3