diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 822786b442f71d6ce43cd02437d595ef3390a443..c50c6dbd85d7114a304455dee26bb56873731de1 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -986,7 +986,8 @@ Tactic Notation "iModIntro" := iModIntro _.
 Tactic Notation "iAlways" := iModIntro.
 
 (** * Later *)
-Tactic Notation "iNext":= iAlways.
+Tactic Notation "iNext" open_constr(n) := iModIntro (modality_laterN n).
+Tactic Notation "iNext" := iModIntro (modality_laterN _).
 
 (** * Update modality *)
 Tactic Notation "iModCore" constr(H) :=