Adding a tclUPDATE_ENV primitive and using it in in tclABSTRACT.

Hopefully, this may fix some nasty bugs lying around.

4 files changed, 11 insertions, 0 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index f10843e7ae..c3d7e13e20 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -547,6 +547,8 @@ let tclEVARMAP =
 
 let tclENV = Proof.current
 
+let tclUPDATE_ENV = Proof.update
+
 let tclEFFECTS eff =
   Proof.modify (fun initial -> emit_side_effects eff initial)
 
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index f59ad0dc14..0f976d2f38 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -248,6 +248,11 @@ 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/proofs/proofview_monad.ml b/proofs/proofview_monad.ml
index 3781324a69..9be26ab2b2 100644
--- a/proofs/proofview_monad.ml
+++ b/proofs/proofview_monad.ml
@@ -253,6 +253,9 @@ struct
   let current : rt tactic = (); fun s ->
     { iolist = fun nil cons -> cons (s.rstate, s) nil }
 
+  let update (rstate : rt) : unit tactic = (); fun s ->
+    { iolist = fun nil cons -> cons ((), { s with rstate }) nil }
+
   let put (w : wt) : unit tactic = (); fun s ->
     { iolist = fun nil cons -> cons ((), { s with wstate = merge w s.wstate }) nil }
 
diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli
index a459db424d..e1d9b4fa1b 100644
--- a/proofs/proofview_monad.mli
+++ b/proofs/proofview_monad.mli
@@ -134,6 +134,7 @@ module Logical : sig
   val modify : (logicalState -> logicalState) -> unit t
   val put : logicalMessageType -> unit t
   val current : logicalEnvironment t
+  val update : logicalEnvironment -> unit t
 
   val zero : exn -> 'a t
   val plus : 'a t -> (exn -> 'a t) -> 'a t