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 /kernel/nativecode.ml | |
| 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 'kernel/nativecode.ml')
| -rw-r--r-- | kernel/nativecode.ml | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index b5c4d6416a..911a879394 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -2192,11 +2192,9 @@ let mk_norm_code env sigma prefix t = [|MLglobal (Ginternal "()")|])) in header::gl, (mind_updates, const_updates) -let mk_library_header dir = - let libname = Format.sprintf "(str_decode \"%s\")" (str_encode dir) in - [Glet(Ginternal "symbols_tbl", - MLapp (MLglobal (Ginternal "get_library_native_symbols"), - [|MLglobal (Ginternal libname)|]))] +let mk_library_header (symbols : Nativevalues.symbols) = + let symbols = Format.sprintf "(str_decode \"%s\")" (str_encode symbols) in + [Glet(Ginternal "symbols_tbl", MLglobal (Ginternal symbols))] let update_location (r,v) = r := v |