diff --git a/tests/bench/qsort.lean b/tests/bench/qsort.lean
index d5c85b119b..5dd965c511 100644
--- a/tests/bench/qsort.lean
+++ b/tests/bench/qsort.lean
@@ -18,7 +18,7 @@ partial def checkSortedAux (a : Array Elem) : Nat → IO Unit
 -- copied from stdlib, but with `UInt32` indices instead of `Nat` (which is more comparable to the other versions)
 abbrev Idx := UInt32
 instance : HasLift UInt32 Nat := ⟨UInt32.toNat⟩
-prefix `↑`:max := coe
+prefix `↑`:max := oldCoe
 
 @[specialize] private partial def partitionAux {α : Type} [Inhabited α] (lt : α → α → Bool) (hi : Idx) (pivot : α) : Array α → Idx → Idx → Idx × Array α
 | as, i, j =>
diff --git a/tests/bench/rbmap.lean b/tests/bench/rbmap.lean
index 737ad997bf..367c14f409 100644
--- a/tests/bench/rbmap.lean
+++ b/tests/bench/rbmap.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Coe
 import Init.Data.Option.Basic
 import Init.Data.List.BasicAux
 import Init.System.IO
diff --git a/tests/bench/rbmap_checkpoint.lean b/tests/bench/rbmap_checkpoint.lean
index 5733c85cc0..f505c9eede 100644
--- a/tests/bench/rbmap_checkpoint.lean
+++ b/tests/bench/rbmap_checkpoint.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Coe
 import Init.Data.Option.Basic
 import Init.Data.List.BasicAux
 import Init.System.IO
diff --git a/tests/lean/run/float_cases_bug.lean b/tests/lean/run/float_cases_bug.lean
index aef21a2a2e..296c21e466 100644
--- a/tests/lean/run/float_cases_bug.lean
+++ b/tests/lean/run/float_cases_bug.lean
@@ -1,2 +1,2 @@
 def foo (xs : List Nat) :=
-xs.span (fun n => coe (decide (n = 1)))
+xs.span (fun n => oldCoe (decide (n = 1)))
diff --git a/tests/lean/run/frontend1.lean b/tests/lean/run/frontend1.lean
index 5729afbd02..0daf41a595 100644
--- a/tests/lean/run/frontend1.lean
+++ b/tests/lean/run/frontend1.lean
@@ -216,7 +216,7 @@ def three := 3
 #eval run "#check g three (z := zero)"
 
 #eval run "open Lean.Parser
- @[termParser] def myParser : Lean.Parser.Parser Lean.ParserKind.leading := parser! coe \"hi\"
+ @[termParser] def myParser : Lean.Parser.Parser Lean.ParserKind.leading := parser! oldCoe \"hi\"
 #check myParser"
 
 #eval run "#check (fun stx => if True then let e := stx; HasPure.pure e else HasPure.pure stx : Nat → Id Nat)"