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/safe_typing.ml | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

(limited to 'kernel/safe_typing.ml')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index ac7a5bb937..ebfb99c73e 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -679,9 +679,7 @@ let export senv dir =
   let ast, values =
     if !Flags.no_native_compiler then [], [||]
     else
-      let ast, values, upds = Nativelibrary.dump_library mp dir senv.env str in
-      Nativecode.update_locations upds;
-      ast, values
+      Nativelibrary.dump_library mp dir senv.env str
   in
   let lib = {
     comp_name = dir;
@@ -700,7 +698,11 @@ let import lib digest senv =
   let env = Environ.add_constraints mb.mod_constraints senv.env in
   (mp, lib.comp_natsymbs),
   { senv with
-    env = Modops.add_module mb env;
+    env =
+      (let linkinfo =
+	 Nativecode.link_info_of_dirpath lib.comp_name
+       in
+       Modops.add_linked_module mb linkinfo env);
     modresolver = Mod_subst.add_delta_resolver mb.mod_delta senv.modresolver;
     imports = (lib.comp_name,digest)::senv.imports;
     loads = (mp,mb)::senv.loads }
-- 
cgit v1.2.3