evalExprCore Elab.block

leanprover · Nov 14, 2024 · 8245a20 · 8245a20
1 parent 4b17c42
commit 8245a20
Showing 1 changed file with 2 additions and 0 deletions.
diff --git 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