Commit 4734a531 authored by Robbert Krebbers's avatar Robbert Krebbers

Restrict `iNext` to laters.

parent c8079d98
...@@ -986,7 +986,8 @@ Tactic Notation "iModIntro" := iModIntro _. ...@@ -986,7 +986,8 @@ Tactic Notation "iModIntro" := iModIntro _.
Tactic Notation "iAlways" := iModIntro. Tactic Notation "iAlways" := iModIntro.
(** * Later *) (** * Later *)
Tactic Notation "iNext":= iAlways. Tactic Notation "iNext" open_constr(n) := iModIntro (modality_laterN n).
Tactic Notation "iNext" := iModIntro (modality_laterN _).
(** * Update modality *) (** * Update modality *)
Tactic Notation "iModCore" constr(H) := Tactic Notation "iModCore" constr(H) :=
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment