simpl breaks error checking of `iNext (S i)`
I'd expect iNext (S i)
to introduce exactly S i
later, and fail otherwise. However, after e.g. simpl
turns ▷^(S i) P
into ▷ ▷^i P
, that will sometimes introduce one later, as shown below.
From iris.proofmode Require Import tactics.
Lemma foo i {PROP} P : P ⊢@{PROP} ▷^(S i) P.
Proof.
iIntros "H".
Fail iNext 2.
iNext (S i).
Fail iNext i.
Fail iNext.
iExact "H".
Restart.
iIntros "H /=".
Fail iNext 2.
iNext (S i).
iNext i. (* !!! *)
Abort.
Iris version
$ opam show coq-iris -f version
dev.2020-05-24.2.af5e50e7
with Coq 8.11.1.