diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 6957533e657ac91047f2519f77bcbdf8f094c6d7..d20f2a92b9576c2cd6bbb88ac4206d1b5f5b3770 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -4,55 +4,100 @@ From iris.proofmode Require Export classes.
 Set Default Proof Using "Type".
 Import bi.
 
-Section always_modalities.
+Section bi_modalities.
   Context {PROP : bi}.
-  Lemma always_modality_persistently_mixin :
-    always_modality_mixin (@bi_persistently PROP) AIEnvId AIEnvClear.
+  Lemma modality_persistently_mixin :
+    modality_mixin (@bi_persistently PROP) MIEnvId MIEnvClear.
   Proof.
     split; eauto using equiv_entails_sym, persistently_intro, persistently_mono,
       persistently_sep_2 with typeclass_instances.
   Qed.
-  Definition always_modality_persistently :=
-    AlwaysModality _ always_modality_persistently_mixin.
+  Definition modality_persistently :=
+    Modality _ modality_persistently_mixin.
 
-  Lemma always_modality_affinely_mixin :
-    always_modality_mixin (@bi_affinely PROP) AIEnvId (AIEnvForall Affine).
+  Lemma modality_affinely_mixin :
+    modality_mixin (@bi_affinely PROP) MIEnvId (MIEnvForall Affine).
   Proof.
     split; eauto using equiv_entails_sym, affinely_intro, affinely_mono,
       affinely_sep_2 with typeclass_instances.
   Qed.
-  Definition always_modality_affinely :=
-    AlwaysModality _ always_modality_affinely_mixin.
+  Definition modality_affinely :=
+    Modality _ modality_affinely_mixin.
 
-  Lemma always_modality_affinely_persistently_mixin :
-    always_modality_mixin (λ P : PROP, □ P)%I AIEnvId AIEnvIsEmpty.
+  Lemma modality_affinely_persistently_mixin :
+    modality_mixin (λ P : PROP, □ P)%I MIEnvId MIEnvIsEmpty.
   Proof.
     split; eauto using equiv_entails_sym, affinely_persistently_emp,
       affinely_mono, persistently_mono, affinely_persistently_idemp,
       affinely_persistently_sep_2 with typeclass_instances.
   Qed.
-  Definition always_modality_affinely_persistently :=
-    AlwaysModality _ always_modality_affinely_persistently_mixin.
+  Definition modality_affinely_persistently :=
+    Modality _ modality_affinely_persistently_mixin.
 
-  Lemma always_modality_plainly_mixin :
-    always_modality_mixin (@bi_plainly PROP) (AIEnvForall Plain) AIEnvClear.
+  Lemma modality_plainly_mixin :
+    modality_mixin (@bi_plainly PROP) (MIEnvForall Plain) MIEnvClear.
   Proof.
     split; split_and?; eauto using equiv_entails_sym, plainly_intro, plainly_mono,
       plainly_and, plainly_sep_2 with typeclass_instances.
   Qed.
-  Definition always_modality_plainly :=
-    AlwaysModality _ always_modality_plainly_mixin.
+  Definition modality_plainly :=
+    Modality _ modality_plainly_mixin.
 
-  Lemma always_modality_affinely_plainly_mixin :
-    always_modality_mixin (λ P : PROP, ■ P)%I (AIEnvForall Plain) AIEnvIsEmpty.
+  Lemma modality_affinely_plainly_mixin :
+    modality_mixin (λ P : PROP, ■ P)%I (MIEnvForall Plain) MIEnvIsEmpty.
   Proof.
     split; split_and?; eauto using equiv_entails_sym, affinely_plainly_emp, affinely_intro,
       plainly_intro, affinely_mono, plainly_mono, affinely_plainly_idemp,
       affinely_plainly_and, affinely_plainly_sep_2 with typeclass_instances.
   Qed.
-  Definition always_modality_affinely_plainly :=
-    AlwaysModality _ always_modality_affinely_plainly_mixin.
-End always_modalities.
+  Definition modality_affinely_plainly :=
+    Modality _ modality_affinely_plainly_mixin.
+
+  Lemma modality_absorbingly_mixin :
+    modality_mixin (@bi_absorbingly PROP) MIEnvId MIEnvId.
+  Proof.
+    split; eauto using equiv_entails_sym, absorbingly_intro,
+      absorbingly_mono, absorbingly_sep.
+  Qed.
+  Definition modality_absorbingly :=
+    Modality _ modality_absorbingly_mixin.
+End bi_modalities.
+
+Section sbi_modalities.
+  Context {PROP : sbi}.
+
+  Lemma modality_except_0_mixin :
+    modality_mixin (@sbi_except_0 PROP) MIEnvId MIEnvId.
+  Proof.
+    split; eauto using equiv_entails_sym,
+      except_0_intro, except_0_mono, except_0_sep.
+  Qed.
+  Definition modality_except_0 :=
+    Modality _ modality_except_0_mixin.
+
+  Lemma modality_laterN_mixin n :
+    modality_mixin (@sbi_laterN PROP n)
+      (MIEnvTransform (MaybeIntoLaterN false n)) (MIEnvTransform (MaybeIntoLaterN false n)).
+  Proof.
+    split; split_and?; eauto using equiv_entails_sym, laterN_intro, laterN_mono,
+      laterN_and, laterN_sep with typeclass_instances.
+    rewrite /MaybeIntoLaterN=> P Q ->. by rewrite laterN_affinely_persistently_2.
+  Qed.
+  Definition modality_laterN n :=
+    Modality _ (modality_laterN_mixin n).
+
+  Lemma modality_bupd_mixin `{BUpdFacts PROP} :
+    modality_mixin (@bupd PROP _) MIEnvId MIEnvId.
+  Proof. split; eauto using bupd_intro, bupd_mono, bupd_sep. Qed.
+  Definition modality_bupd `{BUpdFacts PROP} :=
+    Modality _ modality_bupd_mixin.
+
+  Lemma modality_fupd_mixin `{FUpdFacts PROP} E :
+    modality_mixin (@fupd PROP _ E E) MIEnvId MIEnvId.
+  Proof. split; eauto using fupd_intro, fupd_mono, fupd_sep. Qed.
+  Definition modality_fupd `{FUpdFacts PROP} E :=
+    Modality _ (modality_fupd_mixin E).
+End sbi_modalities.
 
 Section bi_instances.
 Context {PROP : bi}.
@@ -267,54 +312,54 @@ Global Instance into_persistent_persistent P :
   Persistent P → IntoPersistent false P P | 100.
 Proof. intros. by rewrite /IntoPersistent. Qed.
 
