Tacinterp: refactoring using Monad.

Adds a combinator List.map_right which chains effects from right to left.

2 files changed, 15 insertions, 1 deletions

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index c93ec3b234..d6c9a2097f 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -829,6 +829,19 @@ let sig_sig x = x.sigma
 (*******************************************************************)
 (* The state monad with state an evar map. *)
 
+module MonadR =
+  Monad.Make (struct
+
+    type +'a t = evar_map -> evar_map * 'a
+
+    let return a = fun s -> (s,a)
+
+    let (>>=) x f = fun s ->
+      let (s',a) = x s in
+      f a s'
+
+  end)
+
 module Monad =
   Monad.Make (struct
 
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 0e65b151c4..2b0e9ca684 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -276,7 +276,8 @@ val sig_sig : 'a sigma -> evar_map
 
 (** {5 The state monad with state an evar map} *)
 
-module Monad : Monad.S with type +'a t = evar_map -> 'a * evar_map
+module MonadR : Monad.S with type +'a t = evar_map -> evar_map * 'a
+module Monad  : Monad.S with type +'a t = evar_map -> 'a * evar_map
 
 (** {5 Meta machinery}