diff options
| author | Hugo Herbelin | 2017-08-18 01:02:13 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-08-29 05:11:01 +0200 |
| commit | 778374f081163b4658b8a2efa72cb332179b3a7d (patch) | |
| tree | ecda5228a572447ab6e2fc551af4e32a27902da9 /plugins/syntax | |
| parent | c4e3c884316a1156d6707fc7011b6e2f2e7428f0 (diff) | |
Canonically renaming fold_map into fold_left_map in library Option.
Also adding fold_right_map by consistency.
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions