Remove dependency of native_compile on global env for symbols

Instead we get the symbols from a Environ.env.
We make them accessible to the produced code through a reference
managed by the kernel, similar to the return values except inverting
when it's written and when it's read.

1 files changed, 8 insertions, 1 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index c47bde0864..be3d42bbc9 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -95,6 +95,7 @@ type env = {
   env_typing_flags  : typing_flags;
   retroknowledge : Retroknowledge.retroknowledge;
   indirect_pterms : Opaqueproof.opaquetab;
+  native_symbols : Nativevalues.symbols DPmap.t;
 }
 
 let empty_named_context_val = {
@@ -123,7 +124,9 @@ let empty_env = {
   };
   env_typing_flags = Declareops.safe_flags Conv_oracle.empty;
   retroknowledge = Retroknowledge.empty;
-  indirect_pterms = Opaqueproof.empty_opaquetab }
+  indirect_pterms = Opaqueproof.empty_opaquetab;
+  native_symbols = DPmap.empty;
+}
 
 
 (* Rel context *)
@@ -763,3 +766,7 @@ let is_type_in_type env r =
   | ConstructRef cstr -> type_in_type_ind (inductive_of_constructor cstr) env
 
 let set_retroknowledge env r = { env with retroknowledge = r }
+
+let set_native_symbols env native_symbols = { env with native_symbols }
+let add_native_symbols dir syms env =
+  { env with native_symbols = DPmap.add dir syms env.native_symbols }