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).---
 lib/genarg.mli | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'lib/genarg.mli')

diff --git a/lib/genarg.mli b/lib/genarg.mli
index 6eea3ac926..45f0dddf2c 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -186,6 +186,16 @@ val app_pair :
       ('a generic_argument -> 'b generic_argument)
    -> 'a generic_argument -> 'b generic_argument
 
+module Monadic (M:Monad.S) : sig
+
+  (** [Monadic.app_list f x] maps the monadic computation [f] on
+      elements of [x], provided [x] has the tag [List0 t] for some [t]. It
+      fails otherwise. *)
+  val app_list : ('a generic_argument -> 'b generic_argument M.t) ->
+    'a generic_argument -> 'b generic_argument M.t
+
+end
+
 (** {6 Type reification} *)
 
 type argument_type =
-- 
cgit v1.2.3