aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-08-31 16:27:36 +0200
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-07-03 13:36:05 +0200
commit00869a1b9ccda40406b0de18e2636fc400aa785f (patch)
tree38c6df8f5f024049f6270c3f9621842a35a18fca
parent461bdc02eb7e879fac3217e127e565b2623aec45 (diff)
Nativecode.pp_mllam internal pp_letrec: remove unused argument.
-rw-r--r--kernel/nativecode.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 1748e98a4..c5cd28d02 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1649,15 +1649,15 @@ let pp_mllam fmt l =
and pp_letrec fmt defs =
let len = Array.length defs in
- let pp_one_rec i (fn, argsn, body) =
+ let pp_one_rec (fn, argsn, body) =
Format.fprintf fmt "%a%a =@\n %a"
pp_lname fn
pp_ldecls argsn pp_mllam body in
Format.fprintf fmt "@[let rec ";
- pp_one_rec 0 defs.(0);
+ pp_one_rec defs.(0);
for i = 1 to len - 1 do
Format.fprintf fmt "@\nand ";
- pp_one_rec i defs.(i)
+ pp_one_rec defs.(i)
done;
and pp_blam fmt l =