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/declareops.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'kernel/declareops.ml')

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 724f290926..2e691491a8 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -65,7 +65,6 @@ let subst_const_body sub cb = {
   const_type = subst_const_type sub cb.const_type;
   const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code;
   const_constraints = cb.const_constraints;
-  const_native_name = ref NotLinked;
   const_inline_code = cb.const_inline_code }
 
 (** {7 Hash-consing of constants } *)
@@ -201,8 +200,7 @@ let subst_mind sub mib =
     else
       { mib with
         mind_params_ctxt = params';
-        mind_packets = packets';
-        mind_native_name = ref NotLinked }
+        mind_packets = packets' }
 
 (** {6 Hash-consing of inductive declarations } *)
 
-- 
cgit v1.2.3