Skip to content

Commit 0e301e8

Browse files
committed
chore: remove unused respectTransparency options (leanprover-community#37283)
The automated removal of `set_option` only searches for `set_option ... in`, and not for plain `set_option ...`. This PR removes a few such cases.
1 parent 8afd270 commit 0e301e8

4 files changed

Lines changed: 0 additions & 7 deletions

File tree

Mathlib/Geometry/Manifold/Riemannian/Basic.lean

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -211,8 +211,6 @@ the image of the neighborhood in the extended chart.
211211
open Manifold Metric
212212
open scoped NNReal
213213

214-
set_option backward.isDefEq.respectTransparency false
215-
216214
variable [RiemannianBundle (fun (x : M) ↦ TangentSpace I x)]
217215
[IsManifold I 1 M] [IsContinuousRiemannianBundle E (fun (x : M) ↦ TangentSpace I x)]
218216

Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -240,8 +240,6 @@ end Submodule
240240

241241
namespace Subalgebra
242242

243-
set_option backward.isDefEq.respectTransparency false
244-
245243
variable {K L : Type*} [Field K] [Ring L] [Algebra K L] {F E : Subalgebra K L}
246244
[hfin : FiniteDimensional K E]
247245

Mathlib/RingTheory/Adjoin/Dimension.lean

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -23,8 +23,6 @@ universe u v
2323

2424
namespace Subalgebra
2525

26-
set_option backward.isDefEq.respectTransparency false
27-
2826
variable {R : Type u} {S : Type v} [CommRing R] [StrongRankCondition R] [CommRing S] [Algebra R S]
2927
(A B : Subalgebra R S) [Free R A] [Free R B]
3028

Mathlib/RingTheory/DedekindDomain/Different.lean

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,6 @@ public import Mathlib.RingTheory.Trace.Quotient
3434
-/
3535

3636
@[expose] public section
37-
set_option backward.isDefEq.respectTransparency false
3837

3938
open Module
4039

0 commit comments

Comments
 (0)