From 1109581ba7afca804515fc6179565da808bae4f7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 30 Apr 2020 15:57:54 +0200
Subject: Wrap Refiner.refiner in the tactic monad.

This function was used almost everywhere with the wrapper around.
---
 plugins/funind/functional_principles_proofs.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 7b2ce671a3..f4200854c2 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -41,7 +41,10 @@ let observe_tac s = observe_tac (fun _ _ -> Pp.str s)
 let finish_proof dynamic_infos g =
   observe_tac "finish" (Proofview.V82.of_tactic assumption) g
 
-let refine c = Refiner.refiner ~check:true EConstr.Unsafe.(to_constr c)
+let refine c =
+  Proofview.V82.of_tactic
+    (Refiner.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