diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proofview.ml | 4 | ||||
| -rw-r--r-- | proofs/proofview.mli | 2 |
2 files changed, 6 insertions, 0 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 0dbbdca7cb..338a8eede8 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -647,6 +647,10 @@ module Notations = struct end open Notations + +module Monad = + Monad.Make(struct type +'a t = 'a tactic let return=tclUNIT let (>>=)=(>>=) end) + let rec list_map f = function | [] -> tclUNIT [] | a::l -> diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 60a6c558cf..eba6734390 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -260,6 +260,8 @@ val tclTIMEOUT : int -> 'a tactic -> 'a tactic (** [mark_as_unsafe] signals that the current tactic is unsafe. *) val mark_as_unsafe : unit tactic +module Monad : Monad.S with type +'a t = 'a tactic + val list_map : ('a -> 'b tactic) -> 'a list -> 'b list tactic (*** Commands ***) |