diff options
| author | Arnaud Spiwack | 2014-08-05 15:51:16 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-08-05 16:52:14 +0200 |
| commit | 664b3cba1e8d326382ca981aa49fdf00edd429e6 (patch) | |
| tree | 462c7a7e2cc4c0becb5259feb1c25ca10bcdd5c9 /proofs/proofview_monad.mli | |
| parent | 1624735620d7e375a124231fea94648eac0da342 (diff) | |
Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter].
When "entering" in a goal, the environment observed by [tclENV] is changed (in the scope of the goal) to be that of the goal.
I'm not entirely sure it is the right semantics. But it allows to write tactics which are agnostic of whether they are run in a goal or not.
Diffstat (limited to 'proofs/proofview_monad.mli')
| -rw-r--r-- | proofs/proofview_monad.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli index ab92a57fcd..07d61375ec 100644 --- a/proofs/proofview_monad.mli +++ b/proofs/proofview_monad.mli @@ -131,6 +131,8 @@ module Logical : sig val modify : (logicalState -> logicalState) -> unit t val put : logicalMessageType -> unit t val current : logicalEnvironment t + val set_local : logicalEnvironment -> 'a t -> 'a t + val modify_local : (logicalEnvironment->logicalEnvironment) -> 'a t -> 'a t val zero : exn -> 'a t val plus : 'a t -> (exn -> 'a t) -> 'a t |