diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-13 01:05:41 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-13 17:48:45 +0100 |
commit | 742bd7e29dead13617090a146a7c98f0e1ffe0c8 (patch) | |
tree | b7a160c91d7339f4222e3d69aaf06a58f6ef7681 /vernac/lemmas.mli | |
parent | 7799626c67c39c6bd2c5faf247456efb2c26ae82 (diff) |
[lib] Auxiliary functions in List + fixes.
These are convenient to use `command.ml` for example.
We also fix a critical bug in the `fold_left_map` family of functions,
as witnessed by this old behavior.
```ocaml
fold_left2_map (fun c u v -> c+1,u+v) 0 [1;2;3] [1;2;3;];;
- : int * int list = (3, [6; 4; 2])
```
I have opted for a simple fix keeping the tail-recursive nature, I am
not in the mood of writing base libraries, but feel free to improve.
Diffstat (limited to 'vernac/lemmas.mli')
0 files changed, 0 insertions, 0 deletions