From 286984487d515cdb9f2e02834d23c65449760ba2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 6 Apr 2014 17:46:26 +0200
Subject: Adding an [modify] function to the tactic monad. It allows to modify
 the current state without having to use both get, bind and set.

---
 proofs/proofview_gen.ml    | 24 ++++++++++++++++++++++++
 proofs/proofview_monad.mli | 20 +-------------------
 2 files changed, 25 insertions(+), 19 deletions(-)

(limited to 'proofs')

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
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-- 
cgit v1.2.3