diff options
| author | Maxime Dénès | 2013-12-28 20:39:17 -0500 |
|---|---|---|
| committer | Maxime Dénès | 2013-12-28 20:39:17 -0500 |
| commit | d3eac3d5fc8e5af499eb8750ca08ead8562dac6f (patch) | |
| tree | 70540c3d5e8b0856db2a9e82710e1b32cdc8465d /kernel/safe_typing.ml | |
| parent | a681e57e3c76dff2fe710ce533179ea659d8de0b (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.ml | 10 |
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 } |
