diff --git a/theories/base_logic/base_logic.v b/theories/base_logic/base_logic.v
index 701ff8357f9f8c43d9e446f76024b94a6c0fc15f..58a5a0098d6391f1f112526469741343ba2f8a84 100644
--- a/theories/base_logic/base_logic.v
+++ b/theories/base_logic/base_logic.v
@@ -11,7 +11,7 @@ End uPred.
 Hint Resolve pure_intro.
 Hint Resolve or_elim or_intro_l' or_intro_r' : I.
 Hint Resolve and_intro and_elim_l' and_elim_r' : I.
-Hint Resolve always_mono : I.
+Hint Resolve persistently_mono : I.
 Hint Resolve sep_elim_l' sep_elim_r' sep_mono : I.
 Hint Immediate True_intro False_elim : I.
 Hint Immediate iff_refl internal_eq_refl' : I.
diff --git a/theories/base_logic/big_op.v b/theories/base_logic/big_op.v
index 281daba8019e26a225786455713325f235101242..65b9f23910c06d3ed792194c2ef5bc4432bec6bf 100644
--- a/theories/base_logic/big_op.v
+++ b/theories/base_logic/big_op.v
@@ -117,11 +117,11 @@ Section list.
     ▷^n ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, ▷^n Φ k x).
   Proof. apply (big_opL_commute _). Qed.
 
-  Lemma big_sepL_always Φ l :
+  Lemma big_sepL_persistently Φ l :
     (□ [∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, □ Φ k x).
   Proof. apply (big_opL_commute _). Qed.
 
-  Lemma big_sepL_always_if p Φ l :
+  Lemma big_sepL_persistently_if p Φ l :
     □?p ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, □?p Φ k x).
   Proof. apply (big_opL_commute _). Qed.
 
@@ -134,7 +134,7 @@ Section list.
       apply impl_intro_l, pure_elim_l=> ?; by apply big_sepL_lookup. }
     revert Φ HΦ. induction l as [|x l IH]=> Φ HΦ.
     { rewrite big_sepL_nil; auto with I. }
-    rewrite big_sepL_cons. rewrite -always_and_sep_l; apply and_intro.
+    rewrite big_sepL_cons. rewrite -persistently_and_sep_l; apply and_intro.
     - by rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl.
     - rewrite -IH. apply forall_intro=> k; by rewrite (forall_elim (S k)).
   Qed.
@@ -143,10 +143,10 @@ Section list.
     □ (∀ k x, ⌜l !! k = Some x⌝ → Φ k x → Ψ k x) ∧ ([∗ list] k↦x ∈ l, Φ k x)
     ⊢ [∗ list] k↦x ∈ l, Ψ k x.
   Proof.
-    rewrite always_and_sep_l. do 2 setoid_rewrite always_forall.
-    setoid_rewrite always_impl; setoid_rewrite always_pure.
+    rewrite persistently_and_sep_l. do 2 setoid_rewrite persistently_forall.
+    setoid_rewrite persistently_impl; setoid_rewrite persistently_pure.
     rewrite -big_sepL_forall -big_sepL_sepL. apply big_sepL_mono; auto=> k x ?.
-    by rewrite -always_wand_impl always_elim wand_elim_l.
+    by rewrite -persistently_wand_impl persistently_elim wand_elim_l.
   Qed.
 
   Global Instance big_sepL_nil_persistent Φ :
@@ -307,11 +307,11 @@ Section gmap.
     ▷^n ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, ▷^n Φ k x).
   Proof. apply (big_opM_commute _). Qed.
 
-  Lemma big_sepM_always Φ m :
+  Lemma big_sepM_persistently Φ m :
     (□ [∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, □ Φ k x).
   Proof. apply (big_opM_commute _). Qed.
 
-  Lemma big_sepM_always_if p Φ m :
+  Lemma big_sepM_persistently_if p Φ m :
     □?p ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, □?p Φ k x).
   Proof. apply (big_opM_commute _). Qed.
 
@@ -323,7 +323,7 @@ Section gmap.
     { apply forall_intro=> k; apply forall_intro=> x.
       apply impl_intro_l, pure_elim_l=> ?; by apply big_sepM_lookup. }
     induction m as [|i x m ? IH] using map_ind; [rewrite ?big_sepM_empty; auto|].
-    rewrite big_sepM_insert // -always_and_sep_l. apply and_intro.
+    rewrite big_sepM_insert // -persistently_and_sep_l. apply and_intro.
     - rewrite (forall_elim i) (forall_elim x) lookup_insert.
       by rewrite pure_True // True_impl.
     - rewrite -IH. apply forall_mono=> k; apply forall_mono=> y.
@@ -336,10 +336,10 @@ Section gmap.
     □ (∀ k x, ⌜m !! k = Some x⌝ → Φ k x → Ψ k x) ∧ ([∗ map] k↦x ∈ m, Φ k x)
     ⊢ [∗ map] k↦x ∈ m, Ψ k x.
   Proof.
-    rewrite always_and_sep_l. do 2 setoid_rewrite always_forall.
-    setoid_rewrite always_impl; setoid_rewrite always_pure.
+    rewrite persistently_and_sep_l. do 2 setoid_rewrite persistently_forall.
+    setoid_rewrite persistently_impl; setoid_rewrite persistently_pure.
     rewrite -big_sepM_forall -big_sepM_sepM. apply big_sepM_mono; auto=> k x ?.
-    by rewrite -always_wand_impl always_elim wand_elim_l.
+    by rewrite -persistently_wand_impl persistently_elim wand_elim_l.
   Qed.
 
   Global Instance big_sepM_empty_persistent Φ :
@@ -460,10 +460,10 @@ Section gset.
     ▷^n ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, ▷^n Φ y).
   Proof. apply (big_opS_commute _). Qed.
 
-  Lemma big_sepS_always Φ X : □ ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, □ Φ y).
+  Lemma big_sepS_persistently Φ X : □ ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, □ Φ y).
   Proof. apply (big_opS_commute _). Qed.
 
-  Lemma big_sepS_always_if q Φ X :
+  Lemma big_sepS_persistently_if q Φ X :
     □?q ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, □?q Φ y).
   Proof. apply (big_opS_commute _). Qed.
 
@@ -475,7 +475,7 @@ Section gset.
       apply impl_intro_l, pure_elim_l=> ?; by apply big_sepS_elem_of. }
     induction X as [|x X ? IH] using collection_ind_L.
     { rewrite big_sepS_empty; auto. }
-    rewrite big_sepS_insert // -always_and_sep_l. apply and_intro.
+    rewrite big_sepS_insert // -persistently_and_sep_l. apply and_intro.
     - by rewrite (forall_elim x) pure_True ?True_impl; last set_solver.
     - rewrite -IH. apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
       by rewrite pure_True ?True_impl; last set_solver.
@@ -484,10 +484,10 @@ Section gset.
   Lemma big_sepS_impl Φ Ψ X :
     □ (∀ x, ⌜x ∈ X⌝ → Φ x → Ψ x) ∧ ([∗ set] x ∈ X, Φ x) ⊢ [∗ set] x ∈ X, Ψ x.
   Proof.
-    rewrite always_and_sep_l always_forall.
-    setoid_rewrite always_impl; setoid_rewrite always_pure.
+    rewrite persistently_and_sep_l persistently_forall.
+    setoid_rewrite persistently_impl; setoid_rewrite persistently_pure.
     rewrite -big_sepS_forall -big_sepS_sepS. apply big_sepS_mono; auto=> x ?.
-    by rewrite -always_wand_impl always_elim wand_elim_l.
+    by rewrite -persistently_wand_impl persistently_elim wand_elim_l.
   Qed.
 
   Global Instance big_sepS_empty_persistent Φ : Persistent ([∗ set] x ∈ ∅, Φ x).
@@ -571,10 +571,10 @@ Section gmultiset.
     ▷^n ([∗ mset] y ∈ X, Φ y) ⊣⊢ ([∗ mset] y ∈ X, ▷^n Φ y).
   Proof. apply (big_opMS_commute _). Qed.
 
-  Lemma big_sepMS_always Φ X : □ ([∗ mset] y ∈ X, Φ y) ⊣⊢ ([∗ mset] y ∈ X, □ Φ y).
+  Lemma big_sepMS_persistently Φ X : □ ([∗ mset] y ∈ X, Φ y) ⊣⊢ ([∗ mset] y ∈ X, □ Φ y).
   Proof. apply (big_opMS_commute _). Qed.
 
-  Lemma big_sepMS_always_if q Φ X :
+  Lemma big_sepMS_persistently_if q Φ X :
     □?q ([∗ mset] y ∈ X, Φ y) ⊣⊢ ([∗ mset] y ∈ X, □?q Φ y).
   Proof. apply (big_opMS_commute _). Qed.
 
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index cfca37ec9b2deedce019eb77af761281565c1a0e..1839c214e48496a63cd7c7d79ae4a3cc2eee3246 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -16,11 +16,11 @@ Notation "â–·? p P" := (uPred_laterN (Nat.b2n p) P)
   (at level 20, p at level 9, P at level 20,
    format "â–·? p  P") : uPred_scope.
 
-Definition uPred_always_if {M} (p : bool) (P : uPred M) : uPred M :=
+Definition uPred_persistently_if {M} (p : bool) (P : uPred M) : uPred M :=
   (if p then â–¡ P else P)%I.
-Instance: Params (@uPred_always_if) 2.
-Arguments uPred_always_if _ !_ _/.
-Notation "â–¡? p P" := (uPred_always_if p P)
+Instance: Params (@uPred_persistently_if) 2.
+Arguments uPred_persistently_if _ !_ _/.
+Notation "â–¡? p P" := (uPred_persistently_if p P)
   (at level 20, p at level 9, P at level 20, format "â–¡? p  P").
 
 Definition uPred_except_0 {M} (P : uPred M) : uPred M := ▷ False ∨ P.
@@ -472,105 +472,105 @@ Lemma sep_forall_r {A} (Φ : A → uPred M) Q : (∀ a, Φ a) ∗ Q ⊢ ∀ a, 
 Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
 
 (* Always derived *)
-Hint Resolve always_mono always_elim.
-Global Instance always_mono' : Proper ((⊢) ==> (⊢)) (@uPred_always M).
-Proof. intros P Q; apply always_mono. Qed.
-Global Instance always_flip_mono' :
-  Proper (flip (⊢) ==> flip (⊢)) (@uPred_always M).
-Proof. intros P Q; apply always_mono. Qed.
+Hint Resolve persistently_mono persistently_elim.
+Global Instance persistently_mono' : Proper ((⊢) ==> (⊢)) (@uPred_persistently M).
+Proof. intros P Q; apply persistently_mono. Qed.
+Global Instance persistently_flip_mono' :
+  Proper (flip (⊢) ==> flip (⊢)) (@uPred_persistently M).
+Proof. intros P Q; apply persistently_mono. Qed.
 
-Lemma always_intro' P Q : (□ P ⊢ Q) → □ P ⊢ □ Q.
-Proof. intros <-. apply always_idemp_2. Qed.
-Lemma always_idemp P : □ □ P ⊣⊢ □ P.
-Proof. apply (anti_symm _); auto using always_idemp_2. Qed.
+Lemma persistently_intro' P Q : (□ P ⊢ Q) → □ P ⊢ □ Q.
+Proof. intros <-. apply persistently_idemp_2. Qed.
+Lemma persistently_idemp P : □ □ P ⊣⊢ □ P.
+Proof. apply (anti_symm _); auto using persistently_idemp_2. Qed.
 
-Lemma always_pure φ : □ ⌜φ⌝ ⊣⊢ ⌜φ⌝.
+Lemma persistently_pure φ : □ ⌜φ⌝ ⊣⊢ ⌜φ⌝.
 Proof.
   apply (anti_symm _); auto.
   apply pure_elim'=> Hφ.
   trans (∀ x : False, □ True : uPred M)%I; [by apply forall_intro|].
-  rewrite always_forall_2. auto using always_mono, pure_intro.
+  rewrite persistently_forall_2. auto using persistently_mono, pure_intro.
 Qed.
-Lemma always_forall {A} (Ψ : A → uPred M) : (□ ∀ a, Ψ a) ⊣⊢ (∀ a, □ Ψ a).
+Lemma persistently_forall {A} (Ψ : A → uPred M) : (□ ∀ a, Ψ a) ⊣⊢ (∀ a, □ Ψ a).
 Proof.
-  apply (anti_symm _); auto using always_forall_2.
+  apply (anti_symm _); auto using persistently_forall_2.
   apply forall_intro=> x. by rewrite (forall_elim x).
 Qed.
-Lemma always_exist {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a) ⊣⊢ (∃ a, □ Ψ a).
+Lemma persistently_exist {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a) ⊣⊢ (∃ a, □ Ψ a).
 Proof.
-  apply (anti_symm _); auto using always_exist_1.
+  apply (anti_symm _); auto using persistently_exist_1.
   apply exist_elim=> x. by rewrite (exist_intro x).
 Qed.
