From 3732f05e481b2654380ac94a88d39885b1d65365 Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Mon, 28 Sep 2020 10:26:47 -0500
Subject: [PATCH] Improve some iIntros error messages

A failing iIntros for implications should prettify the identifier before
printing, and iIntros on something that isn't a wand or implication
should say what couldn't be introduced (to clarify that `iIntros "HP
HQ"` failed because of the HQ in particular, for example).
---
 tests/proofmode.ref               | 14 ++++++++++++++
 tests/proofmode.v                 | 12 ++++++++++++
 theories/proofmode/ltac_tactics.v |  4 +++-
 3 files changed, 29 insertions(+), 1 deletion(-)

diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 7794b340c..a37992615 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -653,6 +653,20 @@ Tactic failure: iApply: cannot apply P.
      : string
 The command has indeed failed with message:
 Tactic failure: iApply: remaining hypotheses not affine and the goal not absorbing.
+"iIntros_fail_nonempty_spatial"
+     : string
+The command has indeed failed with message:
+Tactic failure: iIntro: introducing non-persistent "HP" : P
+into non-empty spatial context.
+"iIntros_fail_not_fresh"
+     : string
+The command has indeed failed with message:
+Tactic failure: iIntro: "HP" not fresh.
+"iIntros_fail_nothing_to_introduce"
+     : string
+The command has indeed failed with message:
+Tactic failure: iIntro: could not introduce "HQ"
+, goal is not a wand or implication.
 "iApply_fail_not_affine_2"
      : string
 The command has indeed failed with message:
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 941ff8ecb..485d249c6 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1238,6 +1238,18 @@ Check "iApply_fail_not_affine_1".
 Lemma iApply_fail_not_affine_1 P Q : P -∗ Q -∗ Q.
 Proof. iIntros "HP HQ". Fail iApply "HQ". Abort.
 
+Check "iIntros_fail_nonempty_spatial".
+Lemma iIntro_fail_nonempty_spatial P Q : P -∗ P → Q.
+Proof. Fail iIntros "? HP". Abort.
+
+Check "iIntros_fail_not_fresh".
+Lemma iIntro_fail_not_fresh P Q : P -∗ P -∗ Q.
+Proof. Fail iIntros "HP HP". Abort.
+
+Check "iIntros_fail_nothing_to_introduce".
+Lemma iIntro_fail_nothing_to_introduce P Q : P -∗ Q.
+Proof. Fail iIntros "HP HQ". Abort.
+
 Check "iApply_fail_not_affine_2".
 Lemma iApply_fail_not_affine_2 P Q R : P -∗ R -∗ (R -∗ Q) -∗ Q.
 Proof. iIntros "HP HR HQ". Fail iApply ("HQ" with "HR"). Abort.
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 5b8f5c49a..ce7677545 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -491,6 +491,7 @@ Local Tactic Notation "iIntro" constr(H) :=
       [iSolveTC
       |pm_reduce; iSolveTC ||
        let P := lazymatch goal with |- Persistent ?P => P end in
+       let H := pretty_ident H in
        fail 1 "iIntro: introducing non-persistent" H ":" P
               "into non-empty spatial context"
       |iSolveTC
@@ -512,7 +513,8 @@ Local Tactic Notation "iIntro" constr(H) :=
           fail 1 "iIntro:" H "not fresh"
         | _ => idtac (* subgoal *)
         end]
-  | fail 1 "iIntro: nothing to introduce" ].
+  | let H := pretty_ident H in
+    fail 1 "iIntro: could not introduce" H ", goal is not a wand or implication" ].
 
 Local Tactic Notation "iIntro" "#" constr(H) :=
   iStartProof;
-- 
GitLab