Remove unsafe code (Obj.magic) in Tacinterp.

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

1 files changed, 4 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 ->