Skip to content

Commit 9519868

Browse files
chore: remove two unused opened namespaces (#38079)
These were breaking after `lake shake --fix`: cf. #37857
1 parent 2be1d77 commit 9519868

File tree

2 files changed

+2
-2
lines changed

2 files changed

+2
-2
lines changed

Mathlib/CategoryTheory/Monoidal/Internal/Limits.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ in particular `MonCat`, `SemiRingCat`, `RingCat`, and `AlgCat R`.)
2323
@[expose] public section
2424

2525

26-
open CategoryTheory Limits Monoidal MonoidalCategory
26+
open CategoryTheory Limits MonoidalCategory
2727

2828
universe v u w
2929

Mathlib/CategoryTheory/Monoidal/Widesubcategory.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ them to construct monoidal, braided, and symmetric structures on
2727

2828
namespace CategoryTheory
2929

30-
open scoped MonoidalCategory ComonObj
30+
open scoped MonoidalCategory
3131

3232
variable {C : Type*} [Category* C] (P : MorphismProperty C) [MonoidalCategory C]
3333

0 commit comments

Comments
 (0)