diff options
| author | coqbot-app[bot] | 2020-11-10 08:56:03 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-10 08:56:03 +0000 |
| commit | 449aef5dea7314f3bf4311380aa10c5cf0c3a158 (patch) | |
| tree | 81191c6eed316b32aedcd4e4a988edbd685b9f22 /vernac | |
| parent | e38d3bac150b709ffbbe6115723ce97177ace638 (diff) | |
| parent | fb5aa52ab8d870ee3613de325fbab7c98c33a433 (diff) | |
Merge PR #13297: Remove the native symbol registering from the safe environment.
Reviewed-by: SkySkimmer
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/declaremods.mli | 2 | ||||
| -rw-r--r-- | vernac/library.ml | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/vernac/declaremods.mli b/vernac/declaremods.mli index 9ca2ca5593..a1b98e4d9c 100644 --- a/vernac/declaremods.mli +++ b/vernac/declaremods.mli @@ -86,7 +86,7 @@ val start_library : library_name -> unit val end_library : ?except:Future.UUIDSet.t -> output_native_objects:bool -> library_name -> - Safe_typing.compiled_library * library_objects * Safe_typing.native_library + Safe_typing.compiled_library * library_objects * Nativelib.native_library (** append a function to be executed at end_library *) val append_end_library_hook : (unit -> unit) -> unit diff --git a/vernac/library.ml b/vernac/library.ml index e580927bfd..8a9b1fd68d 100644 --- a/vernac/library.ml +++ b/vernac/library.ml @@ -160,7 +160,7 @@ let register_loaded_library m = let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in let f = prefix ^ "cmo" in let f = Dynlink.adapt_filename f in - Nativelib.link_library (Global.env()) ~prefix ~dirname ~basename:f + Nativelib.link_library ~prefix ~dirname ~basename:f in let rec aux = function | [] -> @@ -502,7 +502,7 @@ let save_library_to todo_proofs ~output_native_objects dir f otab = (* Writing native code files *) if output_native_objects then let fn = Filename.dirname f ^"/"^ Nativecode.mod_uid_of_dirpath dir in - Nativelib.compile_library dir ast fn + Nativelib.compile_library ast fn let save_library_raw f sum lib univs proofs = save_library_base f sum lib (Some univs) None proofs |