aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/lemmas.mli
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-12-13 01:05:41 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-12-13 17:48:45 +0100
commit742bd7e29dead13617090a146a7c98f0e1ffe0c8 (patch)
treeb7a160c91d7339f4222e3d69aaf06a58f6ef7681 /vernac/lemmas.mli
parent7799626c67c39c6bd2c5faf247456efb2c26ae82 (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