One more hack to remove!

leanprover-community · Dec 12, 2023 · 816edcc · 816edcc
1 parent b6c65c7
commit 816edcc
Showing 1 changed file with 0 additions and 3 deletions.
diff --git a/Mathlib/Geometry/Manifold/Sheaf/LocallyRingedSpace.lean b/Mathlib/Geometry/Manifold/Sheaf/LocallyRingedSpace.lean
@@ -38,9 +38,6 @@ variable {𝕜 : Type u} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
 
 open AlgebraicGeometry Manifold TopologicalSpace Topology
 
--- HACK to avoid an instance timeout
-attribute [-instance] StarAlgHomClass.toAlgHomClass NonUnitalStarAlgHomClass.toNonUnitalAlgHomClass
-
 /-- The units of the stalk at `x` of the sheaf of smooth functions from `M` to `𝕜`, considered as a
 sheaf of commutative rings, are the functions whose values at `x` are nonzero. -/
 theorem smoothSheafCommRing.isUnit_stalk_iff {x : M}