File tree Expand file tree Collapse file tree 2 files changed +2
-0
lines changed Expand file tree Collapse file tree 2 files changed +2
-0
lines changed Original file line number Diff line number Diff line change @@ -6436,6 +6436,7 @@ public import Mathlib.Tactic.Linter.MinImports
64366436public import Mathlib.Tactic.Linter.Multigoal
64376437public import Mathlib.Tactic.Linter.OldObtain
64386438public import Mathlib.Tactic.Linter.PPRoundtrip
6439+ public import Mathlib.Tactic.Linter.PrivateModule
64396440public import Mathlib.Tactic.Linter.Style
64406441public import Mathlib.Tactic.Linter.TextBased
64416442public import Mathlib.Tactic.Linter.UnusedTactic
Original file line number Diff line number Diff line change @@ -171,6 +171,7 @@ public import Mathlib.Tactic.Linter.MinImports
171171public import Mathlib.Tactic.Linter.Multigoal
172172public import Mathlib.Tactic.Linter.OldObtain
173173public import Mathlib.Tactic.Linter.PPRoundtrip
174+ public import Mathlib.Tactic.Linter.PrivateModule
174175public import Mathlib.Tactic.Linter.Style
175176public import Mathlib.Tactic.Linter.TextBased
176177public import Mathlib.Tactic.Linter.UnusedTactic
You can’t perform that action at this time.
0 commit comments