another test regression

leanprover · Oct 1, 2024 · 7db3312 · 7db3312
1 parent 52267e8
commit 7db3312
Showing 1 changed file with 0 additions and 28 deletions.
diff --git a/tests/lean/run/isDefEqProjIssue.lean b/tests/lean/run/isDefEqProjIssue.lean
@@ -54,34 +54,6 @@ where
 error: (deterministic) timeout at `whnf`, maximum number of heartbeats (400) has been reached
 Use `set_option maxHeartbeats <num>` to set the limit.
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
----
-error: (deterministic) timeout at `isDefEq`, maximum number of heartbeats (400) has been reached
-Use `set_option maxHeartbeats <num>` to set the limit.
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
----
-error: (deterministic) timeout at `elaborator`, maximum number of heartbeats (400) has been reached
-Use `set_option maxHeartbeats <num>` to set the limit.
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
----
-error: (deterministic) timeout at `isDefEq`, maximum number of heartbeats (400) has been reached
-Use `set_option maxHeartbeats <num>` to set the limit.
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
----
-error: (deterministic) timeout at `isDefEq`, maximum number of heartbeats (400) has been reached
-Use `set_option maxHeartbeats <num>` to set the limit.
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
----
-error: (deterministic) timeout at `elaborator`, maximum number of heartbeats (400) has been reached
-Use `set_option maxHeartbeats <num>` to set the limit.
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
----
-error: (deterministic) timeout at `isDefEq`, maximum number of heartbeats (400) has been reached
-Use `set_option maxHeartbeats <num>` to set the limit.
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
----
-error: (deterministic) timeout at `whnf`, maximum number of heartbeats (400) has been reached
-Use `set_option maxHeartbeats <num>` to set the limit.
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 set_option backward.isDefEq.lazyWhnfCore false in