diff options
| author | Pierre-Marie Pédrot | 2020-11-02 15:37:00 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-11-09 16:38:46 +0100 |
| commit | fb5aa52ab8d870ee3613de325fbab7c98c33a433 (patch) | |
| tree | 2d3af63b32225f14a1c541c8fcabe0ed54a8fbfc /pretyping | |
| parent | d2047c6368ae11a3a3fd7f2db8c991d135094e60 (diff) | |
Remove the native symbol registering from the safe environment.
Instead we store that data in the native code that was generated in adapt
the compilation scheme accordingly. Less indirections and less imperative
tinkering makes the code safer.
The global symbol table was originally introduced in #10359 as a way not to
depend on the Global module in the generated code. By storing all the
native-related information in the cmxs file itself, this PR also makes other
changes easier, such as e.g. #13287.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/nativenorm.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 3f68e3c78f..d06d6e01d1 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -525,7 +525,7 @@ let native_norm env sigma c ty = if print_timing then Feedback.msg_info (Pp.str time_info); let profiler_pid = if profile then start_profiler () else None in let t0 = Unix.gettimeofday () in - Nativelib.call_linker ~fatal:true env ~prefix fn (Some upd); + Nativelib.call_linker ~fatal:true ~prefix fn (Some upd); let t1 = Unix.gettimeofday () in if profile then stop_profiler profiler_pid; let time_info = Format.sprintf "native_compute: Evaluation done in %.5f" (t1 -. t0) in |