diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/environ.ml | 20 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 4 |
2 files changed, 22 insertions, 2 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index f61dd0c101..019c0a6819 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -384,8 +384,26 @@ let set_engagement c env = (* Unsafe *) { env with env_stratification = { env.env_stratification with env_engagement = c } } +(* It's convenient to use [{flags with foo = bar}] so we're smart wrt to it. *) +let same_flags { + check_guarded; + check_universes; + conv_oracle; + share_reduction; + enable_VM; + enable_native_compiler; + } alt = + check_guarded == alt.check_guarded && + check_universes == alt.check_universes && + conv_oracle == alt.conv_oracle && + share_reduction == alt.share_reduction && + enable_VM == alt.enable_VM && + enable_native_compiler == alt.enable_native_compiler +[@warning "+9"] + let set_typing_flags c env = (* Unsafe *) - { env with env_typing_flags = c } + if same_flags env.env_typing_flags c then env + else { env with env_typing_flags = c } (* Global constants *) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index df10398b2f..2464df799e 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -192,7 +192,9 @@ let set_engagement c senv = engagement = Some c } let set_typing_flags c senv = - { senv with env = Environ.set_typing_flags c senv.env } + let env = Environ.set_typing_flags c senv.env in + if env == senv.env then senv + else { senv with env } let set_share_reduction b senv = let flags = Environ.typing_flags senv.env in |