diff --git a/tests/compiler/strictOrSimp.lean b/tests/compiler/strictOrSimp.lean
index ea135c5015..7797596110 100644
--- a/tests/compiler/strictOrSimp.lean
+++ b/tests/compiler/strictOrSimp.lean
@@ -1,3 +1,4 @@
+#lang lean4
 partial def spin : Nat → Bool
 | n => spin (n)
 
diff --git a/tests/lean/run/float_cases_bug.lean b/tests/lean/run/float_cases_bug.lean
index 4a3cf3476c..b4b4df6eed 100644
--- a/tests/lean/run/float_cases_bug.lean
+++ b/tests/lean/run/float_cases_bug.lean
@@ -1,4 +1,4 @@
 new_frontend
 
 def foo (xs : List Nat) :=
-xs.span (fun n => oldCoe (decide (n = 1)))
+xs.span (fun n => (decide (n = 1)))
diff --git a/tests/lean/run/typeclass_easy.lean b/tests/lean/run/typeclass_easy.lean
index 30e2690bab..da3b441542 100644
--- a/tests/lean/run/typeclass_easy.lean
+++ b/tests/lean/run/typeclass_easy.lean
@@ -4,7 +4,7 @@ new_frontend
 
 #synth HasAdd Nat
 
-#synth HasCoe Bool Prop
+#synth Coe Bool Prop
 
 #synth Decidable (True ∧ 1 = 1)