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

(limited to 'kernel/indtypes.ml')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 50c052abbb..214aac5ec0 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -686,8 +686,7 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst =
       mind_nparams_rec = nmr;
       mind_params_ctxt = params;
       mind_packets = packets;
-      mind_constraints = cst;
-      mind_native_name = ref NotLinked
+      mind_constraints = cst
     }
 
 (************************************************************************)
-- 
cgit v1.2.3