summaryrefslogtreecommitdiff
path: root/src/util.mli
diff options
context:
space:
mode:
Diffstat (limited to 'src/util.mli')
-rw-r--r--src/util.mli2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/util.mli b/src/util.mli
index 06fd5eff..ddc5347f 100644
--- a/src/util.mli
+++ b/src/util.mli
@@ -194,6 +194,8 @@ val drop : int -> 'a list -> 'a list
val take_drop : ('a -> bool) -> 'a list -> ('a list * 'a list)
+val find_next : ('a -> bool) -> 'a list -> ('a list * ('a * 'a list) option)
+
val list_init : int -> (int -> 'a) -> 'a list
(** {2 Files} *)