From d3eac3d5fc8e5af499eb8750ca08ead8562dac6f Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
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/modops.ml | 21 +++++++++++++++------
 1 file changed, 15 insertions(+), 6 deletions(-)

(limited to 'kernel/modops.ml')

diff --git a/kernel/modops.ml b/kernel/modops.ml
index 6a0a952f7..2942412f0 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -302,28 +302,37 @@ let add_retroknowledge mp =
 
 (** {6 Adding a module in the environment } *)
 
-let rec add_structure mp sign resolver env =
+let rec add_structure mp sign resolver linkinfo env =
   let add_one env (l,elem) = match elem with
     |SFBconst cb ->
       let c = constant_of_delta_kn resolver (KerName.make2 mp l) in
-      Environ.add_constant c cb env
+      Environ.add_constant_key c cb linkinfo env
     |SFBmind mib ->
       let mind = mind_of_delta_kn resolver (KerName.make2 mp l) in
-      Environ.add_mind mind mib env
-    |SFBmodule mb -> add_module mb env (* adds components as well *)
+      Environ.add_mind_key mind (mib,linkinfo) env
+    |SFBmodule mb -> add_module mb linkinfo env (* adds components as well *)
     |SFBmodtype mtb -> Environ.add_modtype mtb env
   in
   List.fold_left add_one env sign
 
-and add_module mb env =
+and add_module mb linkinfo env =
   let mp = mb.mod_mp in
   let env = Environ.shallow_add_module mb env in
   match mb.mod_type with
   |NoFunctor struc ->
     add_retroknowledge mp mb.mod_retroknowledge
-      (add_structure mp struc mb.mod_delta env)
+      (add_structure mp struc mb.mod_delta linkinfo env)
   |MoreFunctor _ -> env
 
+let add_linked_module mb linkinfo env =
+  add_module mb linkinfo env
+
+let add_structure mp sign resolver env =
+  add_structure mp sign resolver (no_link_info ()) env
+
+let add_module mb env =
+  add_module mb (no_link_info ()) env
+
 let add_module_type mp mtb env =
   add_module (module_body_of_type mp mtb) env
 
-- 
cgit v1.2.3