From e6708f08300d8936d9a72fbde2ae27bfd19ae0e3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 3 Sep 2021 11:54:19 +0200
Subject: [PATCH] Make error message of auto frame more informative.
---
iris/proofmode/ltac_tactics.v | 4 +++-
tests/proofmode.ref | 10 ++++++++--
tests/proofmode.v | 8 ++++++++
3 files changed, 19 insertions(+), 3 deletions(-)
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 37a802083..36c1f6342 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 ebb13cbfa..f1dae3539 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 e3257f9e5..31cc46faa 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.
--
GitLab