Skip to content

Commit 5bf5c73

Browse files
authored
chore: prune imports in Try.Collect (#11570)
This PR removed unused imports from Try.Collect
1 parent 5326530 commit 5bf5c73

File tree

1 file changed

+0
-2
lines changed

1 file changed

+0
-2
lines changed

src/Lean/Meta/Tactic/Try/Collect.lean

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,6 @@ module
77
prelude
88
public import Init.Try
99
public import Lean.Meta.Tactic.LibrarySearch
10-
public import Lean.Meta.Tactic.Grind.Cases
11-
public import Lean.Meta.Tactic.Grind.EMatchTheorem
1210
public import Lean.Meta.Tactic.FunIndCollect
1311
import Lean.Meta.Eqns
1412
public section

0 commit comments

Comments
 (0)