diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index ca5444076c210e36d87f595eb1cc68ca6ad5aa27..6764fa796dc3ce52f2580032d37f502e62aa61ff 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -1263,7 +1263,7 @@ Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic(tac) :=
       | 1 => repeat iIntroForall; let H := iFresh in iIntro H; tac H
       | S ?n' => repeat iIntroForall; let H := iFresh in iIntro H; go n'
       end in
-    intros; iStartProof; go n in
+    intros; go n in
   lazymatch type of lem with
   | nat => intro_destruct lem
   | Z => (* to make it work in Z_scope. We should just be able to bind