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.

1 files changed, 19 insertions, 1 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 *)