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/nativelibrary.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/nativelibrary.ml')

diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml
index 8bff436322..edce9367fc 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
-- 
cgit v1.2.3