diff options
| author | Emilio Jesus Gallego Arias | 2018-09-27 22:04:28 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-03 13:52:04 +0200 |
| commit | e11068aa90f6e7fc728d4583998cd99cfa850211 (patch) | |
| tree | 98998fecef98931fea26e5de7d2156c4a6711d42 /clib/cArray.mli | |
| parent | f19d24a462d50c701a3882de2c16180bb739e622 (diff) | |
[pretyper] Remove imperative passing of evar_map.
Diffstat (limited to 'clib/cArray.mli')
| -rw-r--r-- | clib/cArray.mli | 4 |
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 *) |