Skip to content

Commit

Permalink
fix: undo the accidental revert of #11877 in #11807 (#15523)
Browse files Browse the repository at this point in the history
A bad merge in #11807 causes the change from #11877 (removing `import ProofWidgets`) to be reverted.
  • Loading branch information
eric-wieser committed Aug 6, 2024
1 parent 5bc5222 commit 1d4f2c1
Show file tree
Hide file tree
Showing 2 changed files with 1 addition and 5 deletions.
5 changes: 0 additions & 5 deletions Mathlib/Tactic/Common.lean
Original file line number Diff line number Diff line change
Expand Up @@ -11,11 +11,6 @@ import Qq
-- Tools for analysing imports, like `#find_home`, `#minimize_imports`, ...
import ImportGraph.Imports

-- Currently we don't need to import all of ProofWidgets,
-- but without this, if you don't run `lake build ProofWidgets` then `make test` will fail.
-- Hopefully `lake` will be able to handle tests later.
import ProofWidgets

-- Import common Batteries tactics and commands
import Batteries.Tactic.Where

Expand Down
1 change: 1 addition & 0 deletions Mathlib/Tactic/Widget/StringDiagram.lean
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yuma Mizuno
-/
import ProofWidgets.Component.PenroseDiagram
import ProofWidgets.Component.Panel.Basic
import ProofWidgets.Presentation.Expr
import Mathlib.Tactic.CategoryTheory.Monoidal

Expand Down

0 comments on commit 1d4f2c1

Please sign in to comment.