Replace `iNext` by `iModIntro`.

theories/proofmode/class_instances.v

@@ -1458,10 +1458,11 @@ Global Instance is_except_0_fupd `{FUpdFacts PROP} E1 E2 P :
 Proof. by rewrite /IsExcept0 except_0_fupd. Qed.
 
 (* FromModal *)
-Global Instance from_modal_later P : FromModal (modality_laterN 1) (▷ P) P.
-Proof. by rewrite /FromModal. Qed.
-Global Instance from_modal_laterN n P : FromModal (modality_laterN n) (▷^n P) P.
-Proof. by rewrite /FromModal. Qed.
+Global Instance from_modal_later n P Q :
+  NoBackTrack (FromLaterN n P Q) →
+  TCIf (TCEq n 0) False TCTrue →
+  FromModal (modality_laterN n) P Q | 100.
+Proof. rewrite /FromLaterN /FromModal. by intros [?] [_ []|?]. Qed.
 Global Instance from_modal_except_0 P : FromModal modality_except_0 (◇ P) P.
 Proof. by rewrite /FromModal. Qed.
 

theories/proofmode/coq_tactics.v

@@ -1250,6 +1250,8 @@ Proof.
 Qed.
 
 (** * Later *)
+(** Although the `iNext` tactic no longer exists, much of its infrastructure is
+still used by other tactics, e.g. the symbolic execution tactics. *)
 Class MaybeIntoLaterNEnv (n : nat) (Γ1 Γ2 : env PROP) :=
   into_laterN_env : env_Forall2 (MaybeIntoLaterN false n) Γ1 Γ2.
 Class MaybeIntoLaterNEnvs (n : nat) (Δ1 Δ2 : envs PROP) := {
@@ -1282,14 +1284,6 @@ Proof.
   - induction Hs; rewrite /= ?laterN_sep. apply laterN_intro. by apply sep_mono.
 Qed.
 
-Lemma tac_next Δ Δ' n Q Q' :
-  FromLaterN n Q Q' → MaybeIntoLaterNEnvs n Δ Δ' →
-  envs_entails Δ' Q' → envs_entails Δ Q.
-Proof.
-  rewrite envs_entails_eq => ?? HQ.
-  by rewrite -(from_laterN n Q) into_laterN_env_sound HQ.
-Qed.
-
 Lemma tac_löb Δ Δ' i Q :
   env_spatial_is_nil Δ = true →
   envs_app true (Esnoc Enil i (▷ Q)%I) Δ = Some Δ' →

theories/proofmode/tactics.v

@@ -989,22 +989,7 @@ Tactic Notation "iModIntro":=
 Tactic Notation "iAlways" := iModIntro.
 
 (** * Later *)
-Tactic Notation "iNext" open_constr(n) :=
-  iStartProof;
-  let P := match goal with |- envs_entails _ ?P => P end in
-  try lazymatch n with 0 => fail 1 "iNext: cannot strip 0 laters" end;
-  (* apply is sometimes confused wrt. canonical structures search.
-     refine should use the other unification algorithm, which should
-     not have this issue. *)
-  notypeclasses refine (tac_next _ _ n _ _ _ _ _);
-    [apply _ || fail "iNext:" P "does not contain" n "laters"
-    |lazymatch goal with
-     | |- MaybeIntoLaterNEnvs 0 _ _ => fail "iNext:" P "does not contain laters"
-     | _ => apply _
-     end
-    |lazy beta (* remove beta redexes caused by removing laters under binders*)].
-
-Tactic Notation "iNext":= iNext _.
+Tactic Notation "iNext":= iAlways.
 
 (** * Update modality *)
 Tactic Notation "iModCore" constr(H) :=