From 00869a1b9ccda40406b0de18e2636fc400aa785f Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 31 Aug 2017 16:27:36 +0200
Subject: Nativecode.pp_mllam internal pp_letrec: remove unused argument.

---
 kernel/nativecode.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'kernel/nativecode.ml')

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 1748e98a41..c5cd28d02f 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 =
-- 
cgit v1.2.3


From d9d456f310633c5d2f5de99203763c276774df98 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 31 Aug 2017 16:39:50 +0200
Subject: Nativecode compile_mind, compile_mind_field: remove unused arguments

---
 kernel/nativecode.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'kernel/nativecode.ml')

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index c5cd28d02f..39f7de9426 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1941,7 +1941,7 @@ let is_code_loaded ~interactive name =
 let param_name = Name (Id.of_string "params")
 let arg_name = Name (Id.of_string "arg")
 
-let compile_mind prefix ~interactive mb mind stack =
+let compile_mind mb mind stack =
   let u = Declareops.inductive_polymorphic_context mb in
   (** Generate data for every block *)
   let f i stack ob =
@@ -2020,7 +2020,7 @@ let compile_mind_deps env prefix ~interactive
   then init
   else
     let comp_stack =
-      compile_mind prefix ~interactive mib mind comp_stack
+      compile_mind mib mind comp_stack
     in
     let name =
       if interactive then LinkedInteractive prefix
@@ -2092,9 +2092,9 @@ let compile_constant_field env prefix con acc cb =
     in
     gl@acc
 
-let compile_mind_field prefix mp l acc mb =
+let compile_mind_field mp l acc mb =
   let mind = MutInd.make2 mp l in
-  compile_mind prefix ~interactive:false mb mind acc
+  compile_mind mb mind acc
 
 let mk_open s = Gopen s
 
-- 
cgit v1.2.3