Merge PR #10359: Remove dependency of native_compile on global env for symbols

Reviewed-by: maximedenes
Reviewed-by: ppedrot

3 files changed, 1 insertions, 6 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index f3922125fe..eea129eae7 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -956,9 +956,6 @@ let register_library dir cenv (objs:library_objects) digest univ =
   let sobjs,keepobjs = objs in
   do_module false 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 9c0baf0a4c..ada53dbff0 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 -> Nativecode.symbols
-
 val start_library : library_name -> unit
 
 val end_library :
diff --git a/library/library.ml b/library/library.ml
index b72dd9dd67..0faef7bf84 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]