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/term_typing.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'kernel/term_typing.ml')

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 57d4a287b0..b8c32ffe56 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -174,7 +174,6 @@ let build_constant_declaration kn env (def,typ,cst,inline_code,ctx) =
     const_type = typ;
     const_body_code = Cemitcodes.from_val (compile_constant_body env def);
     const_constraints = cst;
-    const_native_name = ref NotLinked;
     const_inline_code = inline_code }
 
 (*s Global and local constant declaration. *)
-- 
cgit v1.2.3