Merge branch 'robbert/error_message_autoframe' into 'master'

Fix and improve `iSpecialize` auto framing error message.

Closes #432

See merge request iris/iris!730

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 "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.
 

tests/proofmode.ref

@@ -549,6 +549,18 @@ 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 P cannot be solved by framing.
+The command has indeed failed with message:
+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:

tests/proofmode.v

@@ -1305,6 +1305,22 @@ 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 "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.