diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 42e4e4c3109ebe06e22edf31c9e1e66156826f17..7ff16dd1523a0252c962c5547972c16765d0ce51 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -306,7 +306,9 @@ Tactic Notation "iAssumption" :=
   end.
 
 (** * False *)
-Tactic Notation "iExFalso" := apply tac_ex_falso.
+Tactic Notation "iExFalso" :=
+  iStartProof;
+  apply tac_ex_falso.
 
 (** * Making hypotheses intuitionistic or pure *)
 Local Tactic Notation "iIntuitionistic" constr(H) "as" constr(H') :=