diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 4c7069ccb79c85c5cead2cd941d235ecae69bb37..2983b97c182ba2393dc2ec7e1dfb8ca689532ed1 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -939,7 +939,7 @@ Tactic Notation "iIntros" constr(pat) :=
     | ?pat :: ?pats =>
        let H := iFresh in iIntro H; iDestructHyp H as pat; go pats
     end
-  in let pats := intro_pat.parse pat in iStartProof; go pats.
+  in let pats := intro_pat.parse pat in try iStartProof; go pats.
 Tactic Notation "iIntros" := iIntros [IAll].
 
 Tactic Notation "iIntros" "(" simple_intropattern(x1) ")" :=
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 356a64bd2e4979af2a9c5aaff32bcd92b6627f1d..c9afe2d6eeb62ea2612bb6272d3d9af5f9687efb 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -93,6 +93,10 @@ Proof.
   iIntros "# _ //".
 Qed.
 
+Lemma test_very_fast_iIntros P :
+  ∀ x y : nat, ⌜ x = y ⌝ -∗ P -∗ P.
+Proof. by iIntros. Qed.
+
 Lemma test_iDestruct_spatial_and P Q1 Q2 : P ∗ (Q1 ∧ Q2) -∗ P ∗ Q1.
 Proof. iIntros "[H1 [H2 _]]". by iFrame. Qed.