-Lemma always_and P Q : □ (P ∧ Q) ⊣⊢ □ P ∧ □ Q.
-Proof. rewrite !and_alt always_forall. by apply forall_proper=> -[]. Qed.
-Lemma always_or P Q : □ (P ∨ Q) ⊣⊢ □ P ∨ □ Q.
-Proof. rewrite !or_alt always_exist. by apply exist_proper=> -[]. Qed.
-Lemma always_impl P Q : □ (P → Q) ⊢ □ P → □ Q.
+Lemma persistently_and P Q : □ (P ∧ Q) ⊣⊢ □ P ∧ □ Q.
+Proof. rewrite !and_alt persistently_forall. by apply forall_proper=> -[]. Qed.
+Lemma persistently_or P Q : □ (P ∨ Q) ⊣⊢ □ P ∨ □ Q.
+Proof. rewrite !or_alt persistently_exist. by apply exist_proper=> -[]. Qed.
+Lemma persistently_impl P Q : □ (P → Q) ⊢ □ P → □ Q.
 Proof.
-  apply impl_intro_l; rewrite -always_and.
-  apply always_mono, impl_elim with P; auto.
+  apply impl_intro_l; rewrite -persistently_and.
+  apply persistently_mono, impl_elim with P; auto.
 Qed.
-Lemma always_internal_eq {A:ofeT} (a b : A) : □ (a ≡ b) ⊣⊢ a ≡ b.
+Lemma persistently_internal_eq {A:ofeT} (a b : A) : □ (a ≡ b) ⊣⊢ a ≡ b.
 Proof.
-  apply (anti_symm (⊢)); auto using always_elim.
+  apply (anti_symm (⊢)); auto using persistently_elim.
   apply (internal_eq_rewrite a b (λ b, □ (a ≡ b))%I); auto.
   { intros n; solve_proper. }
-  rewrite -(internal_eq_refl a) always_pure; auto.
+  rewrite -(internal_eq_refl a) persistently_pure; auto.
 Qed.
 
-Lemma always_and_sep_l' P Q : □ P ∧ Q ⊣⊢ □ P ∗ Q.
-Proof. apply (anti_symm (⊢)); auto using always_and_sep_l_1. Qed.
-Lemma always_and_sep_r' P Q : P ∧ □ Q ⊣⊢ P ∗ □ Q.
-Proof. by rewrite !(comm _ P) always_and_sep_l'. Qed.
-Lemma always_sep_dup' P : □ P ⊣⊢ □ P ∗ □ P.
-Proof. by rewrite -always_and_sep_l' idemp. Qed.
+Lemma persistently_and_sep_l' P Q : □ P ∧ Q ⊣⊢ □ P ∗ Q.
+Proof. apply (anti_symm (⊢)); auto using persistently_and_sep_l_1. Qed.
+Lemma persistently_and_sep_r' P Q : P ∧ □ Q ⊣⊢ P ∗ □ Q.
+Proof. by rewrite !(comm _ P) persistently_and_sep_l'. Qed.
+Lemma persistently_sep_dup' P : □ P ⊣⊢ □ P ∗ □ P.
+Proof. by rewrite -persistently_and_sep_l' idemp. Qed.
 
-Lemma always_and_sep P Q : □ (P ∧ Q) ⊣⊢ □ (P ∗ Q).
+Lemma persistently_and_sep P Q : □ (P ∧ Q) ⊣⊢ □ (P ∗ Q).
 Proof.
   apply (anti_symm (⊢)); auto.
-  rewrite -{1}always_idemp always_and always_and_sep_l'; auto.
+  rewrite -{1}persistently_idemp persistently_and persistently_and_sep_l'; auto.
 Qed.
-Lemma always_sep P Q : □ (P ∗ Q) ⊣⊢ □ P ∗ □ Q.
-Proof. by rewrite -always_and_sep -always_and_sep_l' always_and. Qed.
+Lemma persistently_sep P Q : □ (P ∗ Q) ⊣⊢ □ P ∗ □ Q.
+Proof. by rewrite -persistently_and_sep -persistently_and_sep_l' persistently_and. Qed.
 
-Lemma always_wand P Q : □ (P -∗ Q) ⊢ □ P -∗ □ Q.
-Proof. by apply wand_intro_r; rewrite -always_sep wand_elim_l. Qed.
-Lemma always_wand_impl P Q : □ (P -∗ Q) ⊣⊢ □ (P → Q).
+Lemma persistently_wand P Q : □ (P -∗ Q) ⊢ □ P -∗ □ Q.
+Proof. by apply wand_intro_r; rewrite -persistently_sep wand_elim_l. Qed.
+Lemma persistently_wand_impl P Q : □ (P -∗ Q) ⊣⊢ □ (P → Q).
 Proof.
   apply (anti_symm (⊢)); [|by rewrite -impl_wand].
-  apply always_intro', impl_intro_r.
-  by rewrite always_and_sep_l' always_elim wand_elim_l.
+  apply persistently_intro', impl_intro_r.
+  by rewrite persistently_and_sep_l' persistently_elim wand_elim_l.
 Qed.
-Lemma wand_impl_always P Q : ((□ P) -∗ Q) ⊣⊢ ((□ P) → Q).
+Lemma wand_impl_persistently P Q : ((□ P) -∗ Q) ⊣⊢ ((□ P) → Q).
 Proof.
   apply (anti_symm (⊢)); [|by rewrite -impl_wand].
-  apply impl_intro_l. by rewrite always_and_sep_l' wand_elim_r.
+  apply impl_intro_l. by rewrite persistently_and_sep_l' wand_elim_r.
 Qed.
-Lemma always_entails_l' P Q : (P ⊢ □ Q) → P ⊢ □ Q ∗ P.
-Proof. intros; rewrite -always_and_sep_l'; auto. Qed.
-Lemma always_entails_r' P Q : (P ⊢ □ Q) → P ⊢ P ∗ □ Q.
-Proof. intros; rewrite -always_and_sep_r'; auto. Qed.
+Lemma persistently_entails_l' P Q : (P ⊢ □ Q) → P ⊢ □ Q ∗ P.
+Proof. intros; rewrite -persistently_and_sep_l'; auto. Qed.
+Lemma persistently_entails_r' P Q : (P ⊢ □ Q) → P ⊢ P ∗ □ Q.
+Proof. intros; rewrite -persistently_and_sep_r'; auto. Qed.
 
-Lemma always_laterN n P : □ ▷^n P ⊣⊢ ▷^n □ P.
-Proof. induction n as [|n IH]; simpl; auto. by rewrite always_later IH. Qed.
+Lemma persistently_laterN n P : □ ▷^n P ⊣⊢ ▷^n □ P.
+Proof. induction n as [|n IH]; simpl; auto. by rewrite persistently_later IH. Qed.
 
 Lemma wand_alt P Q : (P -∗ Q) ⊣⊢ ∃ R, R ∗ □ (P ∗ R → Q).
 Proof.
   apply (anti_symm (⊢)).
   - rewrite -(right_id True%I uPred_sep (P -∗ Q)%I) -(exist_intro (P -∗ Q)%I).
-    apply sep_mono_r. rewrite -always_pure. apply always_mono, impl_intro_l.
+    apply sep_mono_r. rewrite -persistently_pure. apply persistently_mono, impl_intro_l.
     by rewrite wand_elim_r right_id.
-  - apply exist_elim=> R. apply wand_intro_l. rewrite assoc -always_and_sep_r'.
-    by rewrite always_elim impl_elim_r.
+  - apply exist_elim=> R. apply wand_intro_l. rewrite assoc -persistently_and_sep_r'.
+    by rewrite persistently_elim impl_elim_r.
 Qed.
 Lemma impl_alt P Q : (P → Q) ⊣⊢ ∃ R, R ∧ □ (P ∧ R -∗ Q).
 Proof.
   apply (anti_symm (⊢)).
   - rewrite -(right_id True%I uPred_and (P → Q)%I) -(exist_intro (P → Q)%I).
-    apply and_mono_r. rewrite -always_pure. apply always_mono, wand_intro_l.
+    apply and_mono_r. rewrite -persistently_pure. apply persistently_mono, wand_intro_l.
     by rewrite impl_elim_r right_id.
-  - apply exist_elim=> R. apply impl_intro_l. rewrite assoc always_and_sep_r'.
-    by rewrite always_elim wand_elim_r.
+  - apply exist_elim=> R. apply impl_intro_l. rewrite assoc persistently_and_sep_r'.
+    by rewrite persistently_elim wand_elim_r.
 Qed.
 
 (* Later derived *)
@@ -671,33 +671,33 @@ Qed.
 Lemma laterN_iff n P Q : ▷^n (P ↔ Q) ⊢ ▷^n P ↔ ▷^n Q.
 Proof. by rewrite /uPred_iff laterN_and !laterN_impl. Qed.
 
-(* Conditional always *)
-Global Instance always_if_ne p : NonExpansive (@uPred_always_if M p).
+(* Conditional persistently *)
+Global Instance persistently_if_ne p : NonExpansive (@uPred_persistently_if M p).
 Proof. solve_proper. Qed.
-Global Instance always_if_proper p : Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_always_if M p).
+Global Instance persistently_if_proper p : Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_persistently_if M p).
 Proof. solve_proper. Qed.
-Global Instance always_if_mono p : Proper ((⊢) ==> (⊢)) (@uPred_always_if M p).
+Global Instance persistently_if_mono p : Proper ((⊢) ==> (⊢)) (@uPred_persistently_if M p).
 Proof. solve_proper. Qed.
 
-Lemma always_if_elim p P : □?p P ⊢ P.
-Proof. destruct p; simpl; auto using always_elim. Qed.
-Lemma always_elim_if p P : □ P ⊢ □?p P.
-Proof. destruct p; simpl; auto using always_elim. Qed.
-
-Lemma always_if_pure p φ : □?p ⌜φ⌝ ⊣⊢ ⌜φ⌝.
-Proof. destruct p; simpl; auto using always_pure. Qed.
-Lemma always_if_and p P Q : □?p (P ∧ Q) ⊣⊢ □?p P ∧ □?p Q.
-Proof. destruct p; simpl; auto using always_and. Qed.
-Lemma always_if_or p P Q : □?p (P ∨ Q) ⊣⊢ □?p P ∨ □?p Q.
-Proof. destruct p; simpl; auto using always_or. Qed.
-Lemma always_if_exist {A} p (Ψ : A → uPred M) : (□?p ∃ a, Ψ a) ⊣⊢ ∃ a, □?p Ψ a.
-Proof. destruct p; simpl; auto using always_exist. Qed.
-Lemma always_if_sep p P Q : □?p (P ∗ Q) ⊣⊢ □?p P ∗ □?p Q.
-Proof. destruct p; simpl; auto using always_sep. Qed.
-Lemma always_if_later p P : □?p ▷ P ⊣⊢ ▷ □?p P.
-Proof. destruct p; simpl; auto using always_later. Qed.
-Lemma always_if_laterN p n P : □?p ▷^n P ⊣⊢ ▷^n □?p P.
-Proof. destruct p; simpl; auto using always_laterN. Qed.
+Lemma persistently_if_elim p P : □?p P ⊢ P.
+Proof. destruct p; simpl; auto using persistently_elim. Qed.
+Lemma persistently_elim_if p P : □ P ⊢ □?p P.
+Proof. destruct p; simpl; auto using persistently_elim. Qed.
+
+Lemma persistently_if_pure p φ : □?p ⌜φ⌝ ⊣⊢ ⌜φ⌝.
+Proof. destruct p; simpl; auto using persistently_pure. Qed.
+Lemma persistently_if_and p P Q : □?p (P ∧ Q) ⊣⊢ □?p P ∧ □?p Q.
+Proof. destruct p; simpl; auto using persistently_and. Qed.
+Lemma persistently_if_or p P Q : □?p (P ∨ Q) ⊣⊢ □?p P ∨ □?p Q.
+Proof. destruct p; simpl; auto using persistently_or. Qed.
+Lemma persistently_if_exist {A} p (Ψ : A → uPred M) : (□?p ∃ a, Ψ a) ⊣⊢ ∃ a, □?p Ψ a.
+Proof. destruct p; simpl; auto using persistently_exist. Qed.
+Lemma persistently_if_sep p P Q : □?p (P ∗ Q) ⊣⊢ □?p P ∗ □?p Q.
+Proof. destruct p; simpl; auto using persistently_sep. Qed.
+Lemma persistently_if_later p P : □?p ▷ P ⊣⊢ ▷ □?p P.
+Proof. destruct p; simpl; auto using persistently_later. Qed.
+Lemma persistently_if_laterN p n P : □?p ▷^n P ⊣⊢ ▷^n □?p P.
+Proof. destruct p; simpl; auto using persistently_laterN. Qed.
 
 (* True now *)
 Global Instance except_0_ne : NonExpansive (@uPred_except_0 M).
@@ -727,7 +727,7 @@ Lemma except_0_sep P Q : ◇ (P ∗ Q) ⊣⊢ ◇ P ∗ ◇ Q.
 Proof.
   rewrite /uPred_except_0. apply (anti_symm _).
   - apply or_elim; last by auto.
-    by rewrite -!or_intro_l -always_pure -always_later -always_sep_dup'.
+    by rewrite -!or_intro_l -persistently_pure -persistently_later -persistently_sep_dup'.
   - rewrite sep_or_r sep_elim_l sep_or_l; auto.
 Qed.
 Lemma except_0_forall {A} (Φ : A → uPred M) : ◇ (∀ a, Φ a) ⊢ ∀ a, ◇ Φ a.
