diff options
| author | coqbot-app[bot] | 2020-11-10 08:56:03 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-10 08:56:03 +0000 |
| commit | 449aef5dea7314f3bf4311380aa10c5cf0c3a158 (patch) | |
| tree | 81191c6eed316b32aedcd4e4a988edbd685b9f22 /kernel/environ.ml | |
| parent | e38d3bac150b709ffbbe6115723ce97177ace638 (diff) | |
| parent | fb5aa52ab8d870ee3613de325fbab7c98c33a433 (diff) | |
Merge PR #13297: Remove the native symbol registering from the safe environment.
Reviewed-by: SkySkimmer
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 17c5a02e2b..914c951eb6 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -104,7 +104,6 @@ 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 = { @@ -136,7 +135,6 @@ let empty_env = { env_typing_flags = Declareops.safe_flags Conv_oracle.empty; retroknowledge = Retroknowledge.empty; indirect_pterms = Opaqueproof.empty_opaquetab; - native_symbols = DPmap.empty; } @@ -829,10 +827,6 @@ let is_type_in_type env r = 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 } - module type QNameS = sig type t |