iNext does not remove diamonds from hypotheses
iNext does not remove diamonds from hypotheses. This feature could be useful, as otherwise you have to iMod everything. Example:
From iris Require Import proofmode.tactics.
Lemma foo {PROP : bi} (P : PROP) :
◇ P ⊢ ▷ P.
Proof.
iIntros "H". iNext.
Admitted.