From 4734a531b1df1e4bd68a3a6b278f391cdb8565e4 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 23 Feb 2018 13:54:13 +0100
Subject: [PATCH] Restrict `iNext` to laters.

---
 theories/proofmode/tactics.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 822786b44..c50c6dbd8 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) :=
-- 
GitLab