Adding an [modify] function to the tactic monad. It allows to modify

the current state without having to use both get, bind and set.

3 files changed, 30 insertions, 21 deletions

diff --git a/bootstrap/Monads.v b/bootstrap/Monads.v
index a160aaa87e..10defd0f98 100644
--- a/bootstrap/Monads.v
+++ b/bootstrap/Monads.v
@@ -130,7 +130,8 @@ Notation "'do' M x ':=' e 'in' u" := (bind _ M e (fun x => u)).
 
 Record State (S:Set) (T:Set->Set) := {
   set : S -> T unit;
-  get : T S
+  get : T S ;
+  modify : (S -> S) -> T unit
 }.
 
 (* spiwack: Environment and Writer are given distinct interfaces from
@@ -318,7 +319,8 @@ Section Common.
 
  Definition State : State S T := {|
    set s := (fun R k _ => k () s) : T unit  ;
-   get := fun R k s => k s s
+   get := fun R k s => k s s ;
+   modify := fun f R k s => k () (f s)
  |}.
 
  Definition lift {A} (x:T₀ A) : T A := fun R k s =>
@@ -681,6 +683,7 @@ Module Logical.
 
  Definition set (s:LogicalState) : t unit := Eval compute in freeze _ (set _ _ LogicalStateM s).
  Definition get : t LogicalState := Eval compute in get _ _ LogicalStateM.
+ Definition modify (f : LogicalState -> LogicalState) : t unit := Eval compute in freeze _ (modify _ _ LogicalStateM f).
  Definition put (m:LogicalMessageType) : t unit := Eval compute in freeze _ (put _ _ LogicalWriter m).
  Definition current : t LogicalEnvironment := Eval compute in current _ _ LogicalReader.
 
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
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-