diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-18 01:02:13 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-29 05:11:01 +0200 |
| commit | 778374f081163b4658b8a2efa72cb332179b3a7d (patch) | |
| tree | ecda5228a572447ab6e2fc551af4e32a27902da9 /plugins/ltac/tacinterp.ml | |
| 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/ltac/tacinterp.ml')
0 files changed, 0 insertions, 0 deletions