diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index d5c5779700a126f27da339fabe047c935dcd8665..02c4e2281d9af91361b00cf0d6ae4221aa8f777a 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -861,7 +861,7 @@ Tactic Notation "iRevertIntros" constr(Hs) "with" tactic(tac) :=
          match p with true => constr:([IAlwaysElim (IName H)]) | false => H end in
        iIntros H'
     end in
-  iElaborateSelPat Hs go.
+  try iStartProof; iElaborateSelPat Hs go.
 
 Tactic Notation "iRevertIntros" "(" ident(x1) ")" constr(Hs) "with" tactic(tac):=
   iRevertIntros Hs with (iRevert (x1); tac; iIntros (x1)).