aboutsummaryrefslogtreecommitdiff
path: root/clib/cArray.mli
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2018-10-04 11:02:11 +0200
committerPierre-Marie Pédrot2018-10-04 11:02:11 +0200
commit07ae306b9601653a6edbdefd1b3b5275439611bf (patch)
tree6aa47f0ef54b32e78fde48802f218eec924b09bf /clib/cArray.mli
parent4b2c12fddf2dfad949eea44326da87b11f614772 (diff)
parente11068aa90f6e7fc728d4583998cd99cfa850211 (diff)
Merge PR #8581: [pretyper] Remove imperative passing of evar_map.
Diffstat (limited to 'clib/cArray.mli')
-rw-r--r--clib/cArray.mli4
1 files changed, 4 insertions, 0 deletions
diff --git a/clib/cArray.mli b/clib/cArray.mli
index 5c7e09eeac..163191681a 100644
--- a/clib/cArray.mli
+++ b/clib/cArray.mli
@@ -114,6 +114,10 @@ sig
val fold_left2_map : ('a -> 'b -> 'c -> 'a * 'd) -> 'a -> 'b array -> 'c array -> 'a * 'd array
(** Same with two arrays, folding on the left; see also [Smart.fold_left2_map] *)
+ val fold_left2_map_i :
+ (int -> 'a -> 'b -> 'c -> 'a * 'd) -> 'a -> 'b array -> 'c array -> 'a * 'd array
+ (** Same than [fold_left2_map] but passing the index of the array *)
+
val fold_right2_map : ('a -> 'b -> 'c -> 'd * 'c) -> 'a array -> 'b array -> 'c -> 'd array * 'c
(** Same with two arrays, folding on the left *)