3 files changed, 6 insertions, 6 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index c5cd28d02..39f7de942 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
 
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli
index 684983a87..96efa7faa 100644
--- a/kernel/nativecode.mli
+++ b/kernel/nativecode.mli
@@ -67,7 +67,7 @@ val register_native_file : string -> unit
 val compile_constant_field : env -> string -> Constant.t ->
   global list -> constant_body -> global list
 
-val compile_mind_field : string -> ModPath.t -> Label.t ->
+val compile_mind_field : ModPath.t -> Label.t ->
   global list -> mutual_inductive_body -> global list
 
 val mk_conv_code : env -> evars -> string -> constr -> constr -> linkable_code
diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml
index 8bff43632..edce9367f 100644
--- a/kernel/nativelibrary.ml
+++ b/kernel/nativelibrary.ml
@@ -37,7 +37,7 @@ and translate_field prefix mp env acc (l,x) =
 	let id = mb.mind_packets.(0).mind_typename in
 	let msg = Printf.sprintf "Compiling inductive %s..." (Id.to_string id) in
 	Feedback.msg_debug (Pp.str msg));
-     compile_mind_field prefix mp l acc mb
+     compile_mind_field mp l acc mb
   | SFBmodule md ->
      let mp = md.mod_mp in
      (if !Flags.debug then