2 files changed, 20 insertions, 0 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 0e53ff1318..c93ec3b234 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -826,6 +826,22 @@ type 'a sigma = {
 let sig_it x = x.it
 let sig_sig x = x.sigma
 
+(*******************************************************************)
+(* The state monad with state an evar map. *)
+
+module Monad =
+  Monad.Make (struct
+
+    type +'a t = evar_map -> 'a * evar_map
+
+    let return a = fun s -> (a,s)
+
+    let (>>=) x f = fun s ->
+      let (a,s') = x s in
+      f a s'
+
+  end)
+
 (**********************************************************)
 (* Failure explanation *)
 
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 58e4cd630b..0e65b151c4 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -274,6 +274,10 @@ type 'a sigma = {
 val sig_it  : 'a sigma -> 'a
 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
+
 (** {5 Meta machinery}
 
     These functions are almost deprecated. They were used before the