diff --git a/tests/lean/pp_no_proofs.lean.expected.out b/tests/lean/pp_no_proofs.lean.expected.out
index cd36b3d787..c105b538fc 100644
--- a/tests/lean/pp_no_proofs.lean.expected.out
+++ b/tests/lean/pp_no_proofs.lean.expected.out
@@ -1,3 +1,5 @@
+pp_no_proofs.lean:8:11:failed to generate bytecode for 'messy'
+code generation failed, VM does not have code for 'f'
 f (Ps (Ps (Ps (Ps (Ps (Ps P0))))))
 f ⌞P 6⌟
 @f 6 ⌞@P ⌞true⌟ 6⌟
diff --git a/tests/lean/pp_proofs_coercions.lean.expected.out b/tests/lean/pp_proofs_coercions.lean.expected.out
index ae220d49d6..f289322de4 100644
--- a/tests/lean/pp_proofs_coercions.lean.expected.out
+++ b/tests/lean/pp_proofs_coercions.lean.expected.out
@@ -1,3 +1,4 @@
+string ↣ name : mk_simple_name
 C ↣ _Fun : f
 C ↣ [fun-class] : f
 c