diff options
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 32f9069747..9a75f0b682 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 } |