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 /stm/vio_checking.mli | |
parent | 0c133afc50ccfda19c4952abf579b6d94ab5f229 (diff) |
Canonically renaming fold_map into fold_left_map in library Name.
Also adding fold_right_map by consistency.
Diffstat (limited to 'stm/vio_checking.mli')
0 files changed, 0 insertions, 0 deletions