aboutsummaryrefslogtreecommitdiff
path: root/kernel/safe_typing.ml
diff options
context:
space:
mode:
authorMaxime Dénès2013-12-28 20:39:17 -0500
committerMaxime Dénès2013-12-28 20:39:17 -0500
commitd3eac3d5fc8e5af499eb8750ca08ead8562dac6f (patch)
tree70540c3d5e8b0856db2a9e82710e1b32cdc8465d /kernel/safe_typing.ml
parenta681e57e3c76dff2fe710ce533179ea659d8de0b (diff)
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.
Diffstat (limited to 'kernel/safe_typing.ml')
-rw-r--r--kernel/safe_typing.ml10
1 files changed, 6 insertions, 4 deletions
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 }