diff options
| -rw-r--r-- | proofs/proofview.ml | 2 | ||||
| -rw-r--r-- | proofs/proofview.mli | 5 | ||||
| -rw-r--r-- | proofs/proofview_monad.ml | 3 | ||||
| -rw-r--r-- | proofs/proofview_monad.mli | 1 | ||||
| -rw-r--r-- | tactics/tactics.ml | 9 |
5 files changed, 18 insertions, 2 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index f10843e7a..c3d7e13e2 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 f59ad0dc1..0f976d2f3 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 3781324a6..9be26ab2b 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 a459db424..e1d9b4fa1 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 diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 0c69f5088..77876e626 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3939,8 +3939,13 @@ let abstract_subproof id gk tac = let effs = cons_side_effects eff Entries.(snd (Future.force const.const_entry_body)) in let args = List.rev (instance_from_named_context sign) in - let solve = Proofview.V82.tclEVARS evd <*> - Proofview.tclEFFECTS effs <*> new_exact_no_check (applist (lem, args)) in + 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 end |