From 29eddad3257cefbb3a5d7645adaeef2f74ba3ad3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 1 Sep 2022 07:18:47 -0700
Subject: [PATCH] chore: only check if `compiler.check` is set to true

---
 src/Lean/Compiler/LCNF/Main.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Compiler/LCNF/Main.lean b/src/Lean/Compiler/LCNF/Main.lean
index 5ae19a7a99..b679c9a1a2 100644
--- a/src/Lean/Compiler/LCNF/Main.lean
+++ b/src/Lean/Compiler/LCNF/Main.lean
@@ -49,7 +49,8 @@ def checkpoint (stepName : Name) (decls : Array Decl) : CompilerM Unit := do
         Lean.addTrace clsName m!"size: {decl.size}\n{← ppDecl decl}"
       if compiler.check.get (← getOptions) then
         decl.check
-  checkDeadLocalDecls decls
+  if compiler.check.get (← getOptions) then
+    checkDeadLocalDecls decls
 
 namespace PassManager