diff options
| author | Pierre-Marie Pédrot | 2014-04-06 17:46:26 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-04-06 18:11:27 +0200 |
| commit | 286984487d515cdb9f2e02834d23c65449760ba2 (patch) | |
| tree | fc6dcbdacd72be59aea3e5082da1d7dc1b65dfac /proofs | |
| parent | 3ace2a027b72ab6328cf844281ad90bfe383f0da (diff) | |
Adding an [modify] function to the tactic monad. It allows to modify
the current state without having to use both get, bind and set.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proofview_gen.ml | 24 | ||||
| -rw-r--r-- | proofs/proofview_monad.mli | 20 |
2 files changed, 25 insertions, 19 deletions
diff --git a/proofs/proofview_gen.ml b/proofs/proofview_gen.ml index 92012d58b1..80ab416425 100644 --- a/proofs/proofview_gen.ml +++ b/proofs/proofview_gen.ml @@ -345,6 +345,30 @@ module Logical = let get r k s = Obj.magic k s s + (** val modify : + (logicalState -> logicalState) -> __ -> (unit -> proofview -> __ -> + ('a1 -> __ -> (__ -> (bool*(Goal.goal list*Goal.goal list)) -> __ -> + (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ + IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> (__ -> (exn -> __ + IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ + IOBase.coq_T) -> Environ.env -> __ -> (__ -> (bool*(Goal.goal + list*Goal.goal list)) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ + IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> + (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ + IOBase.coq_T) -> __ IOBase.coq_T) -> proofview -> __ -> ('a1 -> __ -> + ('a2 -> (bool*(Goal.goal list*Goal.goal list)) -> __ -> (__ -> (exn -> + __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ + IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ + IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> + Environ.env -> __ -> ('a2 -> (bool*(Goal.goal list*Goal.goal list)) -> + __ -> ('a3 -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> + __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> ('a3 -> (exn -> 'a4 + IOBase.coq_T) -> 'a4 IOBase.coq_T) -> (exn -> 'a4 IOBase.coq_T) -> 'a4 + IOBase.coq_T **) + + let modify f = + (); (fun _ k s -> Obj.magic k () (f s)) + (** val put : logicalMessageType -> __ -> (unit -> proofview -> __ -> ('a1 -> __ -> (__ -> (bool*(Goal.goal list*Goal.goal list)) -> __ -> (__ -> (exn -> diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli index fa4392368c..26c6a301e6 100644 --- a/proofs/proofview_monad.mli +++ b/proofs/proofview_monad.mli @@ -57,6 +57,7 @@ module Logical : sig val set : logicalState -> unit t val get : logicalState t + val modify : (logicalState -> logicalState) -> unit t val put : logicalMessageType -> unit t val current : logicalEnvironment t @@ -68,22 +69,3 @@ module Logical : sig val run : 'a t -> logicalEnvironment -> logicalState -> (('a*logicalState)*logicalMessageType) NonLogical.t end - - - - - - - - - - - - - - - - - - - |