diff options
| author | Gaëtan Gilbert | 2018-10-15 14:03:06 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-11-15 10:27:34 +0100 |
| commit | b7203d14aad300c0ef02f66516ce0595182c81cd (patch) | |
| tree | f3b147f9c5141560e32bb252dbf0c05fbdb7af27 /kernel | |
| parent | b6f65c72cce697d7acc11f731983a8c18f497d10 (diff) | |
Make set_typing_flags "smart"
Fix #8609
gares said: I believe it was introduced in de20a45 where the
option (part of the summary) is moved to the save env. By setting the
summary, you unshare the safe env. Now we do that only if needed. The
stm uses `==` on the safe env to detect tactics that alter the env, eg
abstract.
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 |