From a10e32f537fbc94ae6b22d81424b8ce89c4fac04 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 26 Jan 2022 07:50:25 -0800
Subject: [PATCH] fix: check "heartbeats" at `simp`

---
 src/Lean/Meta/Tactic/Simp/Main.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index 89532d9c14..81ec44a9ad 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -142,6 +142,7 @@ def getSimpLetCase (n : Name) (t : Expr) (v : Expr) (b : Expr) : MetaM SimpLetCa
       return SimpLetCase.dep
 
 partial def simp (e : Expr) : M Result := withIncRecDepth do
+  checkMaxHeartbeats "simp"
   let cfg ← getConfig
   if (← isProof e) then
     return { expr := e }