aboutsummaryrefslogtreecommitdiff
path: root/lib/util.mli
diff options
context:
space:
mode:
Diffstat (limited to 'lib/util.mli')
-rw-r--r--lib/util.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/lib/util.mli b/lib/util.mli
index dc6498b15c..49e1fb4bd9 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -196,6 +196,7 @@ val array_for_all3 : ('a -> 'b -> 'c -> bool) ->
'a array -> 'b array -> 'c array -> bool
val array_for_all4 : ('a -> 'b -> 'c -> 'd -> bool) ->
'a array -> 'b array -> 'c array -> 'd array -> bool
+val array_for_all_i : (int -> 'a -> bool) -> int -> 'a array -> bool
val array_hd : 'a array -> 'a
val array_tl : 'a array -> 'a array
val array_last : 'a array -> 'a