From 4d6b938e90ecd9dbfb29a0af28a7d8b6a657ae17 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 27 Feb 2014 13:50:57 +0100
Subject: Remove unsafe code (Obj.magic) in Tacinterp.

This commit also introduces a module Monad to generate monadic combinators (currently, only List.map).---
 proofs/proofview.ml  | 4 ++++
 proofs/proofview.mli | 2 ++
 2 files changed, 6 insertions(+)

(limited to 'proofs')

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 ***)
-- 
cgit v1.2.3