aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-01-01 23:33:40 +0100
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-01-01 23:33:40 +0100
commitc671a5cb30db29feda56f008d45789c2fd4928e9 (patch)
tree97d832c2d28b30962c625d80116b569cfe7de1ad /lib
parentbfdf6d2db29972ff52a1870524a230fdecb636dc (diff)
Do not make it harder on the compiler optimizer by packing arguments.
Diffstat (limited to 'lib')
-rw-r--r--lib/cList.ml9
1 files changed, 5 insertions, 4 deletions
diff --git a/lib/cList.ml b/lib/cList.ml
index 72f892a09..bd3e09b5b 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -645,12 +645,13 @@ let rec split3 = function
let (rx, ry, rz) = split3 l in (x::rx, y::ry, z::rz)
let firstn n l =
- let rec aux acc = function
- | (0, l) -> List.rev acc
- | (n, (h::t)) -> aux (h::acc) (pred n, t)
+ let rec aux acc n l =
+ match n, l with
+ | 0, _ -> List.rev acc
+ | n, h::t -> aux (h::acc) (pred n) t
| _ -> failwith "firstn"
in
- aux [] (n,l)
+ aux [] n l
let rec last = function
| [] -> failwith "List.last"