diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 8ddfcb423e4daebe6278e7887f4f1afb0fb7cb1f..393eada0053361382bbf872e1a16a890ad96dc10 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -541,6 +541,10 @@ The command has indeed failed with message:
 Tactic failure: iIntro: "HP" not fresh.
 The command has indeed failed with message:
 x is already used.
+"iIntros_pure_not_forall"
+     : string
+The command has indeed failed with message:
+Tactic failure: iIntro: cannot turn (P -∗ Q)%I into a universal quantifier.
 "iSplitL_one_of_many"
      : string
 The command has indeed failed with message:
diff --git a/tests/proofmode.v b/tests/proofmode.v
index d84511d9d1fe9f618b54692199563f261eee3af9..cee968cb6aa64d44bfaba81f80e7ffa09674b888 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1104,6 +1104,13 @@ Proof.
   iIntros "HQ" (x). Fail iIntros (x).
 Abort.
 
+Check "iIntros_pure_not_forall".
+Lemma iIntros_pure_not_forall P Q :
+  P -∗ Q.
+Proof.
+  Fail iIntros (?).
+Abort.
+
 Check "iSplitL_one_of_many".
 Lemma iSplitL_one_of_many P :
   P -∗ P -∗ P ∗ P.
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 2a401898652fde7d757ddeb98e8754bb79ecca8d..1aebf309ccceff63aaa36f70b1a530d9b497ccdb 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -472,7 +472,7 @@ Local Tactic Notation "iIntro" "(" simple_intropattern(x) ")" :=
     | |- envs_entails _ _ =>
       eapply tac_forall_intro;
         [iSolveTC ||
-         let P := match goal with |- FromForall ?P _ => P end in
+         let P := match goal with |- FromForall ?P _ _ => P end in
          fail "iIntro: cannot turn" P "into a universal quantifier"
         |let name := lazymatch goal with
                      | |- let _ := (λ name, _) in _ => name