chore: remove references to fixed lean bug (#1338)

Followup to #1335.
leanprover-community · Jan 4, 2023 · c0e8ec7 · c0e8ec7
1 parent 7e2613a
commit c0e8ec7
Show file tree

Hide file tree

Showing 3 changed files with 0 additions and 3 deletions.
diff --git a/Mathlib/Order/Antichain.lean b/Mathlib/Order/Antichain.lean
@@ -336,7 +336,6 @@ variable {ι : Type _} {α : ι → Type _} [∀ i, Preorder (α i)] {s t : Set
   {a b c : ∀ i, α i}
 
 
--- Porting note: local notation given a name because of https://github.com/leanprover/lean4/issues/2000
 @[inherit_doc]
 local infixl:50 " ≺ " => StrongLT
 

diff --git a/Mathlib/Order/Chain.lean b/Mathlib/Order/Chain.lean
@@ -44,7 +44,6 @@ section Chain
 variable (r : α → α → Prop)
 
 /-- In this file, we use `≺` as a local notation for any relation `r`. -/
--- Porting note: local notation given a name because of https://github.com/leanprover/lean4/issues/2000
 local infixl:50 " ≺ " => r
 
 /-- A chain is a set `s` satisfying `x ≺ y ∨ x = y ∨ y ≺ x` for all `x y ∈ s`. -/

diff --git a/Mathlib/Order/Zorn.lean b/Mathlib/Order/Zorn.lean
@@ -71,7 +71,6 @@ open Classical Set
 variable {α β : Type _} {r : α → α → Prop} {c : Set α}
 
 /-- Local notation for the relation being considered. -/
--- Porting note: local notation given a name because of https://github.com/leanprover/lean4/issues/2000
 local infixl:50 " ≺ " => r
 
 /-- **Zorn's lemma**