diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 37a802083a108f58496f3469667002e77aabb948..36c1f6342dab48e53a6a0b26d272a24f0cfa8b13 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -1007,7 +1007,9 @@ Ltac iSpecializePat_go H1 pats :=
             [notypeclasses refine (tac_unlock_emp _ _ _)
             |notypeclasses refine (tac_unlock_True _ _ _)
             |iFrame "∗ #"; notypeclasses refine (tac_unlock _ _ _)
-            |fail 1 "iSpecialize: premise cannot be solved by framing"]
+            |let P :=
+               match goal with |- envs_entails _ (?P ∗ locked _)%I => P end in
+             fail 1 "iSpecialize: premise" P "cannot be solved by framing"]
          |exact eq_refl]; iIntro H1; iSpecializePat_go H1 pats
     end.
 
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index ebb13cbfacdb8717ae2d2c4570b18a17487ca9c4..f1dae353927b7a2d5f2b61358e46bb3d52bde1f1 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -592,9 +592,15 @@ Tactic failure: iSpecialize: "H" not found.
 "iSpecialize_autoframe_fail"
      : string
 The command has indeed failed with message:
-Tactic failure: iSpecialize: premise cannot be solved by framing.
+Tactic failure: iSpecialize: premise P cannot be solved by framing.
 The command has indeed failed with message:
-Tactic failure: iSpecialize: premise cannot be solved by framing.
+Tactic failure: iSpecialize: premise P cannot be solved by framing.
+"iSpecialize_autoframe_fail2"
+     : string
+The command has indeed failed with message:
+Tactic failure: iSpecialize: premise Q cannot be solved by framing.
+The command has indeed failed with message:
+Tactic failure: iSpecialize: premise Q cannot be solved by framing.
 "iExact_fail"
      : string
 The command has indeed failed with message:
diff --git a/tests/proofmode.v b/tests/proofmode.v
index e3257f9e574a38bf1932ccb0c05d02c0f70ebfeb..31cc46faa14e1b1d2bf74238b14435a34b6fd889 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1313,6 +1313,14 @@ Proof.
   Fail iApply ("H" with "[$]").
 Abort.
 
+Check "iSpecialize_autoframe_fail2".
+Lemma iSpecialize_autoframe_fail2 P Q R : (P -∗ Q -∗ R) -∗ P -∗ R.
+Proof.
+  iIntros "H HP".
+  Fail iSpecialize ("H" with "[$] [$]").
+  Fail iApply ("H" with "[$] [$]").
+Abort.
+
 Check "iExact_fail".
 Lemma iExact_fail P Q :
   <affine> P -∗ Q -∗ <affine> P.