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/proofview_gen.ml | |
| 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/proofview_gen.ml')
| -rw-r--r-- | proofs/proofview_gen.ml | 24 |
1 files changed, 24 insertions, 0 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 -> |