Remove unsafe code (Obj.magic) in Tacinterp.

This commit also introduces a module Monad to generate monadic combinators (currently, only List.map).

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 ***)