diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 3275844a0cda383b53fd34509226e741202bde27..34d52265be0f8d05e97247815472e27f21d3c97b 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -621,10 +621,10 @@ k is used in hypothesis Hk.
      : string
 The command has indeed failed with message:
 Tactic failure: iRevert: k is used in hypothesis "Hk".
-"iLöb_no_bi"
+"iLöb_no_BiLöb"
      : string
 The command has indeed failed with message:
-Tactic failure: iLöb: Löb induction not supported for this BI.
+Tactic failure: iLöb: no 'BiLöb' instance found.
 "test_pure_name"
      : string
 1 subgoal
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 9670b934acc1be71146bbb1ee6563768f78632e2..2df448f52408dc24f7624847efd28aed11f7c08b 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1127,8 +1127,8 @@ Section error_tests_bi.
 Context {PROP : bi}.
 Implicit Types P Q R : PROP.
 
-Check "iLöb_no_bi".
-Lemma iLöb_no_bi P : ⊢ P.
+Check "iLöb_no_BiLöb".
+Lemma iLöb_no_BiLöb P : ⊢ P.
 Proof. Fail iLöb as "IH". Abort.
 End error_tests_bi.
 
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 2604bdd673d2fde3cb8d331e8fb3161b0d789e93..95810df702f32c6fd3d38384b8f73cdc5c55df1a 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -2534,7 +2534,7 @@ Tactic Notation "iLöbCore" "as" constr (IH) :=
      refine should use the other unification algorithm, which should
      not have this issue. *)
   notypeclasses refine (tac_löb _ IH _ _ _ _);
-    [iSolveTC || fail "iLöb: Löb induction not supported for this BI"
+    [iSolveTC || fail "iLöb: no 'BiLöb' instance found"
     |reflexivity || fail "iLöb: spatial context not empty, this should not happen"
     |pm_reduce;
      lazymatch goal with