diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 6f6c6cc681e77df65c47b8f20a01b3d758b55740..0515795d034cba2e6f99ff57508f8f90f6dc28d2 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -681,7 +681,7 @@ Tactic Notation "iIntros" constr(pat) :=
     | IName ?H :: ?pats => iIntro H; go pats
     | IPersistent IAnom :: ?pats => let H := iFresh in iIntro #H; go pats
     | IAnom :: ?pats => let H := iFresh in iIntro H; go pats
-    | IAnomPure :: ?pats => iPureIntro; go pats
+    | IAnomPure :: ?pats => iIntro {?}; go pats
     | IPersistent ?pat :: ?pats =>
        let H := iFresh in iIntro #H; iDestructHyp H as pat; go pats
     | ?pat :: ?pats =>