diff options
Diffstat (limited to 'lib/util.mli')
| -rw-r--r-- | lib/util.mli | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/lib/util.mli b/lib/util.mli index abfab29d5..a7586547e 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -118,12 +118,6 @@ val intmap_inv : 'a Intmap.t -> 'a -> int list val interval : int -> int -> int list - -(** In [map_succeed f l] an element [a] is removed if [f a] raises - [Failure _] otherwise behaves as [List.map f l] *) - -val map_succeed : ('a -> 'b) -> 'a list -> 'b list - (** {6 Memoization. } *) (** General comments on memoization: |