From d3eac3d5fc8e5af499eb8750ca08ead8562dac6f Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sat, 28 Dec 2013 20:39:17 -0500
Subject: Removing native_name reference from constant_body.

For now, this reference (renamed to link_info) has been moved to the
environment (for constants and inductive types). But this is only a first step
towards making the native compiler more functional.
---
 kernel/nativelibrary.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/nativelibrary.mli')

diff --git a/kernel/nativelibrary.mli b/kernel/nativelibrary.mli
index 3f413631c1..a45402a437 100644
--- a/kernel/nativelibrary.mli
+++ b/kernel/nativelibrary.mli
@@ -14,7 +14,7 @@ open Nativecode
 compiler *)
 
 val dump_library : module_path -> dir_path -> env -> module_signature ->
-  global list * symbol array * code_location_updates
+  global list * symbol array
 
 val compile_library :
   dir_path -> global list -> string list -> string -> int
-- 
cgit v1.2.3