Merge PR #12227: Spring cleaning of the tactic compatibility layer

Reviewed-by: gares

3 files changed, 7 insertions, 11 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 767f93787d..695e103082 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'))
+    (refiner ~check:false EConstr.Unsafe.(to_constr (clenv_cast_meta clenv (clenv_value clenv))))
   end
 
 let clenv_pose_dependent_evars ?(with_evars=false) clenv =
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 75c3436cf4..29a47c5acd 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -37,6 +37,8 @@ let refiner ~check =
       CProfile.profile2 refiner_key (refiner ~check)
   else refiner ~check
 
+let refiner ~check c = Proofview.V82.tactic ~nf_evars:false (refiner ~check c)
+
 (*********************)
 (*   Tacticals       *)
 (*********************)
@@ -269,5 +271,3 @@ let tclAT_LEAST_ONCE t = (tclTHEN t (tclREPEAT t))
 
 (* Change evars *)
 let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma}
-let tclPUSHEVARUNIVCONTEXT ctx gl =
-  tclEVARS (Evd.merge_universe_context (project gl) ctx) gl
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 66eae1db81..3471f38e9e 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -22,7 +22,7 @@ val project : 'a sigma -> evar_map
 val pf_env  : Goal.goal sigma -> Environ.env
 val pf_hyps : Goal.goal sigma -> named_context
 
-val refiner : check:bool -> Constr.t -> tactic
+val refiner : check:bool -> Constr.t -> unit Proofview.tactic
 
 (** {6 Tacticals. } *)
 
@@ -32,7 +32,6 @@ val tclIDTAC_MESSAGE  : Pp.t -> tactic
 
 (** [tclEVARS sigma] changes the current evar map *)
 val tclEVARS : evar_map -> tactic
-val tclPUSHEVARUNIVCONTEXT : UState.t -> tactic
 
 
 (** [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies