From b7203d14aad300c0ef02f66516ce0595182c81cd Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 15 Oct 2018 14:03:06 +0200
Subject: 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.
---
 kernel/environ.ml     | 20 +++++++++++++++++++-
 kernel/safe_typing.ml |  4 +++-
 2 files changed, 22 insertions(+), 2 deletions(-)

(limited to 'kernel')

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
-- 
cgit v1.2.3