diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 7794b340ccd011965e0f47874704ef795daf82a2..a3799261570cbfd04c93fbaca4faa22e8d71c62a 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 941ff8ecbfc758840aece1b81127ff3ca810437c..485d249c6cc82948d9d0e952290752d257fd61ec 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 5b8f5c49a4d9350a50dc8d4102a537375f498962..ce7677545064c54cce50f854077f92c9034c22b9 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;