@@ -743,20 +743,20 @@ Proof.
 Qed.
 Lemma except_0_later P : ◇ ▷ P ⊢ ▷ P.
 Proof. by rewrite /uPred_except_0 -later_or False_or. Qed.
-Lemma except_0_always P : ◇ □ P ⊣⊢ □ ◇ P.
-Proof. by rewrite /uPred_except_0 always_or always_later always_pure. Qed.
-Lemma except_0_always_if p P : ◇ □?p P ⊣⊢ □?p ◇ P.
-Proof. destruct p; simpl; auto using except_0_always. Qed.
+Lemma except_0_persistently P : ◇ □ P ⊣⊢ □ ◇ P.
+Proof. by rewrite /uPred_except_0 persistently_or persistently_later persistently_pure. Qed.
+Lemma except_0_persistently_if p P : ◇ □?p P ⊣⊢ □?p ◇ P.
+Proof. destruct p; simpl; auto using except_0_persistently. Qed.
 Lemma except_0_frame_l P Q : P ∗ ◇ Q ⊢ ◇ (P ∗ Q).
 Proof. by rewrite {1}(except_0_intro P) except_0_sep. Qed.
 Lemma except_0_frame_r P Q : ◇ P ∗ Q ⊢ ◇ (P ∗ Q).
 Proof. by rewrite {1}(except_0_intro Q) except_0_sep. Qed.
 
 (* Own and valid derived *)
-Lemma always_ownM (a : M) : CoreId a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
+Lemma persistently_ownM (a : M) : CoreId a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
 Proof.
-  intros; apply (anti_symm _); first by apply:always_elim.
-  by rewrite {1}always_ownM_core core_id_core.
+  intros; apply (anti_symm _); first by apply:persistently_elim.
+  by rewrite {1}persistently_ownM_core core_id_core.
 Qed.
 Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊢ False.
 Proof. by intros; rewrite ownM_valid cmra_valid_elim. Qed.
