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/safe_typing.mli | |
| 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/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index b601279e87..6fa9022906 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -191,8 +191,6 @@ val current_dirpath : safe_environment -> DirPath.t type compiled_library -type native_library = Nativecode.global list - val module_of_library : compiled_library -> Declarations.module_body val univs_of_library : compiled_library -> Univ.ContextSet.t @@ -201,7 +199,7 @@ val start_library : DirPath.t -> ModPath.t safe_transformer val export : ?except:Future.UUIDSet.t -> output_native_objects:bool -> safe_environment -> DirPath.t -> - ModPath.t * compiled_library * native_library + ModPath.t * compiled_library * Nativelib.native_library (* Constraints are non empty iff the file is a vi2vo *) val import : compiled_library -> Univ.ContextSet.t -> vodigest -> |