From 20ed9460ec30d7b02aa074c234014f0f2d86ecd3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 12 May 2020 15:06:28 +0200
Subject: Write the outermost part of the legacy refiner directly in the monad.

---
 proofs/logic.ml | 31 +++++++++++++------------------
 1 file changed, 13 insertions(+), 18 deletions(-)

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 812fd1d769..c7a1c32e7c 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -565,23 +565,18 @@ let convert_hyp ~check ~reorder env sigma d =
 (************************************************************************)
 (* Primitive tactics are handled here *)
 
-let prim_refiner ~check r sigma goal =
-  let env = Goal.V82.env sigma goal in
-  let cl = Goal.V82.concl sigma goal in
+let refiner ~check r =
+  let open Proofview.Notations in
+  Proofview.Goal.enter begin fun gl ->
+  let sigma = Proofview.Goal.sigma gl in
+  let env = Proofview.Goal.env gl in
+  let st = Proofview.Goal.state gl in
+  let cl = Proofview.Goal.concl gl in
   check_meta_variables env sigma r;
   let (sgl,cl',sigma,oterm) = mk_refgoals ~check env sigma [] cl r in
-  let sgl = List.rev sgl in
-  let sigma = Goal.V82.partial_solution env sigma goal (EConstr.of_constr oterm) in
-  { Evd.it = sgl; Evd.sigma = sigma; }
-
-let refiner ~check r { Evd.sigma = sigma; Evd.it = goal } =
-  prim_refiner ~check r sigma goal
-
-(* Profiling refiner *)
-let refiner ~check =
-  if Flags.profile then
-    let refiner_key = CProfile.declare_profile "refiner" in
-      CProfile.profile2 refiner_key (refiner ~check)
-  else refiner ~check
-
-let refiner ~check c = Proofview.V82.tactic ~nf_evars:false (refiner ~check c)
+  let map gl = Proofview.goal_with_state gl st in
+  let sgl = List.rev_map map sgl in
+  let sigma = Goal.V82.partial_solution env sigma (Proofview.Goal.goal gl) (EConstr.of_constr oterm) in
+  Proofview.Unsafe.tclEVARS sigma <*>
+  Proofview.Unsafe.tclSETGOALS sgl
+  end
-- 
cgit v1.2.3