aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/util.ml
diff options
context:
space:
mode:
Diffstat (limited to 'lib/util.ml')
-rw-r--r--lib/util.ml5
1 files changed, 0 insertions, 5 deletions
diff --git a/lib/util.ml b/lib/util.ml
index 102541731..6f9f9bd83 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -441,11 +441,6 @@ let interval n m =
in
interval_n ([],m)
-
-let map_succeed f l =
- let filter x = try Some (f x) with Failure _ -> None in
- List.map_filter filter l
-
(*s Memoization *)
let memo1_eq eq f =