diff options
| author | Gaëtan Gilbert | 2019-06-11 11:34:16 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-06-12 14:17:55 +0200 |
| commit | 00fcbf38dcd127e3d2d4f748f215787855abd609 (patch) | |
| tree | fabcbdbe58c7eae35148ad28153e4a96590bff45 /library | |
| parent | 793a442d240c22f99591388ad31e33fbaef96fb0 (diff) | |
Remove dependency of native_compile on global env for symbols
Instead we get the symbols from a Environ.env.
We make them accessible to the produced code through a reference
managed by the kernel, similar to the return values except inverting
when it's written and when it's read.
Diffstat (limited to 'library')
| -rw-r--r-- | library/declaremods.ml | 3 | ||||
| -rw-r--r-- | library/declaremods.mli | 2 | ||||
| -rw-r--r-- | library/library.ml | 2 |
3 files changed, 1 insertions, 6 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index d74bdd484c..a922e84540 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -915,9 +915,6 @@ let register_library dir cenv (objs:library_objects) digest univ = let sobjs,keepobjs = objs in do_module false Lib.load_objects 1 dir mp ([],Objs sobjs) keepobjs -let get_library_native_symbols dir = - Safe_typing.get_library_native_symbols (Global.safe_env ()) dir - let start_library dir = let mp = Global.start_library dir in openmod_info := default_module_info; diff --git a/library/declaremods.mli b/library/declaremods.mli index c35abae155..15191e3d72 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -94,8 +94,6 @@ val register_library : Safe_typing.compiled_library -> library_objects -> Safe_typing.vodigest -> Univ.ContextSet.t -> unit -val get_library_native_symbols : library_name -> Nativevalues.symbols - val start_library : library_name -> unit val end_library : diff --git a/library/library.ml b/library/library.ml index 1ac75d2fdc..b62164d8fa 100644 --- a/library/library.ml +++ b/library/library.ml @@ -173,7 +173,7 @@ let register_loaded_library m = let f = prefix ^ "cmo" in let f = Dynlink.adapt_filename f in if Coq_config.native_compiler then - Nativelib.link_library ~prefix ~dirname ~basename:f + Nativelib.link_library (Global.env()) ~prefix ~dirname ~basename:f in let rec aux = function | [] -> link (); [libname] |