Adding a tclEFFECTS primitive allowing to push STM side-effects in tactics.

3 files changed, 3 insertions, 12 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 85546619e3..d7f0dd83f4 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -343,7 +343,7 @@ let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars d
   let type_of_cls = type_of_clause cls gl in
   let dep = dep_proof_ok && dep_fun c type_of_cls in
   let (elim,effs) = find_elim hdcncl lft2rgt dep cls (Some t) gl in
-  Proofview.V82.tactic (Tactics.emit_side_effects effs) <*>
+  Proofview.tclEFFECTS effs <*>
   general_elim_clause with_evars frzevars tac cls c t l
     (match lft2rgt with None -> false | Some b -> b)
     {elimindex = None; elimbody = (elim,NoBindings)}
@@ -861,7 +861,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn sort =
   let pf_ty = mkArrow eqn absurd_term in
   let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in
   let pf = clenv_value_cast_meta absurd_clause in
-  Proofview.V82.tactic (Tactics.emit_side_effects eff) <*>
+  Proofview.tclEFFECTS eff <*>
   tclTHENS (cut_intro absurd_term)
     [onLastHypId gen_absurdity; (Proofview.V82.tactic (refine pf))]
 
@@ -1231,9 +1231,8 @@ let inject_if_homogenous_dependent_pair env sigma (eq,_,(t,t1,t2)) =
     let inj2 = Coqlib.coq_constant "inj_pair2_eq_dec is missing"
       ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in
     let c, eff = find_scheme (!eq_dec_scheme_kind_name()) ind in
-    let sigma = Evd.emit_side_effects eff (Proofview.Goal.sigma gl) in
       (* cut with the good equality and prove the requested goal *)
-    tclTHENS (tclTHEN (Proofview.V82.tclEVARS sigma) (cut (mkApp (ceq,new_eq_args))))
+    tclTHENS (tclTHEN (Proofview.tclEFFECTS eff) (cut (mkApp (ceq,new_eq_args))))
       [tclIDTAC; tclTHEN (Proofview.V82.tactic (apply (
         mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3)|])
        ))) (Auto.trivial [] [])
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 1f88ed6453..aeac5e2642 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3879,12 +3879,6 @@ let unify ?(state=full_transparent_state) x y gl =
     in tclEVARS evd gl
   with e when Errors.noncritical e -> tclFAIL 0 (str"Not unifiable") gl
 
-let emit_side_effects eff gl =
-(* Declareops.iter_side_effects (fun e ->
-    prerr_endline ("emitting: " ^ Declareops.string_of_side_effect e))
-    eff; *)
-  { it = [gl.it] ; sigma = Evd.emit_side_effects eff gl.sigma; }
-
 module Simple = struct
   (** Simplified version of some of the above tactics *)
 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 9f4f0e9ce1..671343b128 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -394,8 +394,6 @@ val declare_intro_decomp_eq :
    (types * constr * constr) ->
    clausenv -> unit Proofview.tactic) -> unit
 
-val emit_side_effects : Declareops.side_effects -> tactic
-
 module Simple : sig
   (** Simplified version of some of the above tactics *)