Add tests.

tests/proofmode.ref

@@ -589,6 +589,12 @@ Tactic failure: iSpecialize: "H" not found.
      : string
 The command has indeed failed with message:
 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.
+The command has indeed failed with message:
+Tactic failure: iSpecialize: premise cannot be solved by framing.
 "iExact_fail"
      : string
 The command has indeed failed with message:

tests/proofmode.v

@@ -1305,6 +1305,14 @@ Proof.
   iIntros "HW HP". Fail iSpecialize ("HW" with "H").
 Abort.
 
+Check "iSpecialize_autoframe_fail".
+Lemma iSpecialize_autoframe_fail P Q : (P -∗ Q) -∗ Q.
+Proof.
+  iIntros "H".
+  Fail iSpecialize ("H" with "[$]").
+  Fail iApply ("H" with "[$]").
+Abort.
+
 Check "iExact_fail".
 Lemma iExact_fail P Q :
   <affine> P -∗ Q -∗ <affine> P.