From 0706378f8dcea45df2676da9f59f1de6c791bca5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 24 Jul 2023 15:00:19 +0200
Subject: [PATCH] Let `iExFalso` perform `iStartProof`.

---
 iris/proofmode/ltac_tactics.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 42e4e4c31..7ff16dd15 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') :=
-- 
GitLab