fix tests

leanprover-community · Dec 3, 2024 · b07115b · b07115b
1 parent ea60bba
commit b07115b
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 86 deletions.
diff --git a/Batteries.lean b/Batteries.lean
@@ -93,7 +93,6 @@ import Batteries.Tactic.ShowUnused
 import Batteries.Tactic.SqueezeScope
 import Batteries.Tactic.Trans
 import Batteries.Tactic.Unreachable
-import Batteries.Tactic.Where
 import Batteries.Util.Cache
 import Batteries.Util.ExtendedBinder
 import Batteries.Util.LibraryNote

diff --git a/Batteries/Tactic/Where.lean b/Batteries/Tactic/Where.lean
diff --git a/BatteriesTest/where.lean b/BatteriesTest/where.lean
@@ -1,4 +1,7 @@
-import Batteries.Tactic.Where
+-- None of these imports are really necessary, except to create namespace mentioned below.
+import Lean.Elab.Term
+import Lean.Elab.Command
+import Batteries.Data.UnionFind.Basic
 
 -- Return to pristine state
 set_option linter.missingDocs false
@@ -68,6 +71,6 @@ open Array renaming map -> listMap
 info: open Lean Lean.Meta
 open Lean.Elab hiding TermElabM
 open Lean.Elab.Command Batteries
-open listMap → Array.map
+open Array renaming map → listMap
 -/
 #guard_msgs in #where