diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 7f3d22d44be683dea4e1cc8be87017ca4d8ce258..8fad7e78684f3c4aff74af7cf5fdf641f0cf2a10 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -515,7 +515,7 @@ Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
   iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 x6 x7 x8 } pat).
 
 Tactic Notation "iDestruct" open_constr(H) "as" "%" simple_intropattern(pat) :=
-  let Htmp := iFresh in iDestruct H as Htmp; iPure Htmp as pat.
+  let Htmp := iFresh in iDestruct H as Htmp; last iPure Htmp as pat.
 
 (** * Always *)
 Tactic Notation "iAlways":=