diff options
| author | Hugo Herbelin | 2017-08-17 12:57:27 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-08-29 05:10:40 +0200 |
| commit | 2ad320f630e138fc608af836a744a4704be42558 (patch) | |
| tree | 0d4b0c130dc986d0b7d982139f60a5302e548c99 /kernel | |
| parent | 7b1ff0c70a3ba9cd3cfa5aa6723f8f8a2b6e5396 (diff) | |
Adding combinators + a canonical renaming in cList.ml.
- Adding fold_left2_map/fold_right2_map.
- Canonically renaming fold_map/fold_map' into fold_left_map/fold_right_map.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions