From 8245a20591dcfaec8c6ca6e6767c8a8c51bb8b36 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 14 Nov 2024 10:36:48 +0100
Subject: [PATCH] evalExprCore Elab.block

---
 src/Lean/Meta/Eval.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Lean/Meta/Eval.lean b/src/Lean/Meta/Eval.lean
index cd1d38ac0e1b..2383de95fd4d 100644
--- a/src/Lean/Meta/Eval.lean
+++ b/src/Lean/Meta/Eval.lean
@@ -24,6 +24,8 @@ unsafe def evalExprCore (α) (value : Expr) (checkType : Expr → MetaM Unit) (s
        value, hints := ReducibilityHints.opaque,
        safety
     }
+    withTraceNode `Elab.block (fun _ => pure "") do
+      modifyEnv (·.synchronize)
     addAndCompile decl
     evalConst α name