aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativeconv.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-11-02 15:37:00 +0100
committerPierre-Marie Pédrot2020-11-09 16:38:46 +0100
commitfb5aa52ab8d870ee3613de325fbab7c98c33a433 (patch)
tree2d3af63b32225f14a1c541c8fcabe0ed54a8fbfc /kernel/nativeconv.ml
parentd2047c6368ae11a3a3fd7f2db8c991d135094e60 (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 'kernel/nativeconv.ml')
-rw-r--r--kernel/nativeconv.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 76215b4386..d77ee759c6 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -161,7 +161,7 @@ let native_conv_gen pb sigma env univs t1 t2 =
let fn = compile ml_filename code ~profile:false in
if !Flags.debug then Feedback.msg_debug (Pp.str "Running test...");
let t0 = Sys.time () in
- call_linker env ~fatal:true ~prefix fn (Some upds);
+ call_linker ~fatal:true ~prefix fn (Some upds);
let t1 = Sys.time () in
let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
if !Flags.debug then Feedback.msg_debug (Pp.str time_info);