fix imports in tets

leanprover-community · Feb 9, 2024 · b375022 · b375022
1 parent 8e75b1a
commit b375022
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 0 deletions.
diff --git a/AesopTest/EraseSimp.lean b/AesopTest/EraseSimp.lean
@@ -6,6 +6,7 @@ Authors: Jannis Limperg
 
 import Aesop
 import Std.Tactic.GuardMsgs
+import Std.Linter.UnreachableTactic
 
 set_option aesop.check.all true
 set_option aesop.smallErrorMessages true

diff --git a/AesopTest/HeartbeatLimit.lean b/AesopTest/HeartbeatLimit.lean
@@ -6,6 +6,7 @@ Authors: Jannis Limperg
 
 import Aesop
 import Std.Tactic.GuardMsgs
+import Std.Linter.UnreachableTactic
 
 set_option aesop.check.all true
 set_option linter.unreachableTactic false