aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-04-14 11:12:00 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-06-03 15:28:49 +0200
commit56ff0c9c1475fdfe74af760e4e9fff96738c2c64 (patch)
treeb5608d0cdab6efd3831d2cd8ee7fbb18a55e2f94 /printing
parent582c1d2d152b696d0b7ec1ec8240436ae66ff326 (diff)
Cleaning, documentation, uniformisation of the Coq extension of List.
Still some discrepancies though. E.g.: - some functions taking an equality as arguments have suffix `_f` but not all; - the functions possibly raising an error have still different kinds of failure (Failure, Invalid_argument, Not_found or IndexOutOfRange, and when in the first two cases, with no unique rules in the style of the associated string - we thus avoid to document the exact string used). There are a few semantics changes: - skipn_at_least now raises a `Failure` if its argument is negative; - map3 raises an Invalid_argument "List.map3" rather than Invalid_argument "map3" and similarly for map4 - internally, map3 and map4 are now tail-recursive (by uniformity); - internally, split3 and combine3 are now tail-recursive (by uniformity); - filter is now "smart" by default and smartfilter is deprecated; - smartmap is now tail-recursive by default.
Diffstat (limited to 'printing')
0 files changed, 0 insertions, 0 deletions