From 04a8c766a51b17997d8a9ffcf6f2d7beffc599ce Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 30 Apr 2020 15:35:40 +0200
Subject: Remove a critical call to V82.tactic in Clenvtac.

Despite being marked as a breaking change by myself, it seems that the
underlying condition had been solved in the meantime.
---
 proofs/clenvtac.ml | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

(limited to 'proofs')

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 767f93787d..197d69a481 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -61,10 +61,7 @@ let clenv_pose_dependent_evars ?(with_evars=false) clenv =
   clenv_pose_metas_as_evars clenv dep_mvs
 
 let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv =
-  (* ppedrot: a Goal.enter here breaks things, because the tactic below may
-     solve goals by side effects, while the compatibility layer keeps those
-     useless goals. That deserves a FIXME. *)
-  Proofview.V82.tactic begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let clenv, evars = clenv_pose_dependent_evars ~with_evars clenv in
   let evd' =
     if with_classes then
@@ -78,9 +75,9 @@ let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv =
     else clenv.evd
   in
   let clenv = { clenv with evd = evd' } in
-  tclTHEN
-    (tclEVARS (Evd.clear_metas evd'))
-    (refiner ~check:false EConstr.Unsafe.(to_constr (clenv_cast_meta clenv (clenv_value clenv)))) gl
+  Proofview.tclTHEN
+    (Proofview.Unsafe.tclEVARS (Evd.clear_metas evd'))
+    (Proofview.V82.tactic (refiner ~check:false EConstr.Unsafe.(to_constr (clenv_cast_meta clenv (clenv_value clenv)))))
   end
 
 let clenv_pose_dependent_evars ?(with_evars=false) clenv =
-- 
cgit v1.2.3