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/safe_typing.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'kernel/safe_typing.ml')

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