From 1d4f2c16a08a0d2dc2fa7d846fefbcc212ffd46a Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Tue, 6 Aug 2024 08:17:00 +0000 Subject: [PATCH] fix: undo the accidental revert of #11877 in #11807 (#15523) A bad merge in #11807 causes the change from #11877 (removing `import ProofWidgets`) to be reverted. --- Mathlib/Tactic/Common.lean | 5 ----- Mathlib/Tactic/Widget/StringDiagram.lean | 1 + 2 files changed, 1 insertion(+), 5 deletions(-) diff --git a/Mathlib/Tactic/Common.lean b/Mathlib/Tactic/Common.lean index f318dca852025..53c1b1a4c238f 100644 --- a/Mathlib/Tactic/Common.lean +++ b/Mathlib/Tactic/Common.lean @@ -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 diff --git a/Mathlib/Tactic/Widget/StringDiagram.lean b/Mathlib/Tactic/Widget/StringDiagram.lean index b896832c3fa27..56a321a914335 100644 --- a/Mathlib/Tactic/Widget/StringDiagram.lean +++ b/Mathlib/Tactic/Widget/StringDiagram.lean @@ -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