diff options
| author | Pierre-Marie Pédrot | 2014-09-05 14:40:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-09-05 15:32:03 +0200 |
| commit | 581cbe36191901f1dc234fe77d619abfe7b8de34 (patch) | |
| tree | 9d160ef01f541970d2a9fd6788a3377622794600 /lib/monad.ml | |
| parent | 466c25ea43149deedf50e0105a6d1e69db91c8fd (diff) | |
Adding a Ftactic module for potentially focussing tactics.
The code for the module was moved from Tacinterp. We still expose partially
the implementation of the Ftactic.t type, for the sake of simplicity. It may
be dangerous if used improperly though.
Diffstat (limited to 'lib/monad.ml')
| -rw-r--r-- | lib/monad.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/lib/monad.ml b/lib/monad.ml index 7636b1630c..d4641194ee 100644 --- a/lib/monad.ml +++ b/lib/monad.ml @@ -24,6 +24,13 @@ module type Def = sig end +module type ListS = sig + type 'a t + val map : ('a -> 'b t) -> 'a list -> 'b list t + val map_right : ('a -> 'b t) -> 'a list -> 'b list t + val fold_right : ('a -> 'b -> 'b t) -> 'a list -> 'b -> 'b t + val fold_left : ('a -> 'b -> 'a t) -> 'a -> 'b list -> 'a t +end module type S = sig |