-(* FromAlways *)
-Global Instance from_always_affinely P :
-  FromAlways always_modality_affinely (bi_affinely P) P | 2.
-Proof. by rewrite /FromAlways. Qed.
-
-Global Instance from_always_persistently P :
-  FromAlways always_modality_persistently (bi_persistently P) P | 2.
-Proof. by rewrite /FromAlways. Qed.
-Global Instance from_always_affinely_persistently P :
-  FromAlways always_modality_affinely_persistently (â–¡ P) P | 1.
-Proof. by rewrite /FromAlways. Qed.
-Global Instance from_always_affinely_persistently_affine_bi P :
-  BiAffine PROP → FromAlways always_modality_persistently (□ P) P | 0.
-Proof. intros. by rewrite /FromAlways /= affine_affinely. Qed.
-
-Global Instance from_always_plainly P :
-  FromAlways always_modality_plainly (bi_plainly P) P | 2.
-Proof. by rewrite /FromAlways. Qed.
-Global Instance from_always_affinely_plainly P :
-  FromAlways always_modality_affinely_plainly (â–  P) P | 1.
-Proof. by rewrite /FromAlways. Qed.
-Global Instance from_always_affinely_plainly_affine_bi P :
-  BiAffine PROP → FromAlways always_modality_plainly (■ P) P | 0.
-Proof. intros. by rewrite /FromAlways /= affine_affinely. Qed.
-
-Global Instance from_always_affinely_embed `{BiEmbedding PROP PROP'} P Q :
-  FromAlways always_modality_affinely P Q →
-  FromAlways always_modality_affinely ⎡P⎤ ⎡Q⎤.
-Proof. rewrite /FromAlways /= =><-. by rewrite bi_embed_affinely. Qed.
-Global Instance from_always_persistently_embed `{BiEmbedding PROP PROP'} P Q :
-  FromAlways always_modality_persistently P Q →
-  FromAlways always_modality_persistently ⎡P⎤ ⎡Q⎤.
-Proof. rewrite /FromAlways /= =><-. by rewrite bi_embed_persistently. Qed.
-Global Instance from_always_affinely_persistently_embed `{BiEmbedding PROP PROP'} P Q :
-  FromAlways always_modality_affinely_persistently P Q →
-  FromAlways always_modality_affinely_persistently ⎡P⎤ ⎡Q⎤.
-Proof.
-  rewrite /FromAlways /= =><-. by rewrite bi_embed_affinely bi_embed_persistently.
-Qed.
-Global Instance from_always_plainly_embed `{BiEmbedding PROP PROP'} P Q :
-  FromAlways always_modality_plainly P Q →
-  FromAlways always_modality_plainly ⎡P⎤ ⎡Q⎤.
-Proof. rewrite /FromAlways /= =><-. by rewrite bi_embed_plainly. Qed.
-Global Instance from_always_affinely_plainly_embed `{BiEmbedding PROP PROP'} P Q :
-  FromAlways always_modality_affinely_plainly P Q →
-  FromAlways always_modality_affinely_plainly ⎡P⎤ ⎡Q⎤.
-Proof.
-  rewrite /FromAlways /= =><-. by rewrite bi_embed_affinely bi_embed_plainly.
+(* FromModal *)
+Global Instance from_modal_affinely P :
+  FromModal modality_affinely (bi_affinely P) P | 2.
+Proof. by rewrite /FromModal. Qed.
+
+Global Instance from_modal_persistently P :
+  FromModal modality_persistently (bi_persistently P) P | 2.
+Proof. by rewrite /FromModal. Qed.
+Global Instance from_modal_affinely_persistently P :
+  FromModal modality_affinely_persistently (â–¡ P) P | 1.
+Proof. by rewrite /FromModal. Qed.
+Global Instance from_modal_affinely_persistently_affine_bi P :
+  BiAffine PROP → FromModal modality_persistently (□ P) P | 0.
+Proof. intros. by rewrite /FromModal /= affine_affinely. Qed.
+
+Global Instance from_modal_plainly P :
+  FromModal modality_plainly (bi_plainly P) P | 2.
+Proof. by rewrite /FromModal. Qed.
+Global Instance from_modal_affinely_plainly P :
+  FromModal modality_affinely_plainly (â–  P) P | 1.
+Proof. by rewrite /FromModal. Qed.
+Global Instance from_modal_affinely_plainly_affine_bi P :
+  BiAffine PROP → FromModal modality_plainly (■ P) P | 0.
+Proof. intros. by rewrite /FromModal /= affine_affinely. Qed.
+
+Global Instance from_modal_affinely_embed `{BiEmbedding PROP PROP'} P Q :
+  FromModal modality_affinely P Q →
+  FromModal modality_affinely ⎡P⎤ ⎡Q⎤.
+Proof. rewrite /FromModal /= =><-. by rewrite bi_embed_affinely. Qed.
+Global Instance from_modal_persistently_embed `{BiEmbedding PROP PROP'} P Q :
+  FromModal modality_persistently P Q →
+  FromModal modality_persistently ⎡P⎤ ⎡Q⎤.
+Proof. rewrite /FromModal /= =><-. by rewrite bi_embed_persistently. Qed.
+Global Instance from_modal_affinely_persistently_embed `{BiEmbedding PROP PROP'} P Q :
+  FromModal modality_affinely_persistently P Q →
+  FromModal modality_affinely_persistently ⎡P⎤ ⎡Q⎤.
+Proof.
+  rewrite /FromModal /= =><-. by rewrite bi_embed_affinely bi_embed_persistently.
+Qed.
+Global Instance from_modal_plainly_embed `{BiEmbedding PROP PROP'} P Q :
+  FromModal modality_plainly P Q →
+  FromModal modality_plainly ⎡P⎤ ⎡Q⎤.
+Proof. rewrite /FromModal /= =><-. by rewrite bi_embed_plainly. Qed.
+Global Instance from_modal_affinely_plainly_embed `{BiEmbedding PROP PROP'} P Q :
+  FromModal modality_affinely_plainly P Q →
+  FromModal modality_affinely_plainly ⎡P⎤ ⎡Q⎤.
+Proof.
+  rewrite /FromModal /= =><-. by rewrite bi_embed_affinely bi_embed_plainly.
 Qed.
 
 (* IntoWand *)
@@ -1077,11 +1122,14 @@ Proof.
 Qed.
 
 (* FromModal *)
-Global Instance from_modal_absorbingly P : FromModal (bi_absorbingly P) P.
-Proof. apply absorbingly_intro. Qed.
+Global Instance from_modal_absorbingly P :
+  FromModal modality_absorbingly (bi_absorbingly P) P.
+Proof. by rewrite /FromModal. Qed.
+(* FIXME
 Global Instance from_modal_embed `{BiEmbedding PROP PROP'} P Q :
   FromModal P Q → FromModal ⎡P⎤ ⎡Q⎤.
 Proof. by rewrite /FromModal=> ->. Qed.
+*)
 
 (* AsValid *)
 Global Instance as_valid_valid {PROP : bi} (P : PROP) : AsValid0 (bi_valid P) P | 0.
@@ -1410,15 +1458,19 @@ 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 (â–· P) P.
-Proof. apply later_intro. Qed.
-Global Instance from_modal_except_0 P : FromModal (â—‡ P) P.
-Proof. apply except_0_intro. Qed.
-
-Global Instance from_modal_bupd `{BUpdFacts PROP} P : FromModal (|==> P) P.
-Proof. apply bupd_intro. Qed.
-Global Instance from_modal_fupd E P `{FUpdFacts PROP} : FromModal (|={E}=> P) P.
-Proof. rewrite /FromModal. apply fupd_intro. Qed.
+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_except_0 P : FromModal modality_except_0 (â—‡ P) P.
+Proof. by rewrite /FromModal. Qed.
+
+Global Instance from_modal_bupd `{BUpdFacts PROP} P :
+  FromModal modality_bupd (|==> P) P.
+Proof. by rewrite /FromModal. Qed.
+Global Instance from_modal_fupd E P `{FUpdFacts PROP} :
+  FromModal (modality_fupd E) (|={E}=> P) P.
+Proof. by rewrite /FromModal. Qed.
 
 (* IntoInternalEq *)
 Global Instance into_internal_eq_internal_eq {A : ofeT} (x y : A) :
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 79f9e0340c893d36fda5b03a046ba70c4cfb2c99..1443eb7cf81d7535745565e8ab3d8fa922565f58 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -83,12 +83,11 @@ Arguments IntoPersistent {_} _ _%I _%I : simpl never.
 Arguments into_persistent {_} _ _%I _%I {_}.
 Hint Mode IntoPersistent + + ! - : typeclass_instances.
 
-(* The `iAlways` tactic is not tied to `persistently` and `affinely`, but can be
-instantiated with a variety of comonadic (always-style) modalities.
+(* The `iModIntro` tactic is not tied the Iris modalities, but can be
+instantiated with a variety of modalities.
 
-In order to plug in an always-style modality, one has to decide for both the
-persistent and spatial what action should be performed upon introducing the
-modality:
+In order to plug in a modality, one has to decide for both the persistent and
+spatial what action should be performed upon introducing the modality:
 
 - Introduction is only allowed when the context is empty.
 - Introduction is only allowed when all hypotheses satisfy some predicate
@@ -102,125 +101,124 @@ modality:
 
 Formally, these actions correspond to the following inductive type: *)
 
-Inductive always_intro_spec (PROP : bi) :=
-  | AIEnvIsEmpty
-  | AIEnvForall (C : PROP → Prop)
-  | AIEnvTransform (C : PROP → PROP → Prop)
-  | AIEnvClear
-  | AIEnvId.
-Arguments AIEnvIsEmpty {_}.
-Arguments AIEnvForall {_} _.
-Arguments AIEnvTransform {_} _.
-Arguments AIEnvClear {_}.
-Arguments AIEnvId {_}.
-
-Notation AIEnvFilter C := (AIEnvTransform (TCDiag C)).
-
-(* An always-style modality is then a record packing together the modality with
-the laws it should satisfy to justify the given actions for both contexts: *)
-Record always_modality_mixin {PROP : bi} (M : PROP → PROP)
-    (pspec sspec : always_intro_spec PROP) := {
-  always_modality_mixin_persistent :
+Inductive modality_intro_spec (PROP : bi) :=
+  | MIEnvIsEmpty
+  | MIEnvForall (C : PROP → Prop)
+  | MIEnvTransform (C : PROP → PROP → Prop)
+  | MIEnvClear
+  | MIEnvId.
+Arguments MIEnvIsEmpty {_}.
+Arguments MIEnvForall {_} _.
+Arguments MIEnvTransform {_} _.
+Arguments MIEnvClear {_}.
+Arguments MIEnvId {_}.
+
+Notation MIEnvFilter C := (MIEnvTransform (TCDiag C)).
+
+(* A modality is then a record packing together the modality with the laws it
+should satisfy to justify the given actions for both contexts: *)
+Record modality_mixin {PROP : bi} (M : PROP → PROP)
+    (pspec sspec : modality_intro_spec PROP) := {
+  modality_mixin_persistent :
     match pspec with
-    | AIEnvIsEmpty => True
-    | AIEnvForall C => (∀ P, C P → □ P ⊢ M (□ P)) ∧ (∀ P Q, M P ∧ M Q ⊢ M (P ∧ Q))
-    | AIEnvTransform C => (∀ P Q, C P Q → □ P ⊢ M (□ Q)) ∧ (∀ P Q, M P ∧ M Q ⊢ M (P ∧ Q))
-    | AIEnvClear => True
-    | AIEnvId => ∀ P, □ P ⊢ M (□ P)
+    | MIEnvIsEmpty => True
+    | MIEnvForall C => (∀ P, C P → □ P ⊢ M (□ P)) ∧ (∀ P Q, M P ∧ M Q ⊢ M (P ∧ Q))
+    | MIEnvTransform C => (∀ P Q, C P Q → □ P ⊢ M (□ Q)) ∧ (∀ P Q, M P ∧ M Q ⊢ M (P ∧ Q))
+    | MIEnvClear => True
+    | MIEnvId => ∀ P, □ P ⊢ M (□ P)
     end;
-  always_modality_mixin_spatial :
+  modality_mixin_spatial :
     match sspec with
-    | AIEnvIsEmpty => True
-    | AIEnvForall C => ∀ P, C P → P ⊢ M P
-    | AIEnvTransform C => (∀ P Q, C P Q → P ⊢ M Q)
-    | AIEnvClear => ∀ P, Absorbing (M P)
-    | AIEnvId => ∀ P, P ⊢ M P
+    | MIEnvIsEmpty => True
+    | MIEnvForall C => ∀ P, C P → P ⊢ M P
+    | MIEnvTransform C => (∀ P Q, C P Q → P ⊢ M Q)
+    | MIEnvClear => ∀ P, Absorbing (M P)
+    | MIEnvId => ∀ P, P ⊢ M P
     end;
-  always_modality_mixin_emp : emp ⊢ M emp;
-  always_modality_mixin_mono P Q : (P ⊢ Q) → M P ⊢ M Q;
-  always_modality_mixin_sep P Q : M P ∗ M Q ⊢ M (P ∗ Q)
+  modality_mixin_emp : emp ⊢ M emp;
+  modality_mixin_mono P Q : (P ⊢ Q) → M P ⊢ M Q;
+  modality_mixin_sep P Q : M P ∗ M Q ⊢ M (P ∗ Q)
 }.
 
-Record always_modality (PROP : bi) := AlwaysModality {
-  always_modality_car :> PROP → PROP;
-  always_modality_persistent_spec : always_intro_spec PROP;
-  always_modality_spatial_spec : always_intro_spec PROP;
-  always_modality_mixin_of : always_modality_mixin
-    always_modality_car
-    always_modality_persistent_spec always_modality_spatial_spec
+Record modality (PROP : bi) := Modality {
+  modality_car :> PROP → PROP;
+  modality_persistent_spec : modality_intro_spec PROP;
+  modality_spatial_spec : modality_intro_spec PROP;
+  modality_mixin_of :
+    modality_mixin modality_car modality_persistent_spec modality_spatial_spec
 }.
-Arguments AlwaysModality {_} _ {_ _} _.
-Arguments always_modality_persistent_spec {_} _.
-Arguments always_modality_spatial_spec {_} _.
+Arguments Modality {_} _ {_ _} _.
+Arguments modality_persistent_spec {_} _.
+Arguments modality_spatial_spec {_} _.
 
-Section always_modality.
-  Context {PROP} (M : always_modality PROP).
+Section modality.
+  Context {PROP} (M : modality PROP).
 
-  Lemma always_modality_persistent_forall C P :
-    always_modality_persistent_spec M = AIEnvForall C → C P → □ P ⊢ M (□ P).
+  Lemma modality_persistent_forall C P :
+    modality_persistent_spec M = MIEnvForall C → C P → □ P ⊢ M (□ P).
   Proof. destruct M as [??? []]; naive_solver. Qed.
-  Lemma always_modality_and_forall C P Q :
-    always_modality_persistent_spec M = AIEnvForall C → M P ∧ M Q ⊢ M (P ∧ Q).
+  Lemma modality_and_forall C P Q :
+    modality_persistent_spec M = MIEnvForall C → M P ∧ M Q ⊢ M (P ∧ Q).
   Proof. destruct M as [??? []]; naive_solver. Qed.
-  Lemma always_modality_persistent_transform C P Q :
-    always_modality_persistent_spec M = AIEnvTransform C → C P Q → □ P ⊢ M (□ Q).
+  Lemma modality_persistent_transform C P Q :
+    modality_persistent_spec M = MIEnvTransform C → C P Q → □ P ⊢ M (□ Q).
   Proof. destruct M as [??? []]; naive_solver. Qed.
-  Lemma always_modality_and_transform C P Q :
-    always_modality_persistent_spec M = AIEnvTransform C → M P ∧ M Q ⊢ M (P ∧ Q).
+  Lemma modality_and_transform C P Q :
+    modality_persistent_spec M = MIEnvTransform C → M P ∧ M Q ⊢ M (P ∧ Q).
   Proof. destruct M as [??? []]; naive_solver. Qed.
-  Lemma always_modality_persistent_id P :
-    always_modality_persistent_spec M = AIEnvId → □ P ⊢ M (□ P).
+  Lemma modality_persistent_id P :
+    modality_persistent_spec M = MIEnvId → □ P ⊢ M (□ P).
   Proof. destruct M as [??? []]; naive_solver. Qed.
-  Lemma always_modality_spatial_forall C P :
-    always_modality_spatial_spec M = AIEnvForall C → C P → P ⊢ M P.
+  Lemma modality_spatial_forall C P :
+    modality_spatial_spec M = MIEnvForall C → C P → P ⊢ M P.
   Proof. destruct M as [??? []]; naive_solver. Qed.
-  Lemma always_modality_spatial_transform C P Q :
-    always_modality_spatial_spec M = AIEnvTransform C → C P Q → P ⊢ M Q.
+  Lemma modality_spatial_transform C P Q :
+    modality_spatial_spec M = MIEnvTransform C → C P Q → P ⊢ M Q.
   Proof. destruct M as [??? []]; naive_solver. Qed.
-  Lemma always_modality_spatial_clear P :
-    always_modality_spatial_spec M = AIEnvClear → Absorbing (M P).
+  Lemma modality_spatial_clear P :
+    modality_spatial_spec M = MIEnvClear → Absorbing (M P).
   Proof. destruct M as [??? []]; naive_solver. Qed.
-  Lemma always_modality_spatial_id P :
-    always_modality_spatial_spec M = AIEnvId → P ⊢ M P.
+  Lemma modality_spatial_id P :
+    modality_spatial_spec M = MIEnvId → P ⊢ M P.
   Proof. destruct M as [??? []]; naive_solver. Qed.
 
-  Lemma always_modality_emp : emp ⊢ M emp.
-  Proof. eapply always_modality_mixin_emp, always_modality_mixin_of. Qed.
-  Lemma always_modality_mono P Q : (P ⊢ Q) → M P ⊢ M Q.
-  Proof. eapply always_modality_mixin_mono, always_modality_mixin_of. Qed.
-  Lemma always_modality_sep P Q : M P ∗ M Q ⊢ M (P ∗ Q).
-  Proof. eapply always_modality_mixin_sep, always_modality_mixin_of. Qed.
-  Global Instance always_modality_mono' : Proper ((⊢) ==> (⊢)) M.
-  Proof. intros P Q. apply always_modality_mono. Qed.
-  Global Instance always_modality_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) M.
-  Proof. intros P Q. apply always_modality_mono. Qed.
-  Global Instance always_modality_proper : Proper ((≡) ==> (≡)) M.
-  Proof. intros P Q. rewrite !equiv_spec=> -[??]; eauto using always_modality_mono. Qed.
-
-  Lemma always_modality_persistent_forall_big_and C Ps :
-    always_modality_persistent_spec M = AIEnvForall C →
+  Lemma modality_emp : emp ⊢ M emp.
+  Proof. eapply modality_mixin_emp, modality_mixin_of. Qed.
+  Lemma modality_mono P Q : (P ⊢ Q) → M P ⊢ M Q.
+  Proof. eapply modality_mixin_mono, modality_mixin_of. Qed.
+  Lemma modality_sep P Q : M P ∗ M Q ⊢ M (P ∗ Q).
+  Proof. eapply modality_mixin_sep, modality_mixin_of. Qed.
+  Global Instance modality_mono' : Proper ((⊢) ==> (⊢)) M.
+  Proof. intros P Q. apply modality_mono. Qed.
+  Global Instance modality_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) M.
+  Proof. intros P Q. apply modality_mono. Qed.
+  Global Instance modality_proper : Proper ((≡) ==> (≡)) M.
+  Proof. intros P Q. rewrite !equiv_spec=> -[??]; eauto using modality_mono. Qed.
+
+  Lemma modality_persistent_forall_big_and C Ps :
+    modality_persistent_spec M = MIEnvForall C →
     Forall C Ps → □ [∧] Ps ⊢ M (□ [∧] Ps).
   Proof.
     induction 2 as [|P Ps ? _ IH]; simpl.
-    - by rewrite persistently_pure affinely_True_emp affinely_emp -always_modality_emp.
-    - rewrite affinely_persistently_and -always_modality_and_forall // -IH.
-      by rewrite {1}(always_modality_persistent_forall _ P).
+    - by rewrite persistently_pure affinely_True_emp affinely_emp -modality_emp.
+    - rewrite affinely_persistently_and -modality_and_forall // -IH.
+      by rewrite {1}(modality_persistent_forall _ P).
   Qed.
-  Lemma always_modality_spatial_forall_big_sep C Ps :
-    always_modality_spatial_spec M = AIEnvForall C →
+  Lemma modality_spatial_forall_big_sep C Ps :
+    modality_spatial_spec M = MIEnvForall C →
     Forall C Ps → [∗] Ps ⊢ M ([∗] Ps).
   Proof.
     induction 2 as [|P Ps ? _ IH]; simpl.
-    - by rewrite -always_modality_emp.
-    - by rewrite -always_modality_sep -IH {1}(always_modality_spatial_forall _ P).
+    - by rewrite -modality_emp.
+    - by rewrite -modality_sep -IH {1}(modality_spatial_forall _ P).
   Qed.
-End always_modality.
+End modality.
 
-Class FromAlways {PROP : bi} (M : always_modality PROP) (P Q : PROP) :=
-  from_always : M Q ⊢ P.
-Arguments FromAlways {_} _ _%I _%I : simpl never.
-Arguments from_always {_} _ _%I _%I {_}.
-Hint Mode FromAlways + - ! - : typeclass_instances.
+Class FromModal {PROP : bi} (M : modality PROP) (P Q : PROP) :=
+  from_modal : M Q ⊢ P.
+Arguments FromModal {_} _ _%I _%I : simpl never.
+Arguments from_modal {_} _ _%I _%I {_}.
+Hint Mode FromModal + - ! - : typeclass_instances.
 
 Class FromAffinely {PROP : bi} (P Q : PROP) :=
   from_affinely : bi_affinely Q ⊢ P.
@@ -338,11 +336,6 @@ Arguments IsExcept0 {_} _%I : simpl never.
 Arguments is_except_0 {_} _%I {_}.
 Hint Mode IsExcept0 + ! : typeclass_instances.
 
-Class FromModal {PROP : bi} (P Q : PROP) := from_modal : Q ⊢ P.
-Arguments FromModal {_} _%I _%I : simpl never.
-Arguments from_modal {_} _%I _%I {_}.
-Hint Mode FromModal + ! - : typeclass_instances.
-
 Class ElimModal {PROP : bi} (φ : Prop) (P P' : PROP) (Q Q' : PROP) :=
   elim_modal : φ → P ∗ (P' -∗ Q') ⊢ Q.
 Arguments ElimModal {_} _ _%I _%I _%I _%I : simpl never.
@@ -645,8 +638,8 @@ Instance into_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
   IntoExist P Φ → IntoExist (tc_opaque P) Φ := id.
 Instance into_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
   IntoForall P Φ → IntoForall (tc_opaque P) Φ := id.
-Instance from_modal_tc_opaque {PROP : bi} (P Q : PROP) :
-  FromModal P Q → FromModal (tc_opaque P) Q := id.
+Instance from_modal_tc_opaque {PROP : bi} M (P Q : PROP) :
+  FromModal M P Q → FromModal M (tc_opaque P) Q := id.
 Instance elim_modal_tc_opaque {PROP : bi} φ (P P' Q Q' : PROP) :
   ElimModal φ P P' Q Q' → ElimModal φ (tc_opaque P) P' Q Q' := id.
 Instance into_inv_tc_opaque {PROP : bi} (P : PROP) N :
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index f2e1b41ccaf11d0420339394e1458b1618678779..0be4b8574d8b9d96b0f0d122e827ee8bee11ae4c 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -583,149 +583,7 @@ Qed.
 Lemma tac_pure_revert Δ φ Q : envs_entails Δ (⌜φ⌝ → Q) → (φ → envs_entails Δ Q).
 Proof. rewrite envs_entails_eq. intros HΔ ?. by rewrite HΔ pure_True // left_id. Qed.
 
-(** * Always modalities *)
-(** Transforming *)
-Class TransformPersistentEnv
-    (M : always_modality PROP) (C : PROP → PROP → Prop) (Γ1 Γ2 : env PROP) := {
-  transform_persistent_env :
-    (∀ P Q, C P Q → □ P ⊢ M (□ Q)) →
-    (∀ P Q, M P ∧ M Q ⊢ M (P ∧ Q)) →
-    □ ([∧] Γ1) ⊢ M (□ ([∧] Γ2));
-  transform_persistent_env_wf : env_wf Γ1 → env_wf Γ2;
-  transform_persistent_env_dom i : Γ1 !! i = None → Γ2 !! i = None;
-}.
-Global Instance transform_persistent_env_nil M C : TransformPersistentEnv M C Enil Enil.
-Proof.
-  split=> // HC /=. rewrite !persistently_pure !affinely_True_emp.
-  by rewrite affinely_emp -always_modality_emp.
-Qed.
-Global Instance transform_persistent_env_snoc M (C : PROP → PROP → Prop) Γ Γ' i P Q :
-  C P Q →
-  TransformPersistentEnv M C Γ Γ' →
-  TransformPersistentEnv M C (Esnoc Γ i P) (Esnoc Γ' i Q).
-Proof.
-  intros ? [HΓ Hwf Hdom]; split; simpl.
-  - intros HC Hand. rewrite affinely_persistently_and HC // HΓ //.
-    by rewrite Hand -affinely_persistently_and.
-  - inversion 1; constructor; auto.
-  - intros j. destruct (ident_beq _ _); naive_solver.
-Qed.
-Global Instance transform_persistent_env_snoc_not M (C : PROP → PROP → Prop) Γ Γ' i P :
-  TransformPersistentEnv M C Γ Γ' →
-  TransformPersistentEnv M C (Esnoc Γ i P) Γ' | 100.
-Proof.
-  intros [HΓ Hwf Hdom]; split; simpl.
-  - intros HC Hand. by rewrite and_elim_r HΓ.
-  - inversion 1; auto.
-  - intros j. destruct (ident_beq _ _); naive_solver.
-Qed.
-
-Class TransformSpatialEnv
-    (M : always_modality PROP) (C : PROP → PROP → Prop)
-    (Γ1 Γ2 : env PROP) (filtered : bool) := {
-  transform_spatial_env :
-    (∀ P Q, C P Q → P ⊢ M Q) →
-    ([∗] Γ1) ⊢ M ([∗] Γ2) ∗ if filtered then True else emp;
-  transform_spatial_env_wf : env_wf Γ1 → env_wf Γ2;
-  transform_spatial_env_dom i : Γ1 !! i = None → Γ2 !! i = None;
-}.
-Global Instance transform_spatial_env_nil M C :
-  TransformSpatialEnv M C Enil Enil false.
-Proof. split=> // HC /=. by rewrite right_id -always_modality_emp. Qed.
-Global Instance transform_spatial_env_snoc M (C : PROP → PROP → Prop) Γ Γ' i P Q fi :
-  C P Q →
-  TransformSpatialEnv M C Γ Γ' fi →
-  TransformSpatialEnv M C (Esnoc Γ i P) (Esnoc Γ' i Q) fi.
-Proof.
-  intros ? [HΓ Hwf Hdom]; split; simpl.
-  - intros HC. by rewrite {1}(HC P) // HΓ // assoc always_modality_sep.
-  - inversion 1; constructor; auto.
-  - intros j. destruct (ident_beq _ _); naive_solver.
-Qed.
-
-Global Instance transform_spatial_env_snoc_not
-    M (C : PROP → PROP → Prop) Γ Γ' i P fi fi' :
-  TransformSpatialEnv M C Γ Γ' fi →
-  TCIf (TCEq fi false)
-    (TCIf (Affine P) (TCEq fi' false) (TCEq fi' true))
-    (TCEq fi' true) →
-  TransformSpatialEnv M C (Esnoc Γ i P) Γ' fi' | 100.
-Proof.
-  intros [HΓ Hwf Hdom] Hif; split; simpl.
-  - intros ?. rewrite HΓ //. destruct Hif as [-> [? ->| ->]| ->].
-    + by rewrite (affine P) left_id.
-    + by rewrite right_id comm (True_intro P).
-    + by rewrite comm -assoc (True_intro (_ ∗ P)%I).
-  - inversion 1; auto.
-  - intros j. destruct (ident_beq _ _); naive_solver.
-Qed.
-
-(** The actual tactic *)
-Ltac tac_always_cases fi :=
-  simplify_eq/=;
-  repeat match goal with
-  | H : TCAnd _ _ |- _ => destruct H
-  | H : TCEq ?x _ |- _ => inversion H; subst x; clear H
-  | H : TCForall _ _ |- _ => apply TCForall_Forall in H
-  | H : TransformPersistentEnv _ _ _ _ |- _ => destruct H
-  | H : ∃ fi, TransformSpatialEnv _ _ _ _ fi ∧ _ |- _ => destruct H as [fi [[] ?]]
-  end; simpl; auto using Enil_wf.
-
-Lemma tac_always_intro Γp Γs Γp' Γs' M Q Q' :
-  FromAlways M Q' Q →
-  match always_modality_persistent_spec M with
-  | AIEnvForall C => TCAnd (TCForall C (env_to_list Γp)) (TCEq Γp Γp')
-  | AIEnvTransform C => TransformPersistentEnv M C Γp Γp'
-  | AIEnvIsEmpty => TCAnd (TCEq Γp Enil) (TCEq Γp' Enil)
-  | AIEnvClear => TCEq Γp' Enil
-  | AIEnvId => TCEq Γp Γp'
-  end →
-  match always_modality_spatial_spec M with
-  | AIEnvForall C => TCAnd (TCForall C (env_to_list Γs)) (TCEq Γs Γs')
-  | AIEnvTransform C =>
-     ∃ fi, TransformSpatialEnv M C Γs Γs' fi ∧
-     if fi then Absorbing Q' else TCTrue
-  | AIEnvIsEmpty => TCAnd (TCEq Γs Enil) (TCEq Γs' Enil)
-  | AIEnvClear => TCEq Γs' Enil
-  | AIEnvId => TCEq Γs Γs'
-  end →
-  envs_entails (Envs Γp' Γs') Q → envs_entails (Envs Γp Γs) Q'.
-Proof.
-  rewrite envs_entails_eq /FromAlways /of_envs /= => HQ' HΓp HΓs HQ.
-  apply pure_elim_l=> -[???]. assert (envs_wf (Envs Γp' Γs')) as Hwf.
-  { split; simpl in *.
-    - destruct (always_modality_persistent_spec M); tac_always_cases fi.
-    - destruct (always_modality_spatial_spec M); tac_always_cases fi.
-    - destruct (always_modality_persistent_spec M),
-        (always_modality_spatial_spec M); tac_always_cases fi; naive_solver. }
-  assert (□ [∧] Γp ⊢ M (□ [∧] Γp'))%I as HMp.
-  { destruct (always_modality_persistent_spec M) eqn:?; tac_always_cases fi.
-    + by rewrite {1}affinely_elim_emp (always_modality_emp M)
-        persistently_True_emp affinely_persistently_emp.
-    + eauto using always_modality_persistent_forall_big_and.
-    + eauto using always_modality_persistent_transform,
-        always_modality_and_transform.
-    + by rewrite {1}affinely_elim_emp (always_modality_emp M)
-        persistently_True_emp affinely_persistently_emp.
-    + eauto using always_modality_persistent_id. }
-  move: HQ'; rewrite -HQ pure_True // left_id HMp=> HQ' {HQ Hwf HMp}.
-  destruct (always_modality_spatial_spec M) eqn:?; tac_always_cases fi.
-  + by rewrite -HQ' /= !right_id.
-  + rewrite -HQ' {1}(always_modality_spatial_forall_big_sep _ _ Γs') //.
-    by rewrite always_modality_sep.
-  + destruct fi.
-    - rewrite -(absorbing Q') /bi_absorbingly -HQ' (comm _ True%I).
-      rewrite -always_modality_sep -assoc. apply sep_mono_r.
-      eauto using always_modality_spatial_transform.
-    - rewrite -HQ' -always_modality_sep. apply sep_mono_r.
-      rewrite -(right_id emp%I bi_sep (M _)).
-      eauto using always_modality_spatial_transform.
-  + rewrite -HQ' /= right_id comm -{2}(always_modality_spatial_clear M) //.
-    by rewrite (True_intro ([∗] Γs)%I).
-  + rewrite -HQ' {1}(always_modality_spatial_id M ([∗] Γs')%I) //.
-    by rewrite -always_modality_sep.
-Qed.
-
+(** * Persistence *)
 Lemma tac_persistent Δ Δ' i p P P' Q :
   envs_lookup i Δ = Some (p, P) →
   IntoPersistent p P P' →
@@ -1178,9 +1036,147 @@ Proof.
 Qed.
 
 (** * Modalities *)
-Lemma tac_modal_intro Δ P Q :
-  FromModal P Q → envs_entails Δ Q → envs_entails Δ P.
-Proof. by rewrite envs_entails_eq /FromModal=> <- ->. Qed.
+(** Transforming *)
+Class TransformPersistentEnv
+    (M : modality PROP) (C : PROP → PROP → Prop) (Γ1 Γ2 : env PROP) := {
+  transform_persistent_env :
+    (∀ P Q, C P Q → □ P ⊢ M (□ Q)) →
+    (∀ P Q, M P ∧ M Q ⊢ M (P ∧ Q)) →
+    □ ([∧] Γ1) ⊢ M (□ ([∧] Γ2));
+  transform_persistent_env_wf : env_wf Γ1 → env_wf Γ2;
+  transform_persistent_env_dom i : Γ1 !! i = None → Γ2 !! i = None;
+}.
+Global Instance transform_persistent_env_nil M C : TransformPersistentEnv M C Enil Enil.
+Proof.
+  split=> // HC /=. rewrite !persistently_pure !affinely_True_emp.
+  by rewrite affinely_emp -modality_emp.
+Qed.
+Global Instance transform_persistent_env_snoc M (C : PROP → PROP → Prop) Γ Γ' i P Q :
+  C P Q →
+  TransformPersistentEnv M C Γ Γ' →
+  TransformPersistentEnv M C (Esnoc Γ i P) (Esnoc Γ' i Q).
+Proof.
+  intros ? [HΓ Hwf Hdom]; split; simpl.
+  - intros HC Hand. rewrite affinely_persistently_and HC // HΓ //.
+    by rewrite Hand -affinely_persistently_and.
+  - inversion 1; constructor; auto.
+  - intros j. destruct (ident_beq _ _); naive_solver.
+Qed.
+Global Instance transform_persistent_env_snoc_not M (C : PROP → PROP → Prop) Γ Γ' i P :
+  TransformPersistentEnv M C Γ Γ' →
+  TransformPersistentEnv M C (Esnoc Γ i P) Γ' | 100.
+Proof.
+  intros [HΓ Hwf Hdom]; split; simpl.
+  - intros HC Hand. by rewrite and_elim_r HΓ.
+  - inversion 1; auto.
+  - intros j. destruct (ident_beq _ _); naive_solver.
+Qed.
+
+Class TransformSpatialEnv
+    (M : modality PROP) (C : PROP → PROP → Prop)
+    (Γ1 Γ2 : env PROP) (filtered : bool) := {
+  transform_spatial_env :
+    (∀ P Q, C P Q → P ⊢ M Q) →
+    ([∗] Γ1) ⊢ M ([∗] Γ2) ∗ if filtered then True else emp;
+  transform_spatial_env_wf : env_wf Γ1 → env_wf Γ2;
+  transform_spatial_env_dom i : Γ1 !! i = None → Γ2 !! i = None;
+}.
+Global Instance transform_spatial_env_nil M C :
+  TransformSpatialEnv M C Enil Enil false.
+Proof. split=> // HC /=. by rewrite right_id -modality_emp. Qed.
+Global Instance transform_spatial_env_snoc M (C : PROP → PROP → Prop) Γ Γ' i P Q fi :
+  C P Q →
+  TransformSpatialEnv M C Γ Γ' fi →
+  TransformSpatialEnv M C (Esnoc Γ i P) (Esnoc Γ' i Q) fi.
+Proof.
+  intros ? [HΓ Hwf Hdom]; split; simpl.
+  - intros HC. by rewrite {1}(HC P) // HΓ // assoc modality_sep.
+  - inversion 1; constructor; auto.
+  - intros j. destruct (ident_beq _ _); naive_solver.
+Qed.
+
+Global Instance transform_spatial_env_snoc_not
+    M (C : PROP → PROP → Prop) Γ Γ' i P fi fi' :
+  TransformSpatialEnv M C Γ Γ' fi →
+  TCIf (TCEq fi false)
+    (TCIf (Affine P) (TCEq fi' false) (TCEq fi' true))
+    (TCEq fi' true) →
+  TransformSpatialEnv M C (Esnoc Γ i P) Γ' fi' | 100.
+Proof.
+  intros [HΓ Hwf Hdom] Hif; split; simpl.
+  - intros ?. rewrite HΓ //. destruct Hif as [-> [? ->| ->]| ->].
+    + by rewrite (affine P) left_id.
+    + by rewrite right_id comm (True_intro P).
+    + by rewrite comm -assoc (True_intro (_ ∗ P)%I).
+  - inversion 1; auto.
+  - intros j. destruct (ident_beq _ _); naive_solver.
+Qed.
+
+(** The actual introduction tactic *)
+Ltac tac_modal_cases fi :=
+  simplify_eq/=;
+  repeat match goal with
+  | H : TCAnd _ _ |- _ => destruct H
+  | H : TCEq ?x _ |- _ => inversion H; subst x; clear H
+  | H : TCForall _ _ |- _ => apply TCForall_Forall in H
+  | H : TransformPersistentEnv _ _ _ _ |- _ => destruct H
+  | H : ∃ fi, TransformSpatialEnv _ _ _ _ fi ∧ _ |- _ => destruct H as [fi [[] ?]]
+  end; simpl; auto using Enil_wf.
+
+Lemma tac_modal_intro Γp Γs Γp' Γs' M Q Q' :
+  FromModal M Q' Q →
+  match modality_persistent_spec M with
+  | MIEnvForall C => TCAnd (TCForall C (env_to_list Γp)) (TCEq Γp Γp')
+  | MIEnvTransform C => TransformPersistentEnv M C Γp Γp'
+  | MIEnvIsEmpty => TCAnd (TCEq Γp Enil) (TCEq Γp' Enil)
+  | MIEnvClear => TCEq Γp' Enil
+  | MIEnvId => TCEq Γp Γp'
+  end →
+  match modality_spatial_spec M with
+  | MIEnvForall C => TCAnd (TCForall C (env_to_list Γs)) (TCEq Γs Γs')
+  | MIEnvTransform C =>
+     ∃ fi, TransformSpatialEnv M C Γs Γs' fi ∧
+     if fi then Absorbing Q' else TCTrue
+  | MIEnvIsEmpty => TCAnd (TCEq Γs Enil) (TCEq Γs' Enil)
+  | MIEnvClear => TCEq Γs' Enil
+  | MIEnvId => TCEq Γs Γs'
+  end →
+  envs_entails (Envs Γp' Γs') Q → envs_entails (Envs Γp Γs) Q'.
+Proof.
+  rewrite envs_entails_eq /FromModal /of_envs /= => HQ' HΓp HΓs HQ.
+  apply pure_elim_l=> -[???]. assert (envs_wf (Envs Γp' Γs')) as Hwf.
+  { split; simpl in *.
+    - destruct (modality_persistent_spec M); tac_modal_cases fi.
+    - destruct (modality_spatial_spec M); tac_modal_cases fi.
+    - destruct (modality_persistent_spec M),
+        (modality_spatial_spec M); tac_modal_cases fi; naive_solver. }
+  assert (□ [∧] Γp ⊢ M (□ [∧] Γp'))%I as HMp.
+  { destruct (modality_persistent_spec M) eqn:?; tac_modal_cases fi.
+    + by rewrite {1}affinely_elim_emp (modality_emp M)
+        persistently_True_emp affinely_persistently_emp.
+    + eauto using modality_persistent_forall_big_and.
+    + eauto using modality_persistent_transform,
+        modality_and_transform.
+    + by rewrite {1}affinely_elim_emp (modality_emp M)
+        persistently_True_emp affinely_persistently_emp.
+    + eauto using modality_persistent_id. }
+  move: HQ'; rewrite -HQ pure_True // left_id HMp=> HQ' {HQ Hwf HMp}.
+  destruct (modality_spatial_spec M) eqn:?; tac_modal_cases fi.
+  + by rewrite -HQ' /= !right_id.
+  + rewrite -HQ' {1}(modality_spatial_forall_big_sep _ _ Γs') //.
+    by rewrite modality_sep.
+  + destruct fi.
+    - rewrite -(absorbing Q') /bi_absorbingly -HQ' (comm _ True%I).
+      rewrite -modality_sep -assoc. apply sep_mono_r.
+      eauto using modality_spatial_transform.
+    - rewrite -HQ' -modality_sep. apply sep_mono_r.
+      rewrite -(right_id emp%I bi_sep (M _)).
+      eauto using modality_spatial_transform.
+  + rewrite -HQ' /= right_id comm -{2}(modality_spatial_clear M) //.
+    by rewrite (True_intro ([∗] Γs)%I).
+  + rewrite -HQ' {1}(modality_spatial_id M ([∗] Γs')%I) //.
+    by rewrite -modality_sep.
+Qed.
 
 Lemma tac_modal_elim Δ Δ' i p φ P' P Q Q' :
   envs_lookup i Δ = Some (p, P) →
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index 96890ce60dd59bbccd0c40ef61fdb037269963b8..b182599d4bc2fa2d8ba3d76b6ddfb438e6399385 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -14,21 +14,21 @@ Proof. by rewrite /IsBiIndexRel. Qed.
 Hint Extern 1 (IsBiIndexRel _ _) => unfold IsBiIndexRel; assumption
             : typeclass_instances.
 
-Section always_modalities.
+Section modalities.
   Context {I : biIndex} {PROP : bi}.
 
-  Lemma always_modality_absolutely_mixin :
-    always_modality_mixin (@monPred_absolutely I PROP)
-      (AIEnvFilter Absolute) (AIEnvFilter Absolute).
+  Lemma modality_absolutely_mixin :
+    modality_mixin (@monPred_absolutely I PROP)
+      (MIEnvFilter Absolute) (MIEnvFilter Absolute).
   Proof.
     split; split_and?; intros; try match goal with H : TCDiag _ _ _ |- _ => destruct H end;
       eauto using bi.equiv_entails_sym, absolute_absolutely,
         monPred_absolutely_mono, monPred_absolutely_and,
         monPred_absolutely_sep_2 with typeclass_instances.
   Qed.
-  Definition always_modality_absolutely :=
-    AlwaysModality _ always_modality_absolutely_mixin.
-End always_modalities.
+  Definition modality_absolutely :=
+    Modality _ modality_absolutely_mixin.
+End modalities.
 
 Section bi.
 Context {I : biIndex} {PROP : bi}.
@@ -39,9 +39,9 @@ Implicit Types 𝓟 𝓠 𝓡 : PROP.
 Implicit Types φ : Prop.
 Implicit Types i j : I.
 
-Global Instance from_always_absolutely P :
-  FromAlways always_modality_absolutely (∀ᵢ P) P | 1.
-Proof. by rewrite /FromAlways. Qed.
+Global Instance from_modal_absolutely P :
+  FromModal modality_absolutely (∀ᵢ P) P | 1.
+Proof. by rewrite /FromModal. Qed.
 
 Global Instance make_monPred_at_pure φ i : MakeMonPredAt i ⌜φ⌝ ⌜φ⌝.
 Proof. by rewrite /MakeMonPredAt monPred_at_pure. Qed.
@@ -154,23 +154,23 @@ Proof.
   by rewrite -monPred_at_persistently -monPred_at_persistently_if.
 Qed.
 
-Global Instance from_always_affinely_monPred_at P Q 𝓠 i :
-  FromAlways always_modality_affinely P Q → MakeMonPredAt i Q 𝓠 →
-  FromAlways always_modality_affinely (P i) 𝓠 | 0.
+Global Instance from_modal_affinely_monPred_at P Q 𝓠 i :
+  FromModal modality_affinely P Q → MakeMonPredAt i Q 𝓠 →
+  FromModal modality_affinely (P i) 𝓠 | 0.
 Proof.
-  rewrite /FromAlways /MakeMonPredAt /==> <- <-. by rewrite monPred_at_affinely.
+  rewrite /FromModal /MakeMonPredAt /==> <- <-. by rewrite monPred_at_affinely.
 Qed.
-Global Instance from_always_persistently_monPred_at P Q 𝓠 i :
-  FromAlways always_modality_persistently P Q → MakeMonPredAt i Q 𝓠 →
-  FromAlways always_modality_persistently (P i) 𝓠 | 0.
+Global Instance from_modal_persistently_monPred_at P Q 𝓠 i :
+  FromModal modality_persistently P Q → MakeMonPredAt i Q 𝓠 →
+  FromModal modality_persistently (P i) 𝓠 | 0.
 Proof.
-  rewrite /FromAlways /MakeMonPredAt /==> <- <-. by rewrite monPred_at_persistently.
+  rewrite /FromModal /MakeMonPredAt /==> <- <-. by rewrite monPred_at_persistently.
 Qed.
-Global Instance from_always_affinely_persistently_monPred_at P Q 𝓠 i :
-  FromAlways always_modality_affinely_persistently P Q → MakeMonPredAt i Q 𝓠 →
-  FromAlways always_modality_affinely_persistently (P i) 𝓠 | 0.
+Global Instance from_modal_affinely_persistently_monPred_at P Q 𝓠 i :
+  FromModal modality_affinely_persistently P Q → MakeMonPredAt i Q 𝓠 →
+  FromModal modality_affinely_persistently (P i) 𝓠 | 0.
 Proof.
-  rewrite /FromAlways /MakeMonPredAt /==> <- <-.
+  rewrite /FromModal /MakeMonPredAt /==> <- <-.
   by rewrite monPred_at_affinely monPred_at_persistently.
 Qed.
 
@@ -348,10 +348,11 @@ Proof.
                          ?monPred_at_persistently monPred_at_embed.
 Qed.
 
+(* FIXME
 Global Instance from_modal_monPred_at i P Q 𝓠 :
   FromModal P Q → MakeMonPredAt i Q 𝓠 → FromModal (P i) 𝓠.
 Proof. by rewrite /FromModal /MakeMonPredAt=> <- <-. Qed.
-
+*)
 End bi.
 
 (* When P and/or Q are evars when doing typeclass search on [IntoWand
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index ddf62b66f41a4e0542b7da30ba658bf89107eb97..31b297db8860b89593e9d002e190bee2fc1275ee 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -961,31 +961,32 @@ Local Tactic Notation "iExistDestruct" constr(H)
     [env_reflexivity || fail "iExistDestruct:" Hx "not fresh"
     |revert y; intros x].
 
-(** * Always *)
-Tactic Notation "iAlways":=
+(** * Modality introduction *)
+Tactic Notation "iModIntro":=
   iStartProof;
-  eapply tac_always_intro;
+  eapply tac_modal_intro;
     [apply _  ||
-     fail "iAlways: the goal is not an always-style modality"
+     fail "iModIntro: the goal is not a modality"
     |hnf; env_cbv;
      apply _ ||
      lazymatch goal with
-     | |- TCAnd (TCForall ?C _) _ => fail "iAlways: persistent context does not satisfy" C
-     | |- TCAnd (TCEq _ Enil) _ => fail "iAlways: persistent context is non-empty"
+     | |- TCAnd (TCForall ?C _) _ => fail "iModIntro: persistent context does not satisfy" C
+     | |- TCAnd (TCEq _ Enil) _ => fail "iModIntro: persistent context is non-empty"
      end
     |hnf; env_cbv;
      lazymatch goal with
      | |- ∃ _, TransformSpatialEnv _ _ _ _ _ ∧ _ =>
         eexists; split;
           [apply _
-          |apply _ || fail "iAlways: cannot filter spatial context when goal is not absorbing"]
+          |apply _ || fail "iModIntro: cannot filter spatial context when goal is not absorbing"]
      | |- TCAnd (TCForall ?C _) _ =>
-        apply _ || fail "iAlways: spatial context does not satisfy" C
+        apply _ || fail "iModIntro: spatial context does not satisfy" C
      | |- TCAnd (TCEq _ Enil) _ =>
-        apply _ || fail "iAlways: spatial context is non-empty"
+        apply _ || fail "iModIntro: spatial context is non-empty"
      | |- _ => apply _
      end
     |env_cbv].
+Tactic Notation "iAlways" := iModIntro.
 
 (** * Later *)
 Tactic Notation "iNext" open_constr(n) :=
@@ -1006,13 +1007,6 @@ Tactic Notation "iNext" open_constr(n) :=
 Tactic Notation "iNext":= iNext _.
 
 (** * Update modality *)
-Tactic Notation "iModIntro" :=
-  iStartProof;
-  eapply tac_modal_intro;
-    [apply _ ||
-     let P := match goal with |- FromModal ?P _ => P end in
-     fail "iModIntro:" P "not a modality"|].
-
 Tactic Notation "iModCore" constr(H) :=
   eapply tac_modal_elim with _ H _ _ _ _ _;
     [env_reflexivity || fail "iMod:" H "not found"