diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-18 01:02:48 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-29 05:11:01 +0200 |
| commit | 6b4d8df891ff964fb267eec54337a96ccc610ef3 (patch) | |
| tree | d6768928a89761a1c3e5deeef04b8c9e4129d36f /configure.ml | |
| parent | 0c133afc50ccfda19c4952abf579b6d94ab5f229 (diff) | |
Canonically renaming fold_map into fold_left_map in library Name.
Also adding fold_right_map by consistency.
Diffstat (limited to 'configure.ml')
0 files changed, 0 insertions, 0 deletions