@@ -764,10 +764,10 @@ Global Instance ownM_mono : Proper (flip (≼) ==> (⊢)) (@uPred_ownM M).
 Proof. intros a b [b' ->]. rewrite ownM_op. eauto. Qed.
 Lemma ownM_unit' : uPred_ownM ε ⊣⊢ True.
 Proof. apply (anti_symm _); first by auto. apply ownM_unit. Qed.
-Lemma always_cmra_valid {A : cmraT} (a : A) : □ ✓ a ⊣⊢ ✓ a.
+Lemma persistently_cmra_valid {A : cmraT} (a : A) : □ ✓ a ⊣⊢ ✓ a.
 Proof.
-  intros; apply (anti_symm _); first by apply:always_elim.
-  apply:always_cmra_valid_1.
+  intros; apply (anti_symm _); first by apply:persistently_elim.
+  apply:persistently_cmra_valid_1.
 Qed.
 
 (** * Derived rules *)
@@ -823,8 +823,8 @@ Proof.
   apply or_mono, wand_intro_l; first done.
   rewrite -{2}(löb Q); apply impl_intro_l.
   rewrite HQ /uPred_except_0 !and_or_r. apply or_elim; last auto.
-  rewrite -(always_pure) -always_later always_and_sep_l'.
-  by rewrite assoc (comm _ _ P) -assoc -always_and_sep_l' impl_elim_r wand_elim_r.
+  rewrite -(persistently_pure) -persistently_later persistently_and_sep_l'.
+  by rewrite assoc (comm _ _ P) -assoc -persistently_and_sep_l' impl_elim_r wand_elim_r.
 Qed.
 Global Instance forall_timeless {A} (Ψ : A → uPred M) :
   (∀ x, Timeless (Ψ x)) → Timeless (∀ x, Ψ x).
@@ -842,9 +842,9 @@ Proof.
   - rewrite /uPred_except_0; auto.
   - apply exist_elim=> x. rewrite -(exist_intro x); auto.
 Qed.
-Global Instance always_timeless P : Timeless P → Timeless (□ P).
-Proof. intros; rewrite /Timeless except_0_always -always_later; auto. Qed.
-Global Instance always_if_timeless p P : Timeless P → Timeless (□?p P).
+Global Instance persistently_timeless P : Timeless P → Timeless (□ P).
+Proof. intros; rewrite /Timeless except_0_persistently -persistently_later; auto. Qed.
+Global Instance persistently_if_timeless p P : Timeless P → Timeless (□?p P).
 Proof. destruct p; apply _. Qed.
 Global Instance eq_timeless {A : ofeT} (a b : A) :
   Discrete a → Timeless (a ≡ b : uPred M)%I.
@@ -867,71 +867,71 @@ Global Instance limit_preserving_Persistent {A:ofeT} `{Cofe A} (Φ : A → uPred
   NonExpansive Φ → LimitPreserving (λ x, Persistent (Φ x)).
 Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
 
-Lemma always_always P `{!Persistent P} : □ P ⊣⊢ P.
-Proof. apply (anti_symm (⊢)); auto using always_elim. Qed.
-Lemma always_if_always p P `{!Persistent P} : □?p P ⊣⊢ P.
-Proof. destruct p; simpl; auto using always_always. Qed.
-Lemma always_intro P Q `{!Persistent P} : (P ⊢ Q) → P ⊢ □ Q.
-Proof. rewrite -(always_always P); apply always_intro'. Qed.
-Lemma always_and_sep_l P Q `{!Persistent P} : P ∧ Q ⊣⊢ P ∗ Q.
-Proof. by rewrite -(always_always P) always_and_sep_l'. Qed.
-Lemma always_and_sep_r P Q `{!Persistent Q} : P ∧ Q ⊣⊢ P ∗ Q.
-Proof. by rewrite -(always_always Q) always_and_sep_r'. Qed.
-Lemma always_sep_dup P `{!Persistent P} : P ⊣⊢ P ∗ P.
-Proof. by rewrite -(always_always P) -always_sep_dup'. Qed.
-Lemma always_entails_l P Q `{!Persistent Q} : (P ⊢ Q) → P ⊢ Q ∗ P.
-Proof. by rewrite -(always_always Q); apply always_entails_l'. Qed.
-Lemma always_entails_r P Q `{!Persistent Q} : (P ⊢ Q) → P ⊢ P ∗ Q.
-Proof. by rewrite -(always_always Q); apply always_entails_r'. Qed.
-Lemma always_impl_wand P `{!Persistent P} Q : (P → Q) ⊣⊢ (P -∗ Q).
+Lemma persistently_persistently P `{!Persistent P} : □ P ⊣⊢ P.
+Proof. apply (anti_symm (⊢)); auto using persistently_elim. Qed.
+Lemma persistently_if_persistently p P `{!Persistent P} : □?p P ⊣⊢ P.
+Proof. destruct p; simpl; auto using persistently_persistently. Qed.
+Lemma persistently_intro P Q `{!Persistent P} : (P ⊢ Q) → P ⊢ □ Q.
+Proof. rewrite -(persistently_persistently P); apply persistently_intro'. Qed.
+Lemma persistently_and_sep_l P Q `{!Persistent P} : P ∧ Q ⊣⊢ P ∗ Q.
+Proof. by rewrite -(persistently_persistently P) persistently_and_sep_l'. Qed.
+Lemma persistently_and_sep_r P Q `{!Persistent Q} : P ∧ Q ⊣⊢ P ∗ Q.
+Proof. by rewrite -(persistently_persistently Q) persistently_and_sep_r'. Qed.
+Lemma persistently_sep_dup P `{!Persistent P} : P ⊣⊢ P ∗ P.
+Proof. by rewrite -(persistently_persistently P) -persistently_sep_dup'. Qed.
+Lemma persistently_entails_l P Q `{!Persistent Q} : (P ⊢ Q) → P ⊢ Q ∗ P.
+Proof. by rewrite -(persistently_persistently Q); apply persistently_entails_l'. Qed.
+Lemma persistently_entails_r P Q `{!Persistent Q} : (P ⊢ Q) → P ⊢ P ∗ Q.
+Proof. by rewrite -(persistently_persistently Q); apply persistently_entails_r'. Qed.
+Lemma persistently_impl_wand P `{!Persistent P} Q : (P → Q) ⊣⊢ (P -∗ Q).
 Proof.
   apply (anti_symm _); auto using impl_wand.
-  apply impl_intro_l. by rewrite always_and_sep_l wand_elim_r.
+  apply impl_intro_l. by rewrite persistently_and_sep_l wand_elim_r.
 Qed.
 
 (* Persistence *)
 Global Instance pure_persistent φ : Persistent (⌜φ⌝ : uPred M)%I.
-Proof. by rewrite /Persistent always_pure. Qed.
+Proof. by rewrite /Persistent persistently_pure. Qed.
 Global Instance pure_impl_persistent φ Q :
   Persistent Q → Persistent (⌜φ⌝ → Q)%I.
 Proof.
-  rewrite /Persistent pure_impl_forall always_forall. auto using forall_mono.
+  rewrite /Persistent pure_impl_forall persistently_forall. auto using forall_mono.
 Qed.
 Global Instance pure_wand_persistent φ Q :
   Persistent Q → Persistent (⌜φ⌝ -∗ Q)%I.
 Proof.
-  rewrite /Persistent -always_impl_wand pure_impl_forall always_forall.
+  rewrite /Persistent -persistently_impl_wand pure_impl_forall persistently_forall.
   auto using forall_mono.
 Qed.
-Global Instance always_persistent P : Persistent (â–¡ P).
-Proof. by intros; apply always_intro'. Qed.
+Global Instance persistently_persistent P : Persistent (â–¡ P).
+Proof. by intros; apply persistently_intro'. Qed.
 Global Instance and_persistent P Q :
   Persistent P → Persistent Q → Persistent (P ∧ Q).
-Proof. by intros; rewrite /Persistent always_and; apply and_mono. Qed.
+Proof. by intros; rewrite /Persistent persistently_and; apply and_mono. Qed.
 Global Instance or_persistent P Q :
   Persistent P → Persistent Q → Persistent (P ∨ Q).
-Proof. by intros; rewrite /Persistent always_or; apply or_mono. Qed.
+Proof. by intros; rewrite /Persistent persistently_or; apply or_mono. Qed.
 Global Instance sep_persistent P Q :
   Persistent P → Persistent Q → Persistent (P ∗ Q).
-Proof. by intros; rewrite /Persistent always_sep; apply sep_mono. Qed.
+Proof. by intros; rewrite /Persistent persistently_sep; apply sep_mono. Qed.
 Global Instance forall_persistent {A} (Ψ : A → uPred M) :
   (∀ x, Persistent (Ψ x)) → Persistent (∀ x, Ψ x).
-Proof. by intros; rewrite /Persistent always_forall; apply forall_mono. Qed.
+Proof. by intros; rewrite /Persistent persistently_forall; apply forall_mono. Qed.
 Global Instance exist_persistent {A} (Ψ : A → uPred M) :
   (∀ x, Persistent (Ψ x)) → Persistent (∃ x, Ψ x).
-Proof. by intros; rewrite /Persistent always_exist; apply exist_mono. Qed.
+Proof. by intros; rewrite /Persistent persistently_exist; apply exist_mono. Qed.
 Global Instance internal_eq_persistent {A : ofeT} (a b : A) :
   Persistent (a ≡ b : uPred M)%I.
-Proof. by intros; rewrite /Persistent always_internal_eq. Qed.
+Proof. by intros; rewrite /Persistent persistently_internal_eq. Qed.
 Global Instance cmra_valid_persistent {A : cmraT} (a : A) :
   Persistent (✓ a : uPred M)%I.
-Proof. by intros; rewrite /Persistent always_cmra_valid. Qed.
+Proof. by intros; rewrite /Persistent persistently_cmra_valid. Qed.
 Global Instance later_persistent P : Persistent P → Persistent (▷ P).
-Proof. by intros; rewrite /Persistent always_later; apply later_mono. Qed.
+Proof. by intros; rewrite /Persistent persistently_later; apply later_mono. Qed.
 Global Instance laterN_persistent n P : Persistent P → Persistent (▷^n P).
 Proof. induction n; apply _. Qed.
 Global Instance ownM_persistent : CoreId a → Persistent (@uPred_ownM M a).
-Proof. intros. by rewrite /Persistent always_ownM. Qed.
+Proof. intros. by rewrite /Persistent persistently_ownM. Qed.
 Global Instance from_option_persistent {A} P (Ψ : A → uPred M) (mx : option A) :
   (∀ x, Persistent (Ψ x)) → Persistent P → Persistent (from_option Ψ P mx).
 Proof. destruct mx; apply _. Qed.
@@ -944,12 +944,12 @@ Global Instance uPred_or_monoid : Monoid (@uPred_or M) :=
 Global Instance uPred_sep_monoid : Monoid (@uPred_sep M) :=
   {| monoid_unit := True%I |}.
 
-Global Instance uPred_always_and_homomorphism :
-  MonoidHomomorphism uPred_and uPred_and (≡) (@uPred_always M).
-Proof. split; [split; try apply _|]. apply always_and. apply always_pure. Qed.
-Global Instance uPred_always_if_and_homomorphism b :
-  MonoidHomomorphism uPred_and uPred_and (≡) (@uPred_always_if M b).
-Proof. split; [split; try apply _|]. apply always_if_and. apply always_if_pure. Qed.
+Global Instance uPred_persistently_and_homomorphism :
+  MonoidHomomorphism uPred_and uPred_and (≡) (@uPred_persistently M).
+Proof. split; [split; try apply _|]. apply persistently_and. apply persistently_pure. Qed.
+Global Instance uPred_persistently_if_and_homomorphism b :
+  MonoidHomomorphism uPred_and uPred_and (≡) (@uPred_persistently_if M b).
+Proof. split; [split; try apply _|]. apply persistently_if_and. apply persistently_if_pure. Qed.
 Global Instance uPred_later_monoid_and_homomorphism :
   MonoidHomomorphism uPred_and uPred_and (≡) (@uPred_later M).
 Proof. split; [split; try apply _|]. apply later_and. apply later_True. Qed.
@@ -960,12 +960,12 @@ Global Instance uPred_except_0_and_homomorphism :
   MonoidHomomorphism uPred_and uPred_and (≡) (@uPred_except_0 M).
 Proof. split; [split; try apply _|]. apply except_0_and. apply except_0_True. Qed.
 
-Global Instance uPred_always_or_homomorphism :
-  MonoidHomomorphism uPred_or uPred_or (≡) (@uPred_always M).
-Proof. split; [split; try apply _|]. apply always_or. apply always_pure. Qed.
-Global Instance uPred_always_if_or_homomorphism b :
-  MonoidHomomorphism uPred_or uPred_or (≡) (@uPred_always_if M b).
-Proof. split; [split; try apply _|]. apply always_if_or. apply always_if_pure. Qed.
+Global Instance uPred_persistently_or_homomorphism :
+  MonoidHomomorphism uPred_or uPred_or (≡) (@uPred_persistently M).
+Proof. split; [split; try apply _|]. apply persistently_or. apply persistently_pure. Qed.
+Global Instance uPred_persistently_if_or_homomorphism b :
+  MonoidHomomorphism uPred_or uPred_or (≡) (@uPred_persistently_if M b).
+Proof. split; [split; try apply _|]. apply persistently_if_or. apply persistently_if_pure. Qed.
 Global Instance uPred_later_monoid_or_homomorphism :
   WeakMonoidHomomorphism uPred_or uPred_or (≡) (@uPred_later M).
 Proof. split; try apply _. apply later_or. Qed.
@@ -976,12 +976,12 @@ Global Instance uPred_except_0_or_homomorphism :
   WeakMonoidHomomorphism uPred_or uPred_or (≡) (@uPred_except_0 M).
 Proof. split; try apply _. apply except_0_or. Qed. 
 
-Global Instance uPred_always_sep_homomorphism :
-  MonoidHomomorphism uPred_sep uPred_sep (≡) (@uPred_always M).
-Proof. split; [split; try apply _|]. apply always_sep. apply always_pure. Qed.
-Global Instance uPred_always_if_sep_homomorphism b :
-  MonoidHomomorphism uPred_sep uPred_sep (≡) (@uPred_always_if M b).
-Proof. split; [split; try apply _|]. apply always_if_sep. apply always_if_pure. Qed.
+Global Instance uPred_persistently_sep_homomorphism :
+  MonoidHomomorphism uPred_sep uPred_sep (≡) (@uPred_persistently M).
+Proof. split; [split; try apply _|]. apply persistently_sep. apply persistently_pure. Qed.
+Global Instance uPred_persistently_if_sep_homomorphism b :
+  MonoidHomomorphism uPred_sep uPred_sep (≡) (@uPred_persistently_if M b).
+Proof. split; [split; try apply _|]. apply persistently_if_sep. apply persistently_if_pure. Qed.
 Global Instance uPred_later_monoid_sep_homomorphism :
   MonoidHomomorphism uPred_sep uPred_sep (≡) (@uPred_later M).
 Proof. split; [split; try apply _|]. apply later_sep. apply later_True. Qed.
diff --git a/theories/base_logic/lib/fractional.v b/theories/base_logic/lib/fractional.v
index 25956794de7388f946352e96b32d970e5db229e2..c1c2b0d97220a5749d134484c69665ad66df4f72 100644
--- a/theories/base_logic/lib/fractional.v
+++ b/theories/base_logic/lib/fractional.v
@@ -51,7 +51,7 @@ Section fractional.
   (** Fractional and logical connectives *)
   Global Instance persistent_fractional P :
     Persistent P → Fractional (λ _, P).
-  Proof. intros HP q q'. by apply uPred.always_sep_dup. Qed.
+  Proof. intros HP q q'. by apply uPred.persistently_sep_dup. Qed.
 
   Global Instance fractional_sep Φ Ψ :
     Fractional Φ → Fractional Ψ → Fractional (λ q, Φ q ∗ Ψ q)%I.
@@ -134,7 +134,7 @@ Section fractional.
     AsFractional P Φ (q1 + q2) → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
     IntoAnd p P P1 P2.
   Proof.
-    (* TODO: We need a better way to handle this boolean here; always
+    (* TODO: We need a better way to handle this boolean here; persistently
        applying mk_into_and_sep (which only works after introducing all
        assumptions) is rather annoying.
        Ideally, it'd not even be possible to make the mistake that
@@ -148,7 +148,7 @@ Section fractional.
   Proof. intros. apply mk_into_and_sep. rewrite [P]fractional_half //. Qed.
 
   (* The instance [frame_fractional] can be tried at all the nodes of
-     the proof search. The proof search then fails almost always on
+     the proof search. The proof search then fails almost persistently on
      [AsFractional R Φ r], but the slowdown is still noticeable.  For
      that reason, we factorize the three instances that could have been
      defined for that purpose into one. *)
@@ -179,6 +179,6 @@ Section fractional.
     - rewrite fractional=><-<-. by rewrite assoc.
     - rewrite fractional=><-<-=>_.
       by rewrite (comm _ Q (Φ q0)) !assoc (comm _ (Φ _)).
-    - move=>-[-> _]->. by rewrite uPred.always_if_elim -fractional Qp_div_2.
+    - move=>-[-> _]->. by rewrite uPred.persistently_if_elim -fractional Qp_div_2.
   Qed.
 End fractional.
diff --git a/theories/base_logic/lib/iprop.v b/theories/base_logic/lib/iprop.v
index 95a378c30aa8827ddcf550230875418735cb816d..b0462acf5e89fbc7a224c260f94be3770b7dc2ae 100644
--- a/theories/base_logic/lib/iprop.v
+++ b/theories/base_logic/lib/iprop.v
@@ -83,7 +83,7 @@ Class subG (Σ1 Σ2 : gFunctors) := in_subG i : { j | Σ1 i = Σ2 j }.
 
 (** Avoid trigger happy type class search: this line ensures that type class
 search is only triggered if the arguments of [subG] do not contain evars. Since
-instance search for [subG] is restrained, instances should always have [subG] as
+instance search for [subG] is restrained, instances should persistently have [subG] as
 their first parameter to avoid loops. For example, the instances [subG_authΣ]
 and [auth_discrete] otherwise create a cycle that pops up arbitrarily. *)
 Hint Mode subG + + : typeclass_instances.
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index 89bbf7833747f3e1cb595c76a5897560a9ae5f40..d3d71f8d9573fc48128a4b5c228f000699b11385 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -102,7 +102,7 @@ Proof. apply wand_intro_r. by rewrite -own_op own_valid. Qed.
 Lemma own_valid_3 γ a1 a2 a3 : own γ a1 -∗ own γ a2 -∗ own γ a3 -∗ ✓ (a1 ⋅ a2 ⋅ a3).
 Proof. do 2 apply wand_intro_r. by rewrite -!own_op own_valid. Qed.
 Lemma own_valid_r γ a : own γ a ⊢ own γ a ∗ ✓ a.
-Proof. apply: uPred.always_entails_r. apply own_valid. Qed.
+Proof. apply: uPred.persistently_entails_r. apply own_valid. Qed.
 Lemma own_valid_l γ a : own γ a ⊢ ✓ a ∗ own γ a.
 Proof. by rewrite comm -own_valid_r. Qed.
 
diff --git a/theories/base_logic/lib/viewshifts.v b/theories/base_logic/lib/viewshifts.v
index 490ce88166aae344696c038a060de0c92aa9c9e3..cdefcc3f3d34958d9dc35da89ab76655081451b2 100644
--- a/theories/base_logic/lib/viewshifts.v
+++ b/theories/base_logic/lib/viewshifts.v
@@ -81,5 +81,5 @@ Lemma vs_alloc N P : ▷ P ={↑N}=> inv N P.
 Proof. iIntros "!# HP". by iApply inv_alloc. Qed.
 
 Lemma wand_fupd_alt E1 E2 P Q : (P ={E1,E2}=∗ Q) ⊣⊢ ∃ R, R ∗ (P ∗ R ={E1,E2}=> Q).
-Proof. rewrite uPred.wand_alt. by setoid_rewrite <-uPred.always_wand_impl. Qed.
+Proof. rewrite uPred.wand_alt. by setoid_rewrite <-uPred.persistently_wand_impl. Qed.
 End vs.
diff --git a/theories/base_logic/primitive.v b/theories/base_logic/primitive.v
index 4a6159998d90515a39563e82930ad9ff9ae712d7..18d99c2017d88460b7af241a8ab1fea3856054ed 100644
--- a/theories/base_logic/primitive.v
+++ b/theories/base_logic/primitive.v
@@ -97,16 +97,16 @@ Definition uPred_wand {M} := unseal uPred_wand_aux M.
 Definition uPred_wand_eq :
   @uPred_wand = @uPred_wand_def := seal_eq uPred_wand_aux.
 
-Program Definition uPred_always_def {M} (P : uPred M) : uPred M :=
+Program Definition uPred_persistently_def {M} (P : uPred M) : uPred M :=
   {| uPred_holds n x := P n (core x) |}.
 Next Obligation.
   intros M; naive_solver eauto using uPred_mono, @cmra_core_monoN.
 Qed.
 Next Obligation. naive_solver eauto using uPred_closed, @cmra_core_validN. Qed.
-Definition uPred_always_aux : seal (@uPred_always_def). by eexists. Qed.
-Definition uPred_always {M} := unseal uPred_always_aux M.
-Definition uPred_always_eq :
-  @uPred_always = @uPred_always_def := seal_eq uPred_always_aux.
+Definition uPred_persistently_aux : seal (@uPred_persistently_def). by eexists. Qed.
+Definition uPred_persistently {M} := unseal uPred_persistently_aux M.
+Definition uPred_persistently_eq :
+  @uPred_persistently = @uPred_persistently_def := seal_eq uPred_persistently_aux.
 
 Program Definition uPred_later_def {M} (P : uPred M) : uPred M :=
   {| uPred_holds n x := match n return _ with 0 => True | S n' => P n' x end |}.
@@ -176,7 +176,7 @@ Notation "∀ x .. y , P" :=
 Notation "∃ x .. y , P" :=
   (uPred_exist (λ x, .. (uPred_exist (λ y, P)) ..)%I)
   (at level 200, x binder, y binder, right associativity) : uPred_scope.
-Notation "â–¡ P" := (uPred_always P)
+Notation "â–¡ P" := (uPred_persistently P)
   (at level 20, right associativity) : uPred_scope.
 Notation "â–· P" := (uPred_later P)
   (at level 20, right associativity) : uPred_scope.
@@ -198,7 +198,7 @@ Notation "P -∗ Q" := (P ⊢ Q)
 Module uPred.
 Definition unseal_eqs :=
   (uPred_pure_eq, uPred_and_eq, uPred_or_eq, uPred_impl_eq, uPred_forall_eq,
-  uPred_exist_eq, uPred_internal_eq_eq, uPred_sep_eq, uPred_wand_eq, uPred_always_eq,
+  uPred_exist_eq, uPred_internal_eq_eq, uPred_sep_eq, uPred_wand_eq, uPred_persistently_eq,
   uPred_later_eq, uPred_ownM_eq, uPred_cmra_valid_eq, uPred_bupd_eq).
 Ltac unseal := rewrite !unseal_eqs /=.
 
@@ -295,13 +295,13 @@ Proof.
 Qed.
 Global Instance later_proper' :
   Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_later M) := ne_proper _.
-Global Instance always_ne : NonExpansive (@uPred_always M).
+Global Instance persistently_ne : NonExpansive (@uPred_persistently M).
 Proof.
   intros n P1 P2 HP.
   unseal; split=> n' x; split; apply HP; eauto using @cmra_core_validN.
 Qed.
-Global Instance always_proper :
-  Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_always M) := ne_proper _.
+Global Instance persistently_proper :
+  Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_persistently M) := ne_proper _.
 Global Instance ownM_ne : NonExpansive (@uPred_ownM M).
 Proof.
   intros n a b Ha.
@@ -422,22 +422,22 @@ Proof.
 Qed.
 
 (* Always *)
-Lemma always_mono P Q : (P ⊢ Q) → □ P ⊢ □ Q.
+Lemma persistently_mono P Q : (P ⊢ Q) → □ P ⊢ □ Q.
 Proof. intros HP; unseal; split=> n x ? /=. by apply HP, cmra_core_validN. Qed.
-Lemma always_elim P : □ P ⊢ P.
+Lemma persistently_elim P : □ P ⊢ P.
 Proof.
   unseal; split=> n x ? /=.
   eauto using uPred_mono, @cmra_included_core, cmra_included_includedN.
 Qed.
-Lemma always_idemp_2 P : □ P ⊢ □ □ P.
+Lemma persistently_idemp_2 P : □ P ⊢ □ □ P.
 Proof. unseal; split=> n x ?? /=. by rewrite cmra_core_idemp. Qed.
 
-Lemma always_forall_2 {A} (Ψ : A → uPred M) : (∀ a, □ Ψ a) ⊢ (□ ∀ a, Ψ a).
+Lemma persistently_forall_2 {A} (Ψ : A → uPred M) : (∀ a, □ Ψ a) ⊢ (□ ∀ a, Ψ a).
 Proof. by unseal. Qed.
-Lemma always_exist_1 {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a) ⊢ (∃ a, □ Ψ a).
+Lemma persistently_exist_1 {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a) ⊢ (∃ a, □ Ψ a).
 Proof. by unseal. Qed.
 
-Lemma always_and_sep_l_1 P Q : □ P ∧ Q ⊢ □ P ∗ Q.
+Lemma persistently_and_sep_l_1 P Q : □ P ∧ Q ⊢ □ P ∗ Q.
 Proof.
   unseal; split=> n x ? [??]; exists (core x), x; simpl in *.
   by rewrite cmra_core_l cmra_core_idemp.
@@ -475,7 +475,7 @@ Proof.
   intros [|n'] x' ????; [|done].
   eauto using uPred_closed, uPred_mono, cmra_included_includedN.
 Qed.
-Lemma always_later P : □ ▷ P ⊣⊢ ▷ □ P.
+Lemma persistently_later P : □ ▷ P ⊣⊢ ▷ □ P.
 Proof. by unseal. Qed.
 
 (* Own *)
@@ -489,7 +489,7 @@ Proof.
     by rewrite (assoc op _ z1) -(comm op z1) (assoc op z1)
       -(assoc op _ a2) (comm op z1) -Hy1 -Hy2.
 Qed.
-Lemma always_ownM_core (a : M) : uPred_ownM a ⊢ □ uPred_ownM (core a).
+Lemma persistently_ownM_core (a : M) : uPred_ownM a ⊢ □ uPred_ownM (core a).
 Proof.
   split=> n x /=; unseal; intros Hx. simpl. by apply cmra_core_monoN.
 Qed.
@@ -512,7 +512,7 @@ Lemma cmra_valid_intro {A : cmraT} (a : A) : ✓ a → uPred_valid (M:=M) (✓ a
 Proof. unseal=> ?; split=> n x ? _ /=; by apply cmra_valid_validN. Qed.
 Lemma cmra_valid_elim {A : cmraT} (a : A) : ¬ ✓{0} a → ✓ a ⊢ False.
 Proof. unseal=> Ha; split=> n x ??; apply Ha, cmra_validN_le with n; auto. Qed.
-Lemma always_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ □ ✓ a.
+Lemma persistently_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ □ ✓ a.
 Proof. by unseal. Qed.
 Lemma cmra_valid_weaken {A : cmraT} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
 Proof. unseal; split=> n x _; apply cmra_validN_op_l. Qed.
diff --git a/theories/program_logic/hoare.v b/theories/program_logic/hoare.v
index bb4489e5eca99d6bb84ff329c5078b7e08cd34c6..f465765b473d5b432cc5bc96614bb96f61ff5a48 100644
--- a/theories/program_logic/hoare.v
+++ b/theories/program_logic/hoare.v
@@ -37,7 +37,7 @@ Global Instance ht_proper E :
 Proof. solve_proper. Qed.
 Lemma ht_mono E P P' Φ Φ' e :
   (P ⊢ P') → (∀ v, Φ' v ⊢ Φ v) → {{ P' }} e @ E {{ Φ' }} ⊢ {{ P }} e @ E {{ Φ }}.
-Proof. by intros; apply always_mono, wand_mono, wp_mono. Qed.
+Proof. by intros; apply persistently_mono, wand_mono, wp_mono. Qed.
 Global Instance ht_mono' E :
   Proper (flip (⊢) ==> eq ==> pointwise_relation _ (⊢) ==> (⊢)) (ht E).
 Proof. solve_proper. Qed.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index f51eb6f5d178f6620f12b686d3b1570c6e907370..e548668c04f1e2bbb649ec26228eabc86c801828 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -283,7 +283,7 @@ Section proofmode_classes.
     ElimModal (|={E}=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
   Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_wp. Qed.
 
-  (* lower precedence, if possible, it should always pick elim_upd_fupd_wp *)
+  (* lower precedence, if possible, it should persistently pick elim_upd_fupd_wp *)
   Global Instance elim_modal_fupd_wp_atomic E1 E2 e P Φ :
     atomic e →
     ElimModal (|={E1,E2}=> P) P
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index ba0c288c0695dc07731767e90733c8ac8a0a61a8..e4f814b107b234d583aff308fc258884f3c5f378 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -11,17 +11,17 @@ Implicit Types P Q R : uPred M.
 
 (* FromAssumption *)
 Global Instance from_assumption_exact p P : FromAssumption p P P | 0.
-Proof. destruct p; by rewrite /FromAssumption /= ?always_elim. Qed.
+Proof. destruct p; by rewrite /FromAssumption /= ?persistently_elim. Qed.
 Global Instance from_assumption_False p P : FromAssumption p False P | 1.
-Proof. destruct p; rewrite /FromAssumption /= ?always_pure; apply False_elim. Qed.
+Proof. destruct p; rewrite /FromAssumption /= ?persistently_pure; apply False_elim. Qed.
 
-Global Instance from_assumption_always_r P Q :
+Global Instance from_assumption_persistently_r P Q :
   FromAssumption true P Q → FromAssumption true P (□ Q).
-Proof. rewrite /FromAssumption=><-. by rewrite always_always. Qed.
+Proof. rewrite /FromAssumption=><-. by rewrite persistently_persistently. Qed.
 
-Global Instance from_assumption_always_l p P Q :
+Global Instance from_assumption_persistently_l p P Q :
   FromAssumption p P Q → FromAssumption p (□ P) Q.
-Proof. rewrite /FromAssumption=><-. by rewrite always_elim. Qed.
+Proof. rewrite /FromAssumption=><-. by rewrite persistently_elim. Qed.
 Global Instance from_assumption_later p P Q :
   FromAssumption p P Q → FromAssumption p P (▷ Q)%I.
 Proof. rewrite /FromAssumption=>->. apply later_intro. Qed.
@@ -48,8 +48,8 @@ Global Instance into_pure_cmra_valid `{CmraDiscrete A} (a : A) :
   @IntoPure M (✓ a) (✓ a).
 Proof. by rewrite /IntoPure discrete_valid. Qed.
 
-Global Instance into_pure_always P φ : IntoPure P φ → IntoPure (□ P) φ.
-Proof. rewrite /IntoPure=> ->. by rewrite always_pure. Qed.
+Global Instance into_pure_persistently P φ : IntoPure P φ → IntoPure (□ P) φ.
+Proof. rewrite /IntoPure=> ->. by rewrite persistently_pure. Qed.
 
 Global Instance into_pure_pure_and (φ1 φ2 : Prop) P1 P2 :
   IntoPure P1 φ1 → IntoPure P2 φ2 → IntoPure (P1 ∧ P2) (φ1 ∧ φ2).
@@ -66,7 +66,7 @@ Proof. rewrite /FromPure /IntoPure pure_impl. by intros -> ->. Qed.
 Global Instance into_pure_pure_wand (φ1 φ2 : Prop) P1 P2 :
   FromPure P1 φ1 → IntoPure P2 φ2 → IntoPure (P1 -∗ P2) (φ1 → φ2).
 Proof.
-  rewrite /FromPure /IntoPure pure_impl always_impl_wand. by intros -> ->.
+  rewrite /FromPure /IntoPure pure_impl persistently_impl_wand. by intros -> ->.
 Qed.
 
 Global Instance into_pure_exist {X : Type} (Φ : X → uPred M) (φ : X → Prop) :
@@ -97,8 +97,8 @@ Proof.
   rewrite -cmra_valid_intro //. auto with I.
 Qed.
 
-Global Instance from_pure_always P φ : FromPure P φ → FromPure (□ P) φ.
-Proof. rewrite /FromPure=> <-. by rewrite always_pure. Qed.
+Global Instance from_pure_persistently P φ : FromPure P φ → FromPure (□ P) φ.
+Proof. rewrite /FromPure=> <-. by rewrite persistently_pure. Qed.
 Global Instance from_pure_later P φ : FromPure P φ → FromPure (▷ P) φ.
 Proof. rewrite /FromPure=> ->. apply later_intro. Qed.
 Global Instance from_pure_laterN n P φ : FromPure P φ → FromPure (▷^n P) φ.
@@ -113,7 +113,7 @@ Global Instance from_pure_pure_and (φ1 φ2 : Prop) P1 P2 :
 Proof. rewrite /FromPure pure_and. by intros -> ->. Qed.
 Global Instance from_pure_pure_sep (φ1 φ2 : Prop) P1 P2 :
   FromPure P1 φ1 → FromPure P2 φ2 → FromPure (P1 ∗ P2) (φ1 ∧ φ2).
-Proof. rewrite /FromPure pure_and always_and_sep_l. by intros -> ->. Qed.
+Proof. rewrite /FromPure pure_and persistently_and_sep_l. by intros -> ->. Qed.
 Global Instance from_pure_pure_or (φ1 φ2 : Prop) P1 P2 :
   FromPure P1 φ1 → FromPure P2 φ2 → FromPure (P1 ∨ P2) (φ1 ∨ φ2).
 Proof. rewrite /FromPure pure_or. by intros -> ->. Qed.
@@ -123,7 +123,7 @@ Proof. rewrite /FromPure /IntoPure pure_impl. by intros -> ->. Qed.
 Global Instance from_pure_pure_wand (φ1 φ2 : Prop) P1 P2 :
   IntoPure P1 φ1 → FromPure P2 φ2 → FromPure (P1 -∗ P2) (φ1 → φ2).
 Proof.
-  rewrite /FromPure /IntoPure pure_impl always_impl_wand. by intros -> ->.
+  rewrite /FromPure /IntoPure pure_impl persistently_impl_wand. by intros -> ->.
 Qed.
 
 Global Instance from_pure_exist {X : Type} (Φ : X → uPred M) (φ : X → Prop) :
@@ -140,10 +140,10 @@ Proof.
 Qed.
 
 (* IntoPersistent *)
-Global Instance into_persistent_always_trans p P Q :
+Global Instance into_persistent_persistently_trans p P Q :
   IntoPersistent true P Q → IntoPersistent p (□ P) Q | 0.
-Proof. rewrite /IntoPersistent /==> ->. by rewrite always_if_always. Qed.
-Global Instance into_persistent_always P : IntoPersistent true P P | 1.
+Proof. rewrite /IntoPersistent /==> ->. by rewrite persistently_if_persistently. Qed.
+Global Instance into_persistent_persistently P : IntoPersistent true P P | 1.
 Proof. done. Qed.
 Global Instance into_persistent_persistent P :
   Persistent P → IntoPersistent false P P | 100.
@@ -258,9 +258,9 @@ Global Instance from_later_sep n P1 P2 Q1 Q2 :
   FromLaterN n P1 Q1 → FromLaterN n P2 Q2 → FromLaterN n (P1 ∗ P2) (Q1 ∗ Q2).
 Proof. intros ??; red. by rewrite laterN_sep; apply sep_mono. Qed.
 
-Global Instance from_later_always n P Q :
+Global Instance from_later_persistently n P Q :
   FromLaterN n P Q → FromLaterN n (□ P) (□ Q).
-Proof. by rewrite /FromLaterN -always_laterN=> ->. Qed.
+Proof. by rewrite /FromLaterN -persistently_laterN=> ->. Qed.
 
 Global Instance from_later_forall {A} n (Φ Ψ : A → uPred M) :
   (∀ x, FromLaterN n (Φ x) (Ψ x)) → FromLaterN n (∀ x, Φ x) (∀ x, Ψ x).
@@ -278,19 +278,19 @@ Global Instance wand_weaken_later p P Q P' Q' :
   WandWeaken p P Q P' Q' → WandWeaken' p P Q (▷ P') (▷ Q').
 Proof.
   rewrite /WandWeaken' /WandWeaken=> ->.
-  by rewrite always_if_later -later_wand -later_intro.
+  by rewrite persistently_if_later -later_wand -later_intro.
 Qed.
 Global Instance wand_weaken_laterN p n P Q P' Q' :
   WandWeaken p P Q P' Q' → WandWeaken' p P Q (▷^n P') (▷^n Q').
 Proof.
   rewrite /WandWeaken' /WandWeaken=> ->.
-  by rewrite always_if_laterN -laterN_wand -laterN_intro.
+  by rewrite persistently_if_laterN -laterN_wand -laterN_intro.
 Qed.
 Global Instance bupd_weaken_laterN p P Q P' Q' :
   WandWeaken false P Q P' Q' → WandWeaken' p P Q (|==> P') (|==> Q').
 Proof.
   rewrite /WandWeaken' /WandWeaken=> ->.
-  apply wand_intro_l. by rewrite always_if_elim bupd_wand_r.
+  apply wand_intro_l. by rewrite persistently_if_elim bupd_wand_r.
 Qed.
 
 Global Instance into_wand_wand p P P' Q Q' :
@@ -310,16 +310,16 @@ Proof. rewrite /WandWeaken /IntoWand=> <-. apply and_elim_r', impl_wand. Qed.
 Global Instance into_wand_forall {A} p (Φ : A → uPred M) P Q x :
   IntoWand p (Φ x) P Q → IntoWand p (∀ x, Φ x) P Q.
 Proof. rewrite /IntoWand=> <-. apply forall_elim. Qed.
-Global Instance into_wand_always p R P Q :
+Global Instance into_wand_persistently p R P Q :
   IntoWand p R P Q → IntoWand p (□ R) P Q.
-Proof. rewrite /IntoWand=> ->. apply always_elim. Qed.
+Proof. rewrite /IntoWand=> ->. apply persistently_elim. Qed.
 
 Global Instance into_wand_later p R P Q :
   IntoWand p R P Q → IntoWand p (▷ R) (▷ P) (▷ Q).
-Proof. rewrite /IntoWand=> ->. by rewrite always_if_later -later_wand. Qed.
+Proof. rewrite /IntoWand=> ->. by rewrite persistently_if_later -later_wand. Qed.
 Global Instance into_wand_laterN p n R P Q :
   IntoWand p R P Q → IntoWand p (▷^n R) (▷^n P) (▷^n Q).
-Proof. rewrite /IntoWand=> ->. by rewrite always_if_laterN -laterN_wand. Qed.
+Proof. rewrite /IntoWand=> ->. by rewrite persistently_if_laterN -laterN_wand. Qed.
 
 Global Instance into_wand_bupd R P Q :
   IntoWand false R P Q → IntoWand false (|==> R) (|==> P) (|==> Q).
@@ -340,18 +340,18 @@ Global Instance from_and_sep P1 P2 : FromAnd false (P1 ∗ P2) P1 P2 | 100.
 Proof. done. Qed.
 Global Instance from_and_sep_persistent_l P1 P2 :
   Persistent P1 → FromAnd true (P1 ∗ P2) P1 P2 | 9.
-Proof. intros. by rewrite /FromAnd always_and_sep_l. Qed.
+Proof. intros. by rewrite /FromAnd persistently_and_sep_l. Qed.
 Global Instance from_and_sep_persistent_r P1 P2 :
   Persistent P2 → FromAnd true (P1 ∗ P2) P1 P2 | 10.
-Proof. intros. by rewrite /FromAnd always_and_sep_r. Qed.
+Proof. intros. by rewrite /FromAnd persistently_and_sep_r. Qed.
 
 Global Instance from_and_pure p φ ψ : @FromAnd M p ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
 Proof. apply mk_from_and_and. by rewrite pure_and. Qed.
-Global Instance from_and_always p P Q1 Q2 :
+Global Instance from_and_persistently p P Q1 Q2 :
   FromAnd false P Q1 Q2 → FromAnd p (□ P) (□ Q1) (□ Q2).
 Proof.
   intros. apply mk_from_and_and.
-  by rewrite always_and_sep_l' -always_sep -(from_and _ P).
+  by rewrite persistently_and_sep_l' -persistently_sep -(from_and _ P).
 Qed.
 Global Instance from_and_later p P Q1 Q2 :
   FromAnd p P Q1 Q2 → FromAnd p (▷ P) (▷ Q1) (▷ Q2).
@@ -387,7 +387,7 @@ Proof. by rewrite /FromAnd big_sepL_cons. Qed.
 Global Instance from_and_big_sepL_cons_persistent {A} (Φ : nat → A → uPred M) x l :
   Persistent (Φ 0 x) →
   FromAnd true ([∗ list] k ↦ y ∈ x :: l, Φ k y) (Φ 0 x) ([∗ list] k ↦ y ∈ l, Φ (S k) y).
-Proof. intros. by rewrite /FromAnd big_opL_cons always_and_sep_l. Qed.
+Proof. intros. by rewrite /FromAnd big_opL_cons persistently_and_sep_l. Qed.
 
 Global Instance from_and_big_sepL_app {A} (Φ : nat → A → uPred M) l1 l2 :
   FromAnd false ([∗ list] k ↦ y ∈ l1 ++ l2, Φ k y)
@@ -397,7 +397,7 @@ Global Instance from_sep_big_sepL_app_persistent {A} (Φ : nat → A → uPred M
   (∀ k y, Persistent (Φ k y)) →
   FromAnd true ([∗ list] k ↦ y ∈ l1 ++ l2, Φ k y)
     ([∗ list] k ↦ y ∈ l1, Φ k y) ([∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y).
-Proof. intros. by rewrite /FromAnd big_opL_app always_and_sep_l. Qed.
+Proof. intros. by rewrite /FromAnd big_opL_app persistently_and_sep_l. Qed.
 
 (* FromOp *)
 (* TODO: Worst case there could be a lot of backtracking on these instances,
@@ -431,17 +431,17 @@ Global Instance into_and_and P Q : IntoAnd true (P ∧ Q) P Q.
 Proof. done. Qed.
 Global Instance into_and_and_persistent_l P Q :
   Persistent P → IntoAnd false (P ∧ Q) P Q.
-Proof. intros; by rewrite /IntoAnd /= always_and_sep_l. Qed.
+Proof. intros; by rewrite /IntoAnd /= persistently_and_sep_l. Qed.
 Global Instance into_and_and_persistent_r P Q :
   Persistent Q → IntoAnd false (P ∧ Q) P Q.
-Proof. intros; by rewrite /IntoAnd /= always_and_sep_r. Qed.
+Proof. intros; by rewrite /IntoAnd /= persistently_and_sep_r. Qed.
 
 Global Instance into_and_pure p φ ψ : @IntoAnd M p ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
-Proof. apply mk_into_and_sep. by rewrite pure_and always_and_sep_r. Qed.
-Global Instance into_and_always p P Q1 Q2 :
+Proof. apply mk_into_and_sep. by rewrite pure_and persistently_and_sep_r. Qed.
+Global Instance into_and_persistently p P Q1 Q2 :
   IntoAnd true P Q1 Q2 → IntoAnd p (□ P) (□ Q1) (□ Q2).
 Proof.
-  rewrite /IntoAnd=>->. destruct p; by rewrite ?always_and always_and_sep_r.
+  rewrite /IntoAnd=>->. destruct p; by rewrite ?persistently_and persistently_and_sep_r.
 Qed.
 Global Instance into_and_later p P Q1 Q2 :
   IntoAnd p P Q1 Q2 → IntoAnd p (▷ P) (▷ Q1) (▷ Q2).
@@ -471,9 +471,9 @@ Proof. rewrite /IsApp=>->. apply mk_into_and_sep. by rewrite big_sepL_app. Qed.
 
 (* Frame *)
 Global Instance frame_here p R : Frame p R R True.
-Proof. by rewrite /Frame right_id always_if_elim. Qed.
+Proof. by rewrite /Frame right_id persistently_if_elim. Qed.
 Global Instance frame_here_pure p φ Q : FromPure Q φ → Frame p ⌜φ⌝ Q True.
-Proof. rewrite /FromPure /Frame=> ->. by rewrite always_if_elim right_id. Qed.
+Proof. rewrite /FromPure /Frame=> ->. by rewrite persistently_if_elim right_id. Qed.
 
 Class MakeSep (P Q PQ : uPred M) := make_sep : P ∗ Q ⊣⊢ PQ.
 Global Instance make_sep_true_l P : MakeSep True P P.
@@ -488,7 +488,7 @@ Global Instance frame_sep_persistent_l R P1 P2 Q1 Q2 Q' :
   Frame true R (P1 ∗ P2) Q' | 9.
 Proof.
   rewrite /Frame /MaybeFrame /MakeSep /= => <- <- <-.
-  rewrite {1}(always_sep_dup (â–¡ R)). solve_sep_entails.
+  rewrite {1}(persistently_sep_dup (â–¡ R)). solve_sep_entails.
 Qed.
 Global Instance frame_sep_l R P1 P2 Q Q' :
   Frame false R P1 Q → MakeSep Q P2 Q' → Frame false R (P1 ∗ P2) Q' | 9.
@@ -563,7 +563,7 @@ Global Instance frame_later p R R' P Q Q' :
   IntoLaterN 1 R' R → Frame p R P Q → MakeLater Q Q' → Frame p R' (▷ P) Q'.
 Proof.
   rewrite /Frame /MakeLater /IntoLaterN=>-> <- <-.
-  by rewrite always_if_later later_sep.
+  by rewrite persistently_if_later later_sep.
 Qed.
 
 Class MakeLaterN (n : nat) (P lP : uPred M) := make_laterN : ▷^n P ⊣⊢ lP.
@@ -576,20 +576,20 @@ Global Instance frame_laterN p n R R' P Q Q' :
   IntoLaterN n R' R → Frame p R P Q → MakeLaterN n Q Q' → Frame p R' (▷^n P) Q'.
 Proof.
   rewrite /Frame /MakeLater /IntoLaterN=>-> <- <-.
-  by rewrite always_if_laterN laterN_sep.
+  by rewrite persistently_if_laterN laterN_sep.
 Qed.
 
-Class MakeAlways (P Q : uPred M) := make_always : □ P ⊣⊢ Q.
-Global Instance make_always_true : MakeAlways True True.
-Proof. by rewrite /MakeAlways always_pure. Qed.
-Global Instance make_always_default P : MakeAlways P (â–¡ P) | 100.
+Class MakePersistently (P Q : uPred M) := make_persistently : □ P ⊣⊢ Q.
+Global Instance make_persistently_true : MakePersistently True True.
+Proof. by rewrite /MakePersistently persistently_pure. Qed.
+Global Instance make_persistently_default P : MakePersistently P (â–¡ P) | 100.
 Proof. done. Qed.
 
-Global Instance frame_always R P Q Q' :
-  Frame true R P Q → MakeAlways Q Q' → Frame true R (□ P) Q'.
+Global Instance frame_persistently R P Q Q' :
+  Frame true R P Q → MakePersistently Q Q' → Frame true R (□ P) Q'.
 Proof.
-  rewrite /Frame /MakeAlways=> <- <-.
-  by rewrite always_sep /= always_always.
+  rewrite /Frame /MakePersistently=> <- <-.
+  by rewrite persistently_sep /= persistently_persistently.
 Qed.
 
 Class MakeExcept0 (P Q : uPred M) := make_except_0 : ◇ P ⊣⊢ Q.
@@ -623,9 +623,9 @@ Global Instance from_or_bupd P Q1 Q2 :
 Proof. rewrite /FromOr=><-. apply or_elim; apply bupd_mono; auto with I. Qed.
 Global Instance from_or_pure φ ψ : @FromOr M ⌜φ ∨ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
 Proof. by rewrite /FromOr pure_or. Qed.
-Global Instance from_or_always P Q1 Q2 :
+Global Instance from_or_persistently P Q1 Q2 :
   FromOr P Q1 Q2 → FromOr (□ P) (□ Q1) (□ Q2).
-Proof. rewrite /FromOr=> <-. by rewrite always_or. Qed.
+Proof. rewrite /FromOr=> <-. by rewrite persistently_or. Qed.
 Global Instance from_or_later P Q1 Q2 :
   FromOr P Q1 Q2 → FromOr (▷ P) (▷ Q1) (▷ Q2).
 Proof. rewrite /FromOr=><-. by rewrite later_or. Qed.
@@ -641,9 +641,9 @@ Global Instance into_or_or P Q : IntoOr (P ∨ Q) P Q.
 Proof. done. Qed.
 Global Instance into_or_pure φ ψ : @IntoOr M ⌜φ ∨ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
 Proof. by rewrite /IntoOr pure_or. Qed.
-Global Instance into_or_always P Q1 Q2 :
+Global Instance into_or_persistently P Q1 Q2 :
   IntoOr P Q1 Q2 → IntoOr (□ P) (□ Q1) (□ Q2).
-Proof. rewrite /IntoOr=>->. by rewrite always_or. Qed.
+Proof. rewrite /IntoOr=>->. by rewrite persistently_or. Qed.
 Global Instance into_or_later P Q1 Q2 :
   IntoOr P Q1 Q2 → IntoOr (▷ P) (▷ Q1) (▷ Q2).
 Proof. rewrite /IntoOr=>->. by rewrite later_or. Qed.
@@ -665,9 +665,9 @@ Qed.
 Global Instance from_exist_pure {A} (φ : A → Prop) :
   @FromExist M A ⌜∃ x, φ x⌝ (λ a, ⌜φ a⌝)%I.
 Proof. by rewrite /FromExist pure_exist. Qed.
-Global Instance from_exist_always {A} P (Φ : A → uPred M) :
+Global Instance from_exist_persistently {A} P (Φ : A → uPred M) :
   FromExist P Φ → FromExist (□ P) (λ a, □ (Φ a))%I.
-Proof. rewrite /FromExist=> <-. by rewrite always_exist. Qed.
+Proof. rewrite /FromExist=> <-. by rewrite persistently_exist. Qed.
 Global Instance from_exist_later {A} P (Φ : A → uPred M) :
   FromExist P Φ → FromExist (▷ P) (λ a, ▷ (Φ a))%I.
 Proof.
@@ -688,6 +688,7 @@ Proof. done. Qed.
 Global Instance into_exist_pure {A} (φ : A → Prop) :
   @IntoExist M A ⌜∃ x, φ x⌝ (λ a, ⌜φ a⌝)%I.
 Proof. by rewrite /IntoExist pure_exist. Qed.
+
 Global Instance into_exist_and_pure P Q φ :
   IntoPureT P φ → IntoExist (P ∧ Q) (λ _ : φ, Q).
 Proof.
@@ -701,9 +702,9 @@ Proof.
   apply pure_elim_sep_l=> Hφ. by rewrite -(exist_intro Hφ).
 Qed.
 
-Global Instance into_exist_always {A} P (Φ : A → uPred M) :
+Global Instance into_exist_persistently {A} P (Φ : A → uPred M) :
   IntoExist P Φ → IntoExist (□ P) (λ a, □ (Φ a))%I.
-Proof. rewrite /IntoExist=> HP. by rewrite HP always_exist. Qed.
+Proof. rewrite /IntoExist=> HP. by rewrite HP persistently_exist. Qed.
 Global Instance into_exist_later {A} P (Φ : A → uPred M) :
   IntoExist P Φ → Inhabited A → IntoExist (▷ P) (λ a, ▷ (Φ a))%I.
 Proof. rewrite /IntoExist=> HP ?. by rewrite HP later_exist. Qed.
@@ -717,9 +718,9 @@ Proof. rewrite /IntoExist=> HP ?. by rewrite HP except_0_exist. Qed.
 (* IntoForall *)
 Global Instance into_forall_forall {A} (Φ : A → uPred M) : IntoForall (∀ a, Φ a) Φ.
 Proof. done. Qed.
-Global Instance into_forall_always {A} P (Φ : A → uPred M) :
+Global Instance into_forall_persistently {A} P (Φ : A → uPred M) :
   IntoForall P Φ → IntoForall (□ P) (λ a, □ (Φ a))%I.
-Proof. rewrite /IntoForall=> HP. by rewrite HP always_forall. Qed.
+Proof. rewrite /IntoForall=> HP. by rewrite HP persistently_forall. Qed.
 Global Instance into_forall_later {A} P (Φ : A → uPred M) :
   IntoForall P Φ → IntoForall (▷ P) (λ a, ▷ (Φ a))%I.
 Proof. rewrite /IntoForall=> HP. by rewrite HP later_forall. Qed.
@@ -740,12 +741,12 @@ Global Instance from_forall_wand_pure P Q φ :
   IntoPureT P φ → FromForall (P -∗ Q) (λ _ : φ, Q)%I.
 Proof.
   intros (φ'&->&?). rewrite /FromForall -pure_impl_forall.
-  by rewrite always_impl_wand (into_pure P).
+  by rewrite persistently_impl_wand (into_pure P).
 Qed.
 
-Global Instance from_forall_always {A} P (Φ : A → uPred M) :
+Global Instance from_forall_persistently {A} P (Φ : A → uPred M) :
   FromForall P Φ → FromForall (□ P) (λ a, □ (Φ a))%I.
-Proof. rewrite /FromForall=> <-. by rewrite always_forall. Qed.
+Proof. rewrite /FromForall=> <-. by rewrite persistently_forall. Qed.
 Global Instance from_forall_later {A} P (Φ : A → uPred M) :
   FromForall P Φ → FromForall (▷ P) (λ a, ▷ (Φ a))%I.
 Proof. rewrite /FromForall=> <-. by rewrite later_forall. Qed.
@@ -771,8 +772,8 @@ Proof.
   rewrite /ElimModal=> H. apply forall_intro=> a. by rewrite (forall_elim a).
 Qed.
 
-Global Instance elim_modal_always P Q : ElimModal (â–¡ P) P Q Q.
-Proof. intros. by rewrite /ElimModal always_elim wand_elim_r. Qed.
+Global Instance elim_modal_persistently P Q : ElimModal (â–¡ P) P Q Q.
+Proof. intros. by rewrite /ElimModal persistently_elim wand_elim_r. Qed.
 
 Global Instance elim_modal_bupd P Q : ElimModal (|==> P) P (|==> Q) (|==> Q).
 Proof. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_trans. Qed.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 66e68407c2b6f12ebb5173a258da19389c44f2f1..fe35f90c26382b66f7f0cf0514c16a982261cd5d 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -15,7 +15,7 @@ Existing Instance Or_r | 10.
 Class FromAssumption {M} (p : bool) (P Q : uPred M) :=
   from_assumption : □?p P ⊢ Q.
 Arguments from_assumption {_} _ _ _ {_}.
-(* No need to restrict Hint Mode, we have a default instance that will always
+(* No need to restrict Hint Mode, we have a default instance that will persistently
 be used in case of evars *)
 Hint Mode FromAssumption + + - - : typeclass_instances.
 
@@ -125,8 +125,8 @@ Lemma mk_from_and_persistent {M} (P Q1 Q2 : uPred M) :
   Or (Persistent Q1) (Persistent Q2) → (Q1 ∗ Q2 ⊢ P) → FromAnd true P Q1 Q2.
 Proof.
   intros [?|?] ?; rewrite /FromAnd.
-  - by rewrite always_and_sep_l.
-  - by rewrite always_and_sep_r.
+  - by rewrite persistently_and_sep_l.
+  - by rewrite persistently_and_sep_r.
 Qed.
 
 Class IntoAnd {M} (p : bool) (P Q1 Q2 : uPred M) :=
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index a674e9465b56d47c5a9aa341eb9c37d851e5a41b..1d69bf60b8963b346b6830aa58de1e20996935bc 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -140,7 +140,7 @@ Lemma envs_lookup_sound Δ i p P :
 Proof.
   rewrite /envs_lookup /envs_delete /of_envs=>?; apply pure_elim_sep_l=> Hwf.
   destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
-  - rewrite (env_lookup_perm Γp) //= always_sep.
+  - rewrite (env_lookup_perm Γp) //= persistently_sep.
     ecancel [□ [∗] _; □ P; [∗] Γs]%I; apply pure_intro.
     destruct Hwf; constructor;
       naive_solver eauto using env_delete_wf, env_delete_fresh.
@@ -152,11 +152,11 @@ Proof.
 Qed.
 Lemma envs_lookup_sound' Δ i p P :
   envs_lookup i Δ = Some (p,P) → Δ ⊢ P ∗ envs_delete i p Δ.
-Proof. intros. rewrite envs_lookup_sound //. by rewrite always_if_elim. Qed.
+Proof. intros. rewrite envs_lookup_sound //. by rewrite persistently_if_elim. Qed.
 Lemma envs_lookup_persistent_sound Δ i P :
   envs_lookup i Δ = Some (true,P) → Δ ⊢ □ P ∗ Δ.
 Proof.
-  intros. apply (always_entails_l _ _). by rewrite envs_lookup_sound // sep_elim_l.
+  intros. apply (persistently_entails_l _ _). by rewrite envs_lookup_sound // sep_elim_l.
 Qed.
 
 Lemma envs_lookup_split Δ i p P :
@@ -164,7 +164,7 @@ Lemma envs_lookup_split Δ i p P :
 Proof.
   rewrite /envs_lookup /of_envs=>?; apply pure_elim_sep_l=> Hwf.
   destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
-  - rewrite (env_lookup_perm Γp) //= always_sep.
+  - rewrite (env_lookup_perm Γp) //= persistently_sep.
     rewrite pure_True // left_id.
     cancel [â–¡ P]%I. apply wand_intro_l. solve_sep_entails.
   - destruct (Γs !! i) eqn:?; simplify_eq/=.
@@ -183,15 +183,15 @@ Lemma envs_lookup_delete_list_sound Δ Δ' js rp p Ps :
   envs_lookup_delete_list js rp Δ = Some (p, Ps,Δ') → Δ ⊢ □?p [∗] Ps ∗ Δ'.
 Proof.
   revert Δ Δ' p Ps. induction js as [|j js IH]=> Δ Δ'' p Ps ?; simplify_eq/=.
-  { by rewrite always_pure left_id. }
+  { by rewrite persistently_pure left_id. }
   destruct (envs_lookup_delete j Δ) as [[[q1 P] Δ']|] eqn:Hj; simplify_eq/=.
   apply envs_lookup_delete_Some in Hj as [Hj ->].
   destruct (envs_lookup_delete_list js rp _) as [[[q2 Ps'] ?]|] eqn:?; simplify_eq/=.
-  rewrite always_if_sep -assoc. destruct q1; simpl.
+  rewrite persistently_if_sep -assoc. destruct q1; simpl.
   - destruct rp.
-    + rewrite envs_lookup_sound //; simpl. by rewrite IH // (always_elim_if q2).
-    + rewrite envs_lookup_persistent_sound //. by rewrite IH // (always_elim_if q2).
-  - rewrite envs_lookup_sound // IH //; simpl. by rewrite always_if_elim.
+    + rewrite envs_lookup_sound //; simpl. by rewrite IH // (persistently_elim_if q2).
+    + rewrite envs_lookup_persistent_sound //. by rewrite IH // (persistently_elim_if q2).
+  - rewrite envs_lookup_sound // IH //; simpl. by rewrite persistently_if_elim.
 Qed.
 
 Lemma envs_lookup_snoc Δ i p P :
@@ -216,7 +216,7 @@ Proof.
   - apply sep_intro_True_l; [apply pure_intro|].
     + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
       intros j; destruct (strings.string_beq_reflect j i); naive_solver.
-    + by rewrite always_sep assoc.
+    + by rewrite persistently_sep assoc.
   - apply sep_intro_True_l; [apply pure_intro|].
     + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
       intros j; destruct (strings.string_beq_reflect j i); naive_solver.
@@ -234,7 +234,7 @@ Proof.
       intros j. apply (env_app_disjoint _ _ _ j) in Happ.
       naive_solver eauto using env_app_fresh.
     + rewrite (env_app_perm _ _ Γp') //.
-      rewrite big_opL_app always_sep. solve_sep_entails.
+      rewrite big_opL_app persistently_sep. solve_sep_entails.
   - destruct (env_app Γ Γp) eqn:Happ,
       (env_app Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
     apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
@@ -257,7 +257,7 @@ Proof.
       intros j. apply (env_app_disjoint _ _ _ j) in Happ.
       destruct (decide (i = j)); try naive_solver eauto using env_replace_fresh.
     + rewrite (env_replace_perm _ _ Γp') //.
-      rewrite big_opL_app always_sep. solve_sep_entails.
+      rewrite big_opL_app persistently_sep. solve_sep_entails.
   - destruct (env_app Γ Γp) eqn:Happ,
       (env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
     apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
@@ -345,7 +345,7 @@ Lemma envs_split_sound Δ lr js Δ1 Δ2 :
   envs_split lr js Δ = Some (Δ1,Δ2) → Δ ⊢ Δ1 ∗ Δ2.
 Proof.
   rewrite /envs_split=> ?. rewrite -(idemp uPred_and Δ).
-  rewrite {2}envs_clear_spatial_sound sep_elim_l always_and_sep_r.
+  rewrite {2}envs_clear_spatial_sound sep_elim_l persistently_and_sep_r.
   destruct (envs_split_go _ _) as [[Δ1' Δ2']|] eqn:HΔ; [|done].
   apply envs_split_go_sound in HΔ as ->; last first.
   { intros j P. by rewrite envs_lookup_envs_clear_spatial=> ->. }
@@ -388,7 +388,7 @@ Proof. by constructor. Qed.
 (** * Adequacy *)
 Lemma tac_adequate P : (Envs Enil Enil ⊢ P) → P.
 Proof.
-  intros <-. rewrite /of_envs /= always_pure !right_id.
+  intros <-. rewrite /of_envs /= persistently_pure !right_id.
   apply pure_intro; repeat constructor.
 Qed.
 
@@ -450,8 +450,8 @@ Proof. by split. Qed.
 
 Lemma into_laterN_env_sound n Δ1 Δ2 : IntoLaterNEnvs n Δ1 Δ2 → Δ1 ⊢ ▷^n Δ2.
 Proof.
-  intros [Hp Hs]; rewrite /of_envs /= !laterN_sep -always_laterN.
-  repeat apply sep_mono; try apply always_mono.
+  intros [Hp Hs]; rewrite /of_envs /= !laterN_sep -persistently_laterN.
+  repeat apply sep_mono; try apply persistently_mono.
   - rewrite -laterN_intro; apply pure_mono; destruct 1; constructor;
       naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
   - induction Hp; rewrite /= ?laterN_sep. apply laterN_intro. by apply sep_mono.
@@ -467,18 +467,18 @@ Lemma tac_löb Δ Δ' i Q :
   envs_app true (Esnoc Enil i (▷ Q)%I) Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
-  intros ?? HQ. rewrite -(always_elim Q) -(löb (□ Q)) -always_later.
-  apply impl_intro_l, (always_intro _ _).
+  intros ?? HQ. rewrite -(persistently_elim Q) -(löb (□ Q)) -persistently_later.
+  apply impl_intro_l, (persistently_intro _ _).
   rewrite envs_app_sound //; simpl.
-  by rewrite right_id always_and_sep_l' wand_elim_r HQ.
+  by rewrite right_id persistently_and_sep_l' wand_elim_r HQ.
 Qed.
 
 (** * Always *)
-Lemma tac_always_intro Δ Q :
+Lemma tac_persistently_intro Δ Q :
   (envs_clear_spatial Δ ⊢ Q) → Δ ⊢ □ Q.
 Proof.
   intros <-. rewrite envs_clear_spatial_sound sep_elim_l.
-  by apply (always_intro _ _).
+  by apply (persistently_intro _ _).
 Qed.
 
 Lemma tac_persistent Δ Δ' i p P P' Q :
@@ -499,9 +499,9 @@ Lemma tac_impl_intro Δ Δ' i P Q :
 Proof.
   intros ?? <-. destruct (env_spatial_is_nil Δ) eqn:?.
   - rewrite (persistent Δ) envs_app_sound //; simpl.
-    by rewrite right_id always_wand_impl always_elim.
+    by rewrite right_id persistently_wand_impl persistently_elim.
   - apply impl_intro_l. rewrite envs_app_sound //; simpl.
-    by rewrite always_and_sep_l right_id wand_elim_r.
+    by rewrite persistently_and_sep_l right_id wand_elim_r.
 Qed.
 Lemma tac_impl_intro_persistent Δ Δ' i P P' Q :
   IntoPersistent false P P' →
@@ -510,7 +510,7 @@ Lemma tac_impl_intro_persistent Δ Δ' i P P' Q :
 Proof.
   intros ?? HQ. rewrite envs_app_sound //=; simpl. apply impl_intro_l.
   rewrite (_ : P = â–¡?false P) // (into_persistent false P).
-  by rewrite right_id always_and_sep_l wand_elim_r.
+  by rewrite right_id persistently_and_sep_l wand_elim_r.
 Qed.
 
 Lemma tac_impl_intro_drop Δ P Q : (Δ ⊢ Q) → Δ ⊢ P → Q.
@@ -552,11 +552,11 @@ Proof.
   intros [? ->]%envs_lookup_delete_Some ??? <-. destruct p.
   - rewrite envs_lookup_persistent_sound // envs_simple_replace_sound //; simpl.
     rewrite right_id assoc (into_wand _ R) /=. destruct q; simpl.
-    + by rewrite always_wand always_always !wand_elim_r.
+    + by rewrite persistently_wand persistently_persistently !wand_elim_r.
     + by rewrite !wand_elim_r.
   - rewrite envs_lookup_sound //; simpl.
     rewrite envs_lookup_sound // (envs_replace_sound' _ Δ'') //; simpl.
-    by rewrite right_id assoc (into_wand _ R) always_if_elim wand_elim_r wand_elim_r.
+    by rewrite right_id assoc (into_wand _ R) persistently_if_elim wand_elim_r wand_elim_r.
 Qed.
 
 Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q lr js R P1 P2 P1' Q :
@@ -574,7 +574,7 @@ Proof.
   rewrite (envs_app_sound Δ2) //; simpl.
   rewrite right_id (into_wand _ R) HP1 assoc -(comm _ P1') -assoc.
   rewrite -(elim_modal P1' P1 Q Q). apply sep_mono_r, wand_intro_l.
-  by rewrite always_if_elim assoc !wand_elim_r.
+  by rewrite persistently_if_elim assoc !wand_elim_r.
 Qed.
 
 Lemma tac_unlock P Q : (P ⊢ Q) → P ⊢ locked Q.
@@ -590,7 +590,7 @@ Lemma tac_specialize_frame Δ Δ' j q R P1 P2 P1' Q Q' :
 Proof.
   intros [? ->]%envs_lookup_delete_Some ?? HPQ ->.
   rewrite envs_lookup_sound //. rewrite HPQ -lock.
-  rewrite (into_wand _ R) assoc -(comm _ P1') -assoc always_if_elim.
+  rewrite (into_wand _ R) assoc -(comm _ P1') -assoc persistently_if_elim.
   rewrite -{2}(elim_modal P1' P1 Q Q). apply sep_mono_r, wand_intro_l.
   by rewrite assoc !wand_elim_r.
 Qed.
@@ -615,9 +615,9 @@ Proof.
   intros [? ->]%envs_lookup_delete_Some ??? HP1 <-.
   rewrite envs_lookup_sound //.
   rewrite -(idemp uPred_and (envs_delete _ _ _)).
-  rewrite {1}HP1 (persistent P1) always_and_sep_l assoc.
+  rewrite {1}HP1 (persistent P1) persistently_and_sep_l assoc.
   rewrite envs_simple_replace_sound' //; simpl.
-  rewrite right_id (into_wand _ R) (always_elim_if q) -always_if_sep wand_elim_l.
+  rewrite right_id (into_wand _ R) (persistently_elim_if q) -persistently_if_sep wand_elim_l.
   by rewrite wand_elim_r.
 Qed.
 
@@ -628,9 +628,9 @@ Lemma tac_specialize_persistent_helper Δ Δ' j q P R Q :
   (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros ? HR ?? <-.
-  rewrite -(idemp uPred_and Δ) {1}HR always_and_sep_l.
+  rewrite -(idemp uPred_and Δ) {1}HR persistently_and_sep_l.
   rewrite envs_replace_sound //; simpl.
-  by rewrite right_id assoc (sep_elim_l R) always_always wand_elim_r.
+  by rewrite right_id assoc (sep_elim_l R) persistently_persistently wand_elim_r.
 Qed.
 
 Lemma tac_revert Δ Δ' i p P Q :
@@ -638,7 +638,7 @@ Lemma tac_revert Δ Δ' i p P Q :
   (Δ' ⊢ (if p then □ P else P) -∗ Q) → Δ ⊢ Q.
 Proof.
   intros ? HQ. rewrite envs_lookup_delete_sound //; simpl.
-  by rewrite HQ /uPred_always_if wand_elim_r.
+  by rewrite HQ /uPred_persistently_if wand_elim_r.
 Qed.
 
 Class IntoIH (φ : Prop) (Δ : envs M) (Q : uPred M) :=
@@ -680,7 +680,7 @@ Lemma tac_assert_persistent Δ Δ1 Δ2 Δ' lr js j P Q :
   (Δ1 ⊢ P) → (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros ??? HP <-. rewrite -(idemp uPred_and Δ) {1}envs_split_sound //.
-  rewrite HP sep_elim_l (always_and_sep_l P) envs_app_sound //; simpl.
+  rewrite HP sep_elim_l (persistently_and_sep_l P) envs_app_sound //; simpl.
   by rewrite right_id wand_elim_r.
 Qed.
 
@@ -690,7 +690,7 @@ Lemma tac_assert_pure Δ Δ' j P φ Q :
   φ → (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros ??? <-. rewrite envs_app_sound //; simpl.
-  by rewrite right_id -(from_pure P) pure_True // -always_impl_wand True_impl.
+  by rewrite right_id -(from_pure P) pure_True // -persistently_impl_wand True_impl.
 Qed.
 
 Lemma tac_pose_proof Δ Δ' j P Q :
@@ -699,7 +699,7 @@ Lemma tac_pose_proof Δ Δ' j P Q :
   (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros HP ? <-. rewrite envs_app_sound //; simpl.
-  by rewrite right_id -HP always_pure wand_True.
+  by rewrite right_id -HP persistently_pure wand_True.
 Qed.
 
 Lemma tac_pose_proof_hyp Δ Δ' Δ'' i p j P Q :
@@ -748,7 +748,7 @@ Lemma tac_rewrite_in Δ i p Pxy j q P (lr : bool) Q :
 Proof.
   intros ?? A Δ' x y Φ HPxy HP ?? <-.
   rewrite -(idemp uPred_and Δ) {2}(envs_lookup_sound' _ i) //.
-  rewrite sep_elim_l HPxy always_and_sep_r.
+  rewrite sep_elim_l HPxy persistently_and_sep_r.
   rewrite (envs_simple_replace_sound _ _ j) //; simpl.
   rewrite HP right_id -assoc; apply wand_elim_r'. destruct lr.
   - apply (internal_eq_rewrite x y (λ y, □?q Φ y -∗ Δ')%I);
@@ -803,7 +803,7 @@ Lemma tac_and_destruct Δ Δ' i p j1 j2 P P1 P2 Q :
   (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros. rewrite envs_simple_replace_sound //; simpl. rewrite (into_and p P).
-  by destruct p; rewrite /= ?right_id (comm _ P1) ?always_and_sep wand_elim_r.
+  by destruct p; rewrite /= ?right_id (comm _ P1) ?persistently_and_sep wand_elim_r.
 Qed.
 
 (* Using this tactic, one can destruct a (non-separating) conjunction in the
@@ -824,7 +824,7 @@ Qed.
 Lemma tac_frame_pure Δ (φ : Prop) P Q :
   φ → Frame true ⌜φ⌝ P Q → (Δ ⊢ Q) → Δ ⊢ P.
 Proof.
-  intros ?? ->. by rewrite -(frame ⌜φ⌝ P) /= always_pure pure_True // left_id.
+  intros ?? ->. by rewrite -(frame ⌜φ⌝ P) /= persistently_pure pure_True // left_id.
 Qed.
 
 Lemma tac_frame Δ Δ' i p R P Q :
@@ -849,7 +849,7 @@ Lemma tac_or_destruct Δ Δ1 Δ2 i p j1 j2 P P1 P2 Q :
   (Δ1 ⊢ Q) → (Δ2 ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros ???? HP1 HP2. rewrite envs_lookup_sound //.
-  rewrite (into_or P) always_if_or sep_or_r; apply or_elim.
+  rewrite (into_or P) persistently_if_or sep_or_r; apply or_elim.
   - rewrite (envs_simple_replace_sound' _ Δ1) //.
     by rewrite /= right_id wand_elim_r.
   - rewrite (envs_simple_replace_sound' _ Δ2) //.
@@ -890,7 +890,7 @@ Lemma tac_exist_destruct {A} Δ i p j P (Φ : A → uPred M) Q :
   Δ ⊢ Q.
 Proof.
   intros ?? HΦ. rewrite envs_lookup_sound //.
-  rewrite (into_exist P) always_if_exist sep_exist_r.
+  rewrite (into_exist P) persistently_if_exist sep_exist_r.
   apply exist_elim=> a; destruct (HΦ a) as (Δ'&?&?).
   rewrite envs_simple_replace_sound' //; simpl. by rewrite right_id wand_elim_r.
 Qed.
@@ -906,6 +906,6 @@ Lemma tac_modal_elim Δ Δ' i p P' P Q Q' :
   (Δ' ⊢ Q') → Δ ⊢ Q.
 Proof.
   intros ??? HΔ. rewrite envs_replace_sound //; simpl.
-  rewrite right_id HΔ always_if_elim. by apply elim_modal.
+  rewrite right_id HΔ persistently_if_elim. by apply elim_modal.
 Qed.
 End tactics.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index df997893a4b8faf46d52cb25c65f63ff94a07338..cfc0658260fd598ed221f0fac755a92a0be74082 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -802,8 +802,8 @@ Local Tactic Notation "iExistDestruct" constr(H)
 (** * Always *)
 Tactic Notation "iAlways":=
   iStartProof;
-  apply tac_always_intro; env_cbv
-    || fail "iAlways: the goal is not an always modality".
+  apply tac_persistently_intro; env_cbv
+    || fail "iAlways: the goal is not an persistently modality".
 
 (** * Later *)
 Tactic Notation "iNext" open_constr(n) :=
@@ -1217,7 +1217,7 @@ Instance copy_destruct_impl {M} (P Q : uPred M) :
   CopyDestruct Q → CopyDestruct (P → Q).
 Instance copy_destruct_wand {M} (P Q : uPred M) :
   CopyDestruct Q → CopyDestruct (P -∗ Q).
-Instance copy_destruct_always {M} (P : uPred M) :
+Instance copy_destruct_persistently {M} (P : uPred M) :
   CopyDestruct P → CopyDestruct (□ P).
 
 Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic(tac) :=
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 96ceba7824627eec12c63470b98d9e97f7be7473..71505deab13254b7af0dbea0c04a4133b18e39a7 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -177,7 +177,7 @@ Lemma test_iFrame_persistent (P Q : uPred M) :
   □ P -∗ Q -∗ □ (P ∗ P) ∗ (P ∧ Q ∨ Q).
 Proof. iIntros "#HP". iFrame "HP". iIntros "$". Qed.
 
-Lemma test_iSplit_always P Q : □ P -∗ □ (P ∗ P).
+Lemma test_iSplit_persistently P Q : □ P -∗ □ (P ∗ P).
 Proof. iIntros "#?". by iSplit. Qed.
 
 Lemma test_iSpecialize_persistent P Q :