Make tclEFFECTS also update the env in the proof monad

3 files changed, 5 insertions, 10 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 365591242a..9f8458ba79 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -565,10 +565,12 @@ let tclEVARMAP =
 
 let tclENV = Proof.current
 
-let tclUPDATE_ENV = Proof.update
-
 let tclEFFECTS eff =
-  Proof.modify (fun initial -> emit_side_effects eff initial)
+  Proof.bind (Proof.ret ())
+    (fun () -> (* The Global.env should be taken at exec time *)
+       Proof.seq
+         (Proof.update (Global.env ()))
+         (Proof.modify (fun initial -> emit_side_effects eff initial)))
 
 exception Timeout
 let _ = Errors.register_handler begin function
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index a1213cde25..0eae9b6056 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -247,11 +247,6 @@ val tclEVARMAP : Evd.evar_map tactic
    environment is returned by {!Proofview.Goal.env}. *)
 val tclENV : Environ.env tactic
 
-(* [tclUPDATE_ENV e] modifies the global environment of the tactic. It is
-   required by workarounds like the [abstract] tactical. Not to be used by the
-   casual user. *)
-val tclUPDATE_ENV : Environ.env -> unit tactic
-
 (* [tclEFFECTS eff] add the effects [eff] to the current state. *)
 val tclEFFECTS : Declareops.side_effects -> unit tactic
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5b329a3fa4..cc95430f5a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4107,8 +4107,6 @@ let abstract_subproof id gk tac =
   let solve =
     Proofview.V82.tclEVARS evd <*>
     Proofview.tclEFFECTS effs <*>
-    (** Hack around *)
-    Proofview.tclUPDATE_ENV (Global.env ()) <*>
     new_exact_no_check (applist (lem, args))
   in
   if not safe then Proofview.mark_as_unsafe <*> solve else solve