diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 61762f93c58b6ebab0a6cf230ce67846ac6714e7..f329c4624a688ab752693de3a6b826ef01829893 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -158,6 +158,7 @@ Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
     |intros pat].
 
 Tactic Notation "iPureIntro" :=
+  iStartProof;
   eapply tac_pure_intro;
     [let P := match goal with |- FromPure ?P _ => P end in
      apply _ || fail "iPureIntro:" P "not pure"|].