diff --git a/theories/base_logic/big_op.v b/theories/base_logic/big_op.v
index 9b9daea32a22a5a4ff0b6ca3b520d6d444b436e9..281daba8019e26a225786455713325f235101242 100644
--- a/theories/base_logic/big_op.v
+++ b/theories/base_logic/big_op.v
@@ -126,7 +126,7 @@ Section list.
   Proof. apply (big_opL_commute _). Qed.
 
   Lemma big_sepL_forall Φ l :
-    (∀ k x, PersistentP (Φ k x)) →
+    (∀ k x, Persistent (Φ k x)) →
     ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ (∀ k x, ⌜l !! k = Some x⌝ → Φ k x).
   Proof.
     intros HΦ. apply (anti_symm _).
@@ -150,23 +150,23 @@ Section list.
   Qed.
 
   Global Instance big_sepL_nil_persistent Φ :
-    PersistentP ([∗ list] k↦x ∈ [], Φ k x).
+    Persistent ([∗ list] k↦x ∈ [], Φ k x).
   Proof. simpl; apply _. Qed.
   Global Instance big_sepL_persistent Φ l :
-    (∀ k x, PersistentP (Φ k x)) → PersistentP ([∗ list] k↦x ∈ l, Φ k x).
+    (∀ k x, Persistent (Φ k x)) → Persistent ([∗ list] k↦x ∈ l, Φ k x).
   Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
   Global Instance big_sepL_persistent_id Ps :
-    TCForall PersistentP Ps → PersistentP ([∗] Ps).
+    TCForall Persistent Ps → Persistent ([∗] Ps).
   Proof. induction 1; simpl; apply _. Qed.
 
   Global Instance big_sepL_nil_timeless Φ :
-    TimelessP ([∗ list] k↦x ∈ [], Φ k x).
+    Timeless ([∗ list] k↦x ∈ [], Φ k x).
   Proof. simpl; apply _. Qed.
   Global Instance big_sepL_timeless Φ l :
-    (∀ k x, TimelessP (Φ k x)) → TimelessP ([∗ list] k↦x ∈ l, Φ k x).
+    (∀ k x, Timeless (Φ k x)) → Timeless ([∗ list] k↦x ∈ l, Φ k x).
   Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
   Global Instance big_sepL_timeless_id Ps :
-    TCForall TimelessP Ps → TimelessP ([∗] Ps).
+    TCForall Timeless Ps → Timeless ([∗] Ps).
   Proof. induction 1; simpl; apply _. Qed.
 End list.
 
@@ -316,7 +316,7 @@ Section gmap.
   Proof. apply (big_opM_commute _). Qed.
 
   Lemma big_sepM_forall Φ m :
-    (∀ k x, PersistentP (Φ k x)) →
+    (∀ k x, Persistent (Φ k x)) →
     ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ (∀ k x, ⌜m !! k = Some x⌝ → Φ k x).
   Proof.
     intros. apply (anti_symm _).
@@ -343,16 +343,16 @@ Section gmap.
   Qed.
 
   Global Instance big_sepM_empty_persistent Φ :
-    PersistentP ([∗ map] k↦x ∈ ∅, Φ k x).
+    Persistent ([∗ map] k↦x ∈ ∅, Φ k x).
   Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
   Global Instance big_sepM_persistent Φ m :
-    (∀ k x, PersistentP (Φ k x)) → PersistentP ([∗ map] k↦x ∈ m, Φ k x).
+    (∀ k x, Persistent (Φ k x)) → Persistent ([∗ map] k↦x ∈ m, Φ k x).
   Proof. intros. apply big_sepL_persistent=> _ [??]; apply _. Qed.
   Global Instance big_sepM_nil_timeless Φ :
-    TimelessP ([∗ map] k↦x ∈ ∅, Φ k x).
+    Timeless ([∗ map] k↦x ∈ ∅, Φ k x).
   Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
   Global Instance big_sepM_timeless Φ m :
-    (∀ k x, TimelessP (Φ k x)) → TimelessP ([∗ map] k↦x ∈ m, Φ k x).
+    (∀ k x, Timeless (Φ k x)) → Timeless ([∗ map] k↦x ∈ m, Φ k x).
   Proof. intros. apply big_sepL_timeless=> _ [??]; apply _. Qed.
 End gmap.
 
@@ -468,7 +468,7 @@ Section gset.
   Proof. apply (big_opS_commute _). Qed.
 
   Lemma big_sepS_forall Φ X :
-    (∀ x, PersistentP (Φ x)) → ([∗ set] x ∈ X, Φ x) ⊣⊢ (∀ x, ⌜x ∈ X⌝ → Φ x).
+    (∀ x, Persistent (Φ x)) → ([∗ set] x ∈ X, Φ x) ⊣⊢ (∀ x, ⌜x ∈ X⌝ → Φ x).
   Proof.
     intros. apply (anti_symm _).
     { apply forall_intro=> x.
@@ -490,15 +490,15 @@ Section gset.
     by rewrite -always_wand_impl always_elim wand_elim_l.
   Qed.
 
-  Global Instance big_sepS_empty_persistent Φ : PersistentP ([∗ set] x ∈ ∅, Φ x).
+  Global Instance big_sepS_empty_persistent Φ : Persistent ([∗ set] x ∈ ∅, Φ x).
   Proof. rewrite /big_opS elements_empty. apply _. Qed.
   Global Instance big_sepS_persistent Φ X :
-    (∀ x, PersistentP (Φ x)) → PersistentP ([∗ set] x ∈ X, Φ x).
+    (∀ x, Persistent (Φ x)) → Persistent ([∗ set] x ∈ X, Φ x).
   Proof. rewrite /big_opS. apply _. Qed.
-  Global Instance big_sepS_nil_timeless Φ : TimelessP ([∗ set] x ∈ ∅, Φ x).
+  Global Instance big_sepS_nil_timeless Φ : Timeless ([∗ set] x ∈ ∅, Φ x).
   Proof. rewrite /big_opS elements_empty. apply _. Qed.
   Global Instance big_sepS_timeless Φ X :
-    (∀ x, TimelessP (Φ x)) → TimelessP ([∗ set] x ∈ X, Φ x).
+    (∀ x, Timeless (Φ x)) → Timeless ([∗ set] x ∈ X, Φ x).
   Proof. rewrite /big_opS. apply _. Qed.
 End gset.
 
@@ -578,15 +578,15 @@ Section gmultiset.
     □?q ([∗ mset] y ∈ X, Φ y) ⊣⊢ ([∗ mset] y ∈ X, □?q Φ y).
   Proof. apply (big_opMS_commute _). Qed.
 
-  Global Instance big_sepMS_empty_persistent Φ : PersistentP ([∗ mset] x ∈ ∅, Φ x).
+  Global Instance big_sepMS_empty_persistent Φ : Persistent ([∗ mset] x ∈ ∅, Φ x).
   Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed.
   Global Instance big_sepMS_persistent Φ X :
-    (∀ x, PersistentP (Φ x)) → PersistentP ([∗ mset] x ∈ X, Φ x).
+    (∀ x, Persistent (Φ x)) → Persistent ([∗ mset] x ∈ X, Φ x).
   Proof. rewrite /big_opMS. apply _. Qed.
-  Global Instance big_sepMS_nil_timeless Φ : TimelessP ([∗ mset] x ∈ ∅, Φ x).
+  Global Instance big_sepMS_nil_timeless Φ : Timeless ([∗ mset] x ∈ ∅, Φ x).
   Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed.
   Global Instance big_sepMS_timeless Φ X :
-    (∀ x, TimelessP (Φ x)) → TimelessP ([∗ mset] x ∈ X, Φ x).
+    (∀ x, Timeless (Φ x)) → Timeless ([∗ mset] x ∈ X, Φ x).
   Proof. rewrite /big_opMS. apply _. Qed.
 End gmultiset.
 End big_op.
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index abb22af999528be7cbbca1167458df8f127814cd..cfca37ec9b2deedce019eb77af761281565c1a0e 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -29,15 +29,15 @@ Notation "â—‡ P" := (uPred_except_0 P)
 Instance: Params (@uPred_except_0) 1.
 Typeclasses Opaque uPred_except_0.
 
-Class TimelessP {M} (P : uPred M) := timelessP : ▷ P ⊢ ◇ P.
+Class Timeless {M} (P : uPred M) := timelessP : ▷ P ⊢ ◇ P.
 Arguments timelessP {_} _ {_}.
-Hint Mode TimelessP + ! : typeclass_instances.
-Instance: Params (@TimelessP) 1.
+Hint Mode Timeless + ! : typeclass_instances.
+Instance: Params (@Timeless) 1.
 
-Class PersistentP {M} (P : uPred M) := persistentP : P ⊢ □ P.
-Arguments persistentP {_} _ {_}.
-Hint Mode PersistentP + ! : typeclass_instances.
-Instance: Params (@PersistentP) 1.
+Class Persistent {M} (P : uPred M) := persistent : P ⊢ □ P.
+Arguments persistent {_} _ {_}.
+Hint Mode Persistent + ! : typeclass_instances.
+Instance: Params (@Persistent) 1.
 
 Module uPred.
 Section derived.
@@ -794,33 +794,32 @@ Proof.
   by rewrite -bupd_intro -or_intro_l.
 Qed.
 
-(* Discrete instances *)
-Global Instance TimelessP_proper : Proper ((≡) ==> iff) (@TimelessP M).
+Global Instance Timeless_proper : Proper ((≡) ==> iff) (@Timeless M).
 Proof. solve_proper. Qed.
-Global Instance pure_timeless φ : TimelessP (⌜φ⌝ : uPred M)%I.
+Global Instance pure_timeless φ : Timeless (⌜φ⌝ : uPred M)%I.
 Proof.
-  rewrite /TimelessP pure_alt later_exist_false. by setoid_rewrite later_True.
+  rewrite /Timeless pure_alt later_exist_false. by setoid_rewrite later_True.
 Qed.
 Global Instance valid_timeless {A : cmraT} `{CmraDiscrete A} (a : A) :
-  TimelessP (✓ a : uPred M)%I.
-Proof. rewrite /TimelessP !discrete_valid. apply (timelessP _). Qed.
-Global Instance and_timeless P Q: TimelessP P → TimelessP Q → TimelessP (P ∧ Q).
-Proof. intros; rewrite /TimelessP except_0_and later_and; auto. Qed.
-Global Instance or_timeless P Q : TimelessP P → TimelessP Q → TimelessP (P ∨ Q).
-Proof. intros; rewrite /TimelessP except_0_or later_or; auto. Qed.
-Global Instance impl_timeless P Q : TimelessP Q → TimelessP (P → Q).
-Proof.
-  rewrite /TimelessP=> HQ. rewrite later_false_excluded_middle.
+  Timeless (✓ a : uPred M)%I.
+Proof. rewrite /Timeless !discrete_valid. apply (timelessP _). Qed.
+Global Instance and_timeless P Q: Timeless P → Timeless Q → Timeless (P ∧ Q).
+Proof. intros; rewrite /Timeless except_0_and later_and; auto. Qed.
+Global Instance or_timeless P Q : Timeless P → Timeless Q → Timeless (P ∨ Q).
+Proof. intros; rewrite /Timeless except_0_or later_or; auto. Qed.
+Global Instance impl_timeless P Q : Timeless Q → Timeless (P → Q).
+Proof.
+  rewrite /Timeless=> HQ. rewrite later_false_excluded_middle.
   apply or_mono, impl_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.
   by rewrite assoc (comm _ _ P) -assoc !impl_elim_r.
 Qed.
-Global Instance sep_timeless P Q: TimelessP P → TimelessP Q → TimelessP (P ∗ Q).
-Proof. intros; rewrite /TimelessP except_0_sep later_sep; auto. Qed.
-Global Instance wand_timeless P Q : TimelessP Q → TimelessP (P -∗ Q).
+Global Instance sep_timeless P Q: Timeless P → Timeless Q → Timeless (P ∗ Q).
+Proof. intros; rewrite /Timeless except_0_sep later_sep; auto. Qed.
+Global Instance wand_timeless P Q : Timeless Q → Timeless (P -∗ Q).
 Proof.
-  rewrite /TimelessP=> HQ. rewrite later_false_excluded_middle.
+  rewrite /Timeless=> HQ. rewrite later_false_excluded_middle.
   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.
@@ -828,113 +827,113 @@ Proof.
   by rewrite assoc (comm _ _ P) -assoc -always_and_sep_l' impl_elim_r wand_elim_r.
 Qed.
 Global Instance forall_timeless {A} (Ψ : A → uPred M) :
-  (∀ x, TimelessP (Ψ x)) → TimelessP (∀ x, Ψ x).
+  (∀ x, Timeless (Ψ x)) → Timeless (∀ x, Ψ x).
 Proof.
-  rewrite /TimelessP=> HQ. rewrite later_false_excluded_middle.
+  rewrite /Timeless=> HQ. rewrite later_false_excluded_middle.
   apply or_mono; first done. apply forall_intro=> x.
   rewrite -(löb (Ψ x)); apply impl_intro_l.
   rewrite HQ /uPred_except_0 !and_or_r. apply or_elim; last auto.
   by rewrite impl_elim_r (forall_elim x).
 Qed.
 Global Instance exist_timeless {A} (Ψ : A → uPred M) :
-  (∀ x, TimelessP (Ψ x)) → TimelessP (∃ x, Ψ x).
+  (∀ x, Timeless (Ψ x)) → Timeless (∃ x, Ψ x).
 Proof.
-  rewrite /TimelessP=> ?. rewrite later_exist_false. apply or_elim.
+  rewrite /Timeless=> ?. rewrite later_exist_false. apply or_elim.
   - rewrite /uPred_except_0; auto.
   - apply exist_elim=> x. rewrite -(exist_intro x); auto.
 Qed.
-Global Instance always_timeless P : TimelessP P → TimelessP (□ P).
-Proof. intros; rewrite /TimelessP except_0_always -always_later; auto. Qed.
-Global Instance always_if_timeless p P : TimelessP P → TimelessP (□?p P).
+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).
 Proof. destruct p; apply _. Qed.
 Global Instance eq_timeless {A : ofeT} (a b : A) :
-  Discrete a → TimelessP (a ≡ b : uPred M)%I.
-Proof. intros. rewrite /TimelessP !discrete_eq. apply (timelessP _). Qed.
-Global Instance ownM_timeless (a : M) : Discrete a → TimelessP (uPred_ownM a).
+  Discrete a → Timeless (a ≡ b : uPred M)%I.
+Proof. intros. rewrite /Timeless !discrete_eq. apply (timelessP _). Qed.
+Global Instance ownM_timeless (a : M) : Discrete a → Timeless (uPred_ownM a).
 Proof.
-  intros ?. rewrite /TimelessP later_ownM. apply exist_elim=> b.
+  intros ?. rewrite /Timeless later_ownM. apply exist_elim=> b.
   rewrite (timelessP (a≡b)) (except_0_intro (uPred_ownM b)) -except_0_and.
   apply except_0_mono. rewrite internal_eq_sym.
   apply (internal_eq_rewrite b a (uPred_ownM)); first apply _; auto.
 Qed.
 Global Instance from_option_timeless {A} P (Ψ : A → uPred M) (mx : option A) :
-  (∀ x, TimelessP (Ψ x)) → TimelessP P → TimelessP (from_option Ψ P mx).
+  (∀ x, Timeless (Ψ x)) → Timeless P → Timeless (from_option Ψ P mx).
 Proof. destruct mx; apply _. Qed.
 
 (* Derived lemmas for persistence *)
-Global Instance PersistentP_proper : Proper ((≡) ==> iff) (@PersistentP M).
+Global Instance Persistent_proper : Proper ((≡) ==> iff) (@Persistent M).
 Proof. solve_proper. Qed.
-Global Instance limit_preserving_PersistentP {A:ofeT} `{Cofe A} (Φ : A → uPred M) :
-  NonExpansive Φ → LimitPreserving (λ x, PersistentP (Φ x)).
+Global Instance limit_preserving_Persistent {A:ofeT} `{Cofe A} (Φ : A → uPred M) :
+  NonExpansive Φ → LimitPreserving (λ x, Persistent (Φ x)).
 Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
 
-Lemma always_always P `{!PersistentP P} : □ P ⊣⊢ P.
+Lemma always_always P `{!Persistent P} : □ P ⊣⊢ P.
 Proof. apply (anti_symm (⊢)); auto using always_elim. Qed.
-Lemma always_if_always p P `{!PersistentP P} : □?p P ⊣⊢ P.
+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 `{!PersistentP P} : (P ⊢ Q) → P ⊢ □ Q.
+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 `{!PersistentP P} : P ∧ Q ⊣⊢ P ∗ Q.
+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 `{!PersistentP Q} : P ∧ Q ⊣⊢ P ∗ Q.
+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 `{!PersistentP P} : P ⊣⊢ P ∗ P.
+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 `{!PersistentP Q} : (P ⊢ Q) → P ⊢ Q ∗ P.
+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 `{!PersistentP Q} : (P ⊢ Q) → P ⊢ P ∗ Q.
+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 `{!PersistentP P} Q : (P → Q) ⊣⊢ (P -∗ Q).
+Lemma always_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.
 Qed.
 
 (* Persistence *)
-Global Instance pure_persistent φ : PersistentP (⌜φ⌝ : uPred M)%I.
-Proof. by rewrite /PersistentP always_pure. Qed.
+Global Instance pure_persistent φ : Persistent (⌜φ⌝ : uPred M)%I.
+Proof. by rewrite /Persistent always_pure. Qed.
 Global Instance pure_impl_persistent φ Q :
-  PersistentP Q → PersistentP (⌜φ⌝ → Q)%I.
+  Persistent Q → Persistent (⌜φ⌝ → Q)%I.
 Proof.
-  rewrite /PersistentP pure_impl_forall always_forall. auto using forall_mono.
+  rewrite /Persistent pure_impl_forall always_forall. auto using forall_mono.
 Qed.
 Global Instance pure_wand_persistent φ Q :
-  PersistentP Q → PersistentP (⌜φ⌝ -∗ Q)%I.
+  Persistent Q → Persistent (⌜φ⌝ -∗ Q)%I.
 Proof.
-  rewrite /PersistentP -always_impl_wand pure_impl_forall always_forall.
+  rewrite /Persistent -always_impl_wand pure_impl_forall always_forall.
   auto using forall_mono.
 Qed.
-Global Instance always_persistent P : PersistentP (â–¡ P).
+Global Instance always_persistent P : Persistent (â–¡ P).
 Proof. by intros; apply always_intro'. Qed.
 Global Instance and_persistent P Q :
-  PersistentP P → PersistentP Q → PersistentP (P ∧ Q).
-Proof. by intros; rewrite /PersistentP always_and; apply and_mono. Qed.
+  Persistent P → Persistent Q → Persistent (P ∧ Q).
+Proof. by intros; rewrite /Persistent always_and; apply and_mono. Qed.
 Global Instance or_persistent P Q :
-  PersistentP P → PersistentP Q → PersistentP (P ∨ Q).
-Proof. by intros; rewrite /PersistentP always_or; apply or_mono. Qed.
+  Persistent P → Persistent Q → Persistent (P ∨ Q).
+Proof. by intros; rewrite /Persistent always_or; apply or_mono. Qed.
 Global Instance sep_persistent P Q :
-  PersistentP P → PersistentP Q → PersistentP (P ∗ Q).
-Proof. by intros; rewrite /PersistentP always_sep; apply sep_mono. Qed.
+  Persistent P → Persistent Q → Persistent (P ∗ Q).
+Proof. by intros; rewrite /Persistent always_sep; apply sep_mono. Qed.
 Global Instance forall_persistent {A} (Ψ : A → uPred M) :
-  (∀ x, PersistentP (Ψ x)) → PersistentP (∀ x, Ψ x).
-Proof. by intros; rewrite /PersistentP always_forall; apply forall_mono. Qed.
+  (∀ x, Persistent (Ψ x)) → Persistent (∀ x, Ψ x).
+Proof. by intros; rewrite /Persistent always_forall; apply forall_mono. Qed.
 Global Instance exist_persistent {A} (Ψ : A → uPred M) :
-  (∀ x, PersistentP (Ψ x)) → PersistentP (∃ x, Ψ x).
-Proof. by intros; rewrite /PersistentP always_exist; apply exist_mono. Qed.
+  (∀ x, Persistent (Ψ x)) → Persistent (∃ x, Ψ x).
+Proof. by intros; rewrite /Persistent always_exist; apply exist_mono. Qed.
 Global Instance internal_eq_persistent {A : ofeT} (a b : A) :
-  PersistentP (a ≡ b : uPred M)%I.
-Proof. by intros; rewrite /PersistentP always_internal_eq. Qed.
+  Persistent (a ≡ b : uPred M)%I.
+Proof. by intros; rewrite /Persistent always_internal_eq. Qed.
 Global Instance cmra_valid_persistent {A : cmraT} (a : A) :
-  PersistentP (✓ a : uPred M)%I.
-Proof. by intros; rewrite /PersistentP always_cmra_valid. Qed.
-Global Instance later_persistent P : PersistentP P → PersistentP (▷ P).
-Proof. by intros; rewrite /PersistentP always_later; apply later_mono. Qed.
-Global Instance laterN_persistent n P : PersistentP P → PersistentP (▷^n P).
+  Persistent (✓ a : uPred M)%I.
+Proof. by intros; rewrite /Persistent always_cmra_valid. Qed.
+Global Instance later_persistent P : Persistent P → Persistent (▷ P).
+Proof. by intros; rewrite /Persistent always_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 → PersistentP (@uPred_ownM M a).
-Proof. intros. by rewrite /PersistentP always_ownM. Qed.
+Global Instance ownM_persistent : CoreId a → Persistent (@uPred_ownM M a).
+Proof. intros. by rewrite /Persistent always_ownM. Qed.
 Global Instance from_option_persistent {A} P (Ψ : A → uPred M) (mx : option A) :
-  (∀ x, PersistentP (Ψ x)) → PersistentP P → PersistentP (from_option Ψ P mx).
+  (∀ x, Persistent (Ψ x)) → Persistent P → Persistent (from_option Ψ P mx).
 Proof. destruct mx; apply _. Qed.
 
 (* For big ops *)
diff --git a/theories/base_logic/lib/auth.v b/theories/base_logic/lib/auth.v
index ad830d5948086b69ca9f9749b339cc15f623d6b7..adcd5859d32af3cb3546104a78b12ca563529c9c 100644
--- a/theories/base_logic/lib/auth.v
+++ b/theories/base_logic/lib/auth.v
@@ -30,9 +30,9 @@ Section definitions.
   Proof. solve_proper. Qed.
   Global Instance auth_own_proper : Proper ((≡) ==> (⊣⊢)) auth_own.
   Proof. solve_proper. Qed.
-  Global Instance auth_own_timeless a : TimelessP (auth_own a).
+  Global Instance auth_own_timeless a : Timeless (auth_own a).
   Proof. apply _. Qed.
-  Global Instance auth_own_core_id a : CoreId a → PersistentP (auth_own a).
+  Global Instance auth_own_core_id a : CoreId a → Persistent (auth_own a).
   Proof. apply _. Qed.
 
   Global Instance auth_inv_ne n :
@@ -51,7 +51,7 @@ Section definitions.
     Proper (pointwise_relation T (≡) ==>
             pointwise_relation T (⊣⊢) ==> (⊣⊢)) (auth_ctx N).
   Proof. solve_proper. Qed.
-  Global Instance auth_ctx_persistent N f φ : PersistentP (auth_ctx N f φ).
+  Global Instance auth_ctx_persistent N f φ : Persistent (auth_ctx N f φ).
   Proof. apply _. Qed.
 End definitions.
 
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index 8cf543fd6a2afea91678e5bc70108dc236aba1dc..3d7a7ca77bfdd5f43e0ea1773ea9591f52e73bda 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -65,7 +65,7 @@ Proof. solve_contractive. Qed.
 Global Instance slice_proper γ : Proper ((≡) ==> (≡)) (slice N γ).
 Proof. apply ne_proper, _. Qed.
 
-Global Instance slice_persistent γ P : PersistentP (slice N γ P).
+Global Instance slice_persistent γ P : Persistent (slice N γ P).
 Proof. apply _. Qed.
 
 Global Instance box_contractive f : Contractive (box N f).
diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index 83e3629d72766bd9640ffc8fa96ec5f6dbd5c8a2..3a4f1c92bf2e5d982c993bc94005c72697b9f979 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -24,7 +24,7 @@ Instance: Params (@cinv) 5.
 Section proofs.
   Context `{invG Σ, cinvG Σ}.
 
-  Global Instance cinv_own_timeless γ p : TimelessP (cinv_own γ p).
+  Global Instance cinv_own_timeless γ p : Timeless (cinv_own γ p).
   Proof. rewrite /cinv_own; apply _. Qed.
 
   Global Instance cinv_contractive N γ : Contractive (cinv N γ).
@@ -34,7 +34,7 @@ Section proofs.
   Global Instance cinv_proper N γ : Proper ((≡) ==> (≡)) (cinv N γ).
   Proof. exact: ne_proper. Qed.
 
-  Global Instance cinv_persistent N γ P : PersistentP (cinv N γ P).
+  Global Instance cinv_persistent N γ P : Persistent (cinv N γ P).
   Proof. rewrite /cinv; apply _. Qed.
 
   Global Instance cinv_own_fractionnal γ : Fractional (cinv_own γ).
diff --git a/theories/base_logic/lib/core.v b/theories/base_logic/lib/core.v
index f96e6edf2baa7848d6863ac9d8abd4121be1c930..e6d584217ca120eb903dcc557cd024f17b7b7f14 100644
--- a/theories/base_logic/lib/core.v
+++ b/theories/base_logic/lib/core.v
@@ -15,7 +15,7 @@ Import uPred.
 *)
 
 Definition coreP {M : ucmraT} (P : uPred M) : uPred M :=
-  (∀ `(!PersistentP Q), ⌜P ⊢ Q⌝ → Q)%I.
+  (∀ `(!Persistent Q), ⌜P ⊢ Q⌝ → Q)%I.
 Instance: Params (@coreP) 1.
 Typeclasses Opaque coreP.
 
@@ -26,7 +26,7 @@ Section core.
   Lemma coreP_intro P : P -∗ coreP P.
   Proof. rewrite /coreP. iIntros "HP". by iIntros (Q HQ ->). Qed.
 
-  Global Instance coreP_persistent P : PersistentP (coreP P).
+  Global Instance coreP_persistent P : Persistent (coreP P).
   Proof. rewrite /coreP. apply _. Qed.
 
   Global Instance coreP_mono : Proper ((⊢) ==> (⊢)) (@coreP M).
@@ -38,7 +38,7 @@ Section core.
   Global Instance coreP_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@coreP M).
   Proof. intros P Q. rewrite !equiv_spec=>-[??]. by split; apply coreP_mono. Qed.
 
-  Lemma coreP_elim P : PersistentP P → coreP P -∗ P.
+  Lemma coreP_elim P : Persistent P → coreP P -∗ P.
   Proof. rewrite /coreP. iIntros (?) "HCP". unshelve iApply ("HCP" $! P); auto. Qed.
 
   Lemma coreP_wand P Q :
diff --git a/theories/base_logic/lib/counter_examples.v b/theories/base_logic/lib/counter_examples.v
index d9f02cf5bec7003bbec19138ab250dc564968cdc..259eb66d28c31118b991225c71cdee14b0be16e1 100644
--- a/theories/base_logic/lib/counter_examples.v
+++ b/theories/base_logic/lib/counter_examples.v
@@ -12,7 +12,7 @@ Module savedprop. Section savedprop.
 
   (** Saved Propositions and the update modality *)
   Context (sprop : Type) (saved : sprop → iProp → iProp).
-  Hypothesis sprop_persistent : ∀ i P, PersistentP (saved i P).
+  Hypothesis sprop_persistent : ∀ i P, Persistent (saved i P).
   Hypothesis sprop_alloc_dep :
     ∀ (P : sprop → iProp), (|==> (∃ i, saved i (P i)))%I.
   Hypothesis sprop_agree : ∀ i P Q, saved i P ∧ saved i Q ⊢ □ (P ↔ Q).
@@ -69,7 +69,7 @@ Module inv. Section inv.
 
   (** We have invariants *)
   Context (name : Type) (inv : name → iProp → iProp).
-  Hypothesis inv_persistent : ∀ i P, PersistentP (inv i P).
+  Hypothesis inv_persistent : ∀ i P, Persistent (inv i P).
   Hypothesis inv_alloc : ∀ P, P ⊢ fupd M1 (∃ i, inv i P).
   Hypothesis inv_open :
     ∀ i P Q R, (P ∗ Q ⊢ fupd M0 (P ∗ R)) → (inv i P ∗ Q ⊢ fupd M1 R).
@@ -132,7 +132,7 @@ Module inv. Section inv.
   (** Now to the actual counterexample. We start with a weird form of saved propositions. *)
   Definition saved (γ : gname) (P : iProp) : iProp :=
     ∃ i, inv i (start γ ∨ (finished γ ∗ □ P)).
-  Global Instance saved_persistent γ P : PersistentP (saved γ P) := _.
+  Global Instance saved_persistent γ P : Persistent (saved γ P) := _.
 
   Lemma saved_alloc (P : gname → iProp) : fupd M1 (∃ γ, saved γ (P γ)).
   Proof.
@@ -165,7 +165,7 @@ Module inv. Section inv.
   (** And now we tie a bad knot. *)
   Notation "¬ P" := (□ (P -∗ fupd M1 False))%I : uPred_scope.
   Definition A i : iProp := ∃ P, ¬P ∗ saved i P.
-  Global Instance A_persistent i : PersistentP (A i) := _.
+  Global Instance A_persistent i : Persistent (A i) := _.
 
   Lemma A_alloc : fupd M1 (∃ i, saved i (A i)).
   Proof. by apply saved_alloc. Qed.
diff --git a/theories/base_logic/lib/fancy_updates_from_vs.v b/theories/base_logic/lib/fancy_updates_from_vs.v
index fc505d702d42d078b694c975f12bee859205abb2..5e6bb63a35348fcbd87b03fe2d1a80e5bff65da9 100644
--- a/theories/base_logic/lib/fancy_updates_from_vs.v
+++ b/theories/base_logic/lib/fancy_updates_from_vs.v
@@ -13,7 +13,7 @@ Notation "P ={ E1 , E2 }=> Q" := (vs E1 E2 P Q)
    format "P  ={ E1 , E2 }=>  Q") : uPred_scope.
 
 Context (vs_ne : ∀ E1 E2, NonExpansive2 (vs E1 E2)).
-Context (vs_persistent : ∀ E1 E2 P Q, PersistentP (P ={E1,E2}=> Q)).
+Context (vs_persistent : ∀ E1 E2 P Q, Persistent (P ={E1,E2}=> Q)).
 
 Context (vs_impl : ∀ E P Q, □ (P → Q) ⊢ P ={E,E}=> Q).
 Context (vs_transitive : ∀ E1 E2 E3 P Q R,
@@ -24,7 +24,7 @@ Context (vs_frame_r : ∀ E1 E2 P Q R, (P ={E1,E2}=> Q) ⊢ P ∗ R ={E1,E2}=> Q
 Context (vs_exists : ∀ {A} E1 E2 (Φ : A → uPred M) Q,
   (∀ x, Φ x ={E1,E2}=> Q) ⊢ (∃ x, Φ x) ={E1,E2}=> Q).
 Context (vs_persistent_intro_r : ∀ E1 E2 P Q R,
-  PersistentP R →
+  Persistent R →
   (R -∗ (P ={E1,E2}=> Q)) ⊢ P ∗ R ={E1,E2}=> Q).
 
 Definition fupd (E1 E2 : coPset) (P : uPred M) : uPred M :=
diff --git a/theories/base_logic/lib/fractional.v b/theories/base_logic/lib/fractional.v
index a94ea6989ed1ee7caf9790a6215928d8e3c639f7..25956794de7388f946352e96b32d970e5db229e2 100644
--- a/theories/base_logic/lib/fractional.v
+++ b/theories/base_logic/lib/fractional.v
@@ -50,7 +50,7 @@ Section fractional.
 
   (** Fractional and logical connectives *)
   Global Instance persistent_fractional P :
-    PersistentP P → Fractional (λ _, P).
+    Persistent P → Fractional (λ _, P).
   Proof. intros HP q q'. by apply uPred.always_sep_dup. Qed.
 
   Global Instance fractional_sep Φ Ψ :
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 89914dc635f5dbd3fd2bf3e94a2c61cae981e9ae..2f27f2965702e536f18326ca77b9a1b208d5a944 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -82,7 +82,7 @@ Section gen_heap.
   Implicit Types v : V.
 
   (** General properties of mapsto *)
-  Global Instance mapsto_timeless l q v : TimelessP (l ↦{q} v).
+  Global Instance mapsto_timeless l q v : Timeless (l ↦{q} v).
   Proof. rewrite mapsto_eq /mapsto_def. apply _. Qed.
   Global Instance mapsto_fractional l v : Fractional (λ q, l ↦{q} v)%I.
   Proof.
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index 467d60e224c5a82d5a0d5f02b635015bb8f73fde..1608c9a29e941181ae9db80c95ecf686113466dd 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -31,7 +31,7 @@ Proof. apply contractive_ne, _. Qed.
 Global Instance inv_Proper N : Proper ((⊣⊢) ==> (⊣⊢)) (inv N).
 Proof. apply ne_proper, _. Qed.
 
-Global Instance inv_persistent N P : PersistentP (inv N P).
+Global Instance inv_persistent N P : Persistent (inv N P).
 Proof. rewrite inv_eq /inv; apply _. Qed.
 
 Lemma fresh_inv_name (E : gset positive) N : ∃ i, i ∉ E ∧ i ∈ (↑N:coPset).
@@ -81,7 +81,7 @@ Proof.
   iIntros "HP [Hw $] !> !>". iApply ownI_close; by iFrame.
 Qed.
 
-Lemma inv_open_timeless E N P `{!TimelessP P} :
+Lemma inv_open_timeless E N P `{!Timeless P} :
   ↑N ⊆ E → inv N P ={E,E∖↑N}=∗ P ∗ (P ={E∖↑N,E}=∗ True).
 Proof.
   iIntros (?) "Hinv". iMod (inv_open with "Hinv") as "[>HP Hclose]"; auto.
diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index 2f20a514e2d7996ba685afc4e3af319c62b73422..385d17e64204d2e551b008ef10ae09e55a920c9a 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -32,7 +32,7 @@ Typeclasses Opaque na_own na_inv.
 Section proofs.
   Context `{invG Σ, na_invG Σ}.
 
-  Global Instance na_own_timeless p E : TimelessP (na_own p E).
+  Global Instance na_own_timeless p E : Timeless (na_own p E).
   Proof. rewrite /na_own; apply _. Qed.
 
   Global Instance na_inv_ne p N : NonExpansive (na_inv p N).
@@ -40,7 +40,7 @@ Section proofs.
   Global Instance na_inv_proper p N : Proper ((≡) ==> (≡)) (na_inv p N).
   Proof. apply (ne_proper _). Qed.
 
-  Global Instance na_inv_persistent p N P : PersistentP (na_inv p N P).
+  Global Instance na_inv_persistent p N P : Persistent (na_inv p N P).
   Proof. rewrite /na_inv; apply _. Qed.
 
   Lemma na_alloc : (|==> ∃ p, na_own p ⊤)%I.
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index 6067d9b772294745cb9cecf922553d317872fbe6..89bbf7833747f3e1cb595c76a5897560a9ae5f40 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -106,9 +106,9 @@ Proof. apply: uPred.always_entails_r. apply own_valid. Qed.
 Lemma own_valid_l γ a : own γ a ⊢ ✓ a ∗ own γ a.
 Proof. by rewrite comm -own_valid_r. Qed.
 
-Global Instance own_timeless γ a : Discrete a → TimelessP (own γ a).
+Global Instance own_timeless γ a : Discrete a → Timeless (own γ a).
 Proof. rewrite !own_eq /own_def; apply _. Qed.
-Global Instance own_core_persistent γ a : CoreId a → PersistentP (own γ a).
+Global Instance own_core_persistent γ a : CoreId a → Persistent (own γ a).
 Proof. rewrite !own_eq /own_def; apply _. Qed.
 
 (** ** Allocation *)
diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index 4002d1d821aedea8544a46a4bf9a2b83ba274531..4ce4a3ce2da7b3035353289cb0f9c695387c628c 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -23,7 +23,7 @@ Section saved_prop.
   Implicit Types x y : F (iProp Σ).
   Implicit Types γ : gname.
 
-  Global Instance saved_prop_persistent γ x : PersistentP (saved_prop_own γ x).
+  Global Instance saved_prop_persistent γ x : Persistent (saved_prop_own γ x).
   Proof. rewrite /saved_prop_own; apply _. Qed.
 
   Lemma saved_prop_alloc_strong x (G : gset gname) :
diff --git a/theories/base_logic/lib/sts.v b/theories/base_logic/lib/sts.v
index 047d10d32b0ebab956aa04ea9138683e9be6deb8..9effaf4d7c82c8a31163b9075fb40e2d83d752a2 100644
--- a/theories/base_logic/lib/sts.v
+++ b/theories/base_logic/lib/sts.v
@@ -43,11 +43,11 @@ Section definitions.
   Global Instance sts_ctx_proper `{!invG Σ} N :
     Proper (pointwise_relation _ (≡) ==> (⊣⊢)) (sts_ctx N).
   Proof. solve_proper. Qed.
-  Global Instance sts_ctx_persistent `{!invG Σ} N φ : PersistentP (sts_ctx N φ).
+  Global Instance sts_ctx_persistent `{!invG Σ} N φ : Persistent (sts_ctx N φ).
   Proof. apply _. Qed.
-  Global Instance sts_own_persistent s : PersistentP (sts_own s ∅).
+  Global Instance sts_own_persistent s : Persistent (sts_own s ∅).
   Proof. apply _. Qed.
-  Global Instance sts_ownS_persistent S : PersistentP (sts_ownS S ∅).
+  Global Instance sts_ownS_persistent S : Persistent (sts_ownS S ∅).
   Proof. apply _. Qed.
 End definitions.
 
diff --git a/theories/base_logic/lib/viewshifts.v b/theories/base_logic/lib/viewshifts.v
index a4dd554853d18885448c34a163bdf11f3adbb836..490ce88166aae344696c038a060de0c92aa9c9e3 100644
--- a/theories/base_logic/lib/viewshifts.v
+++ b/theories/base_logic/lib/viewshifts.v
@@ -41,7 +41,7 @@ Proof. solve_proper. Qed.
 
 Lemma vs_false_elim E1 E2 P : False ={E1,E2}=> P.
 Proof. iIntros "!# []". Qed.
-Lemma vs_timeless E P : TimelessP P → ▷ P ={E}=> P.
+Lemma vs_timeless E P : Timeless P → ▷ P ={E}=> P.
 Proof. by iIntros (?) "!# > ?". Qed.
 
 Lemma vs_transitive E1 E2 E3 P Q R :
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index b270879e1d0dcf8b1bcb8764d981c7734b8f53c1..4a0fa26984a6b9a7f5dad445d1604319b409fe1d 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -49,7 +49,7 @@ Instance invariant_unfold_contractive : Contractive (@invariant_unfold Σ).
 Proof. solve_contractive. Qed.
 Global Instance ownI_contractive i : Contractive (@ownI Σ _ i).
 Proof. solve_contractive. Qed.
-Global Instance ownI_persistent i P : PersistentP (ownI i P).
+Global Instance ownI_persistent i P : Persistent (ownI i P).
 Proof. rewrite /ownI. apply _. Qed.
 
 Lemma ownE_empty : (|==> ownE ∅)%I.
diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index 79112c3fa39170854b808dce42c4a1716a7219fd..b9632c00c56c77d877d82dc6294721e44be25a74 100644
--- a/theories/heap_lang/lib/counter.v
+++ b/theories/heap_lang/lib/counter.v
@@ -29,7 +29,7 @@ Section mono_proof.
     (∃ γ, inv N (mcounter_inv γ l) ∧ own γ (◯ (n : mnat)))%I.
 
   (** The main proofs. *)
-  Global Instance mcounter_persistent l n : PersistentP (mcounter l n).
+  Global Instance mcounter_persistent l n : Persistent (mcounter l n).
   Proof. apply _. Qed.
 
   Lemma newcounter_mono_spec :
diff --git a/theories/heap_lang/lib/lock.v b/theories/heap_lang/lib/lock.v
index 720dcc19aa4af6c4696ed456ae0167c6f797ac7d..a5d9966a25060e0ffdd20dc6bc361e9bf7ee8dae 100644
--- a/theories/heap_lang/lib/lock.v
+++ b/theories/heap_lang/lib/lock.v
@@ -14,8 +14,8 @@ Structure lock Σ `{!heapG Σ} := Lock {
   locked (γ: name) : iProp Σ;
   (* -- general properties -- *)
   is_lock_ne N γ lk : NonExpansive (is_lock N γ lk);
-  is_lock_persistent N γ lk R : PersistentP (is_lock N γ lk R);
-  locked_timeless γ : TimelessP (locked γ);
+  is_lock_persistent N γ lk R : Persistent (is_lock N γ lk R);
+  locked_timeless γ : Timeless (locked γ);
   locked_exclusive γ : locked γ -∗ locked γ -∗ False;
   (* -- operation specs -- *)
   newlock_spec N (R : iProp Σ) :
diff --git a/theories/heap_lang/lib/spin_lock.v b/theories/heap_lang/lib/spin_lock.v
index 007093dcda47bc7964077053434878a8f7799346..9abf0f6e7eff8755d4e0e5451fcc718090cb05a4 100644
--- a/theories/heap_lang/lib/spin_lock.v
+++ b/theories/heap_lang/lib/spin_lock.v
@@ -40,9 +40,9 @@ Section proof.
   Proof. solve_proper. Qed.
 
   (** The main proofs. *)
-  Global Instance is_lock_persistent γ l R : PersistentP (is_lock γ l R).
+  Global Instance is_lock_persistent γ l R : Persistent (is_lock γ l R).
   Proof. apply _. Qed.
-  Global Instance locked_timeless γ : TimelessP (locked γ).
+  Global Instance locked_timeless γ : Timeless (locked γ).
   Proof. apply _. Qed.
 
   Lemma newlock_spec (R : iProp Σ):
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index b5c0b7350e8c409bd972feace1b3113a0a3b771e..4d4d6cba841cbfb687b454444cb7562615f96ab7 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -59,9 +59,9 @@ Section proof.
   Proof. solve_proper. Qed.
   Global Instance is_lock_ne γ lk : NonExpansive (is_lock γ lk).
   Proof. solve_proper. Qed.
-  Global Instance is_lock_persistent γ lk R : PersistentP (is_lock γ lk R).
+  Global Instance is_lock_persistent γ lk R : Persistent (is_lock γ lk R).
   Proof. apply _. Qed.
-  Global Instance locked_timeless γ : TimelessP (locked γ).
+  Global Instance locked_timeless γ : Timeless (locked γ).
   Proof. apply _. Qed.
 
   Lemma locked_exclusive (γ : gname) : locked γ -∗ locked γ -∗ False.
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index f57fd0442c2b5b535a7b7656a22631ead9594720..1c3a8d3e34439ae1684659138937e0dd672729dd 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -75,7 +75,7 @@ Section lifting.
 
   Lemma ownP_twice σ1 σ2 : ownP σ1 ∗ ownP σ2 ⊢ False.
   Proof. rewrite /ownP -own_op own_valid. by iIntros (?). Qed.
-  Global Instance ownP_timeless σ : TimelessP (@ownP (state Λ) Σ _ σ).
+  Global Instance ownP_timeless σ : Timeless (@ownP (state Λ) Σ _ σ).
   Proof. rewrite /ownP; apply _. Qed.
 
   Lemma ownP_lift_step E Φ e1 :
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 50827dbea2aeff584174869f28cfd725e4a707d3..ba0c288c0695dc07731767e90733c8ac8a0a61a8 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -139,14 +139,14 @@ Proof.
   rewrite -Hx. apply pure_intro. done.
 Qed.
 
-(* IntoPersistentP *)
-Global Instance into_persistentP_always_trans p P Q :
-  IntoPersistentP true P Q → IntoPersistentP p (□ P) Q | 0.
-Proof. rewrite /IntoPersistentP /==> ->. by rewrite always_if_always. Qed.
-Global Instance into_persistentP_always P : IntoPersistentP true P P | 1.
+(* IntoPersistent *)
+Global Instance into_persistent_always_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. done. Qed.
-Global Instance into_persistentP_persistent P :
-  PersistentP P → IntoPersistentP false P P | 100.
+Global Instance into_persistent_persistent P :
+  Persistent P → IntoPersistent false P P | 100.
 Proof. done. Qed.
 
 (* IntoLater *)
@@ -339,10 +339,10 @@ Proof. by apply mk_from_and_and. Qed.
 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 :
-  PersistentP P1 → FromAnd true (P1 ∗ P2) P1 P2 | 9.
+  Persistent P1 → FromAnd true (P1 ∗ P2) P1 P2 | 9.
 Proof. intros. by rewrite /FromAnd always_and_sep_l. Qed.
 Global Instance from_and_sep_persistent_r P1 P2 :
-  PersistentP P2 → FromAnd true (P1 ∗ P2) P1 P2 | 10.
+  Persistent P2 → FromAnd true (P1 ∗ P2) P1 P2 | 10.
 Proof. intros. by rewrite /FromAnd always_and_sep_r. Qed.
 
 Global Instance from_and_pure p φ ψ : @FromAnd M p ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
@@ -385,7 +385,7 @@ Global Instance from_and_big_sepL_cons {A} (Φ : nat → A → uPred M) x l :
   FromAnd false ([∗ list] k ↦ y ∈ x :: l, Φ k y) (Φ 0 x) ([∗ list] k ↦ y ∈ l, Φ (S k) y).
 Proof. by rewrite /FromAnd big_sepL_cons. Qed.
 Global Instance from_and_big_sepL_cons_persistent {A} (Φ : nat → A → uPred M) x l :
-  PersistentP (Φ 0 x) →
+  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.
 
@@ -394,7 +394,7 @@ Global Instance from_and_big_sepL_app {A} (Φ : nat → A → uPred M) l1 l2 :
     ([∗ list] k ↦ y ∈ l1, Φ k y) ([∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y).
 Proof. by rewrite /FromAnd big_opL_app. Qed.
 Global Instance from_sep_big_sepL_app_persistent {A} (Φ : nat → A → uPred M) l1 l2 :
-  (∀ k y, PersistentP (Φ k y)) →
+  (∀ 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.
@@ -430,10 +430,10 @@ Proof. intros. apply mk_into_and_sep. by rewrite (is_op a) ownM_op. Qed.
 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 :
-  PersistentP P → IntoAnd false (P ∧ Q) P Q.
+  Persistent P → IntoAnd false (P ∧ Q) P Q.
 Proof. intros; by rewrite /IntoAnd /= always_and_sep_l. Qed.
 Global Instance into_and_and_persistent_r P Q :
-  PersistentP Q → IntoAnd false (P ∧ Q) P Q.
+  Persistent Q → IntoAnd false (P ∧ Q) P Q.
 Proof. intros; by rewrite /IntoAnd /= always_and_sep_r. Qed.
 
 Global Instance into_and_pure p φ ψ : @IntoAnd M p ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
@@ -783,13 +783,13 @@ Proof.
   by rewrite -except_0_sep wand_elim_r.
 Qed.
 Global Instance elim_modal_timeless_bupd P Q :
-  TimelessP P → IsExcept0 Q → ElimModal (▷ P) P Q Q.
+  Timeless P → IsExcept0 Q → ElimModal (▷ P) P Q Q.
 Proof.
   intros. rewrite /ElimModal (except_0_intro (_ -∗ _)) (timelessP P).
   by rewrite -except_0_sep wand_elim_r.
 Qed.
 Global Instance elim_modal_timeless_bupd' p P Q :
-  TimelessP P → IsExcept0 Q → ElimModal (▷?p P) P Q Q.
+  Timeless P → IsExcept0 Q → ElimModal (▷?p P) P Q Q.
 Proof.
   destruct p; simpl; auto using elim_modal_timeless_bupd.
   intros _ _. by rewrite /ElimModal wand_elim_r.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index caaa47f1784ba14068ee09c3031b249abaaaeb51..66e68407c2b6f12ebb5173a258da19389c44f2f1 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -54,10 +54,10 @@ Class FromPure {M} (P : uPred M) (φ : Prop) := from_pure : ⌜φ⌝ ⊢ P.
 Arguments from_pure {_} _ _ {_}.
 Hint Mode FromPure + ! - : typeclass_instances.
 
-Class IntoPersistentP {M} (p : bool) (P Q : uPred M) :=
-  into_persistentP : □?p P ⊢ □ Q.
-Arguments into_persistentP {_} _ _ _ {_}.
-Hint Mode IntoPersistentP + + ! - : typeclass_instances.
+Class IntoPersistent {M} (p : bool) (P Q : uPred M) :=
+  into_persistent : □?p P ⊢ □ Q.
+Arguments into_persistent {_} _ _ _ {_}.
+Hint Mode IntoPersistent + + ! - : typeclass_instances.
 
 (* The class [IntoLaterN] has only two instances:
 
@@ -122,7 +122,7 @@ Lemma mk_from_and_and {M} p (P Q1 Q2 : uPred M) :
   (Q1 ∧ Q2 ⊢ P) → FromAnd p P Q1 Q2.
 Proof. rewrite /FromAnd=><-. destruct p; auto using sep_and. Qed.
 Lemma mk_from_and_persistent {M} (P Q1 Q2 : uPred M) :
-  Or (PersistentP Q1) (PersistentP Q2) → (Q1 ∗ Q2 ⊢ P) → FromAnd true P Q1 Q2.
+  Or (Persistent Q1) (Persistent Q2) → (Q1 ∗ Q2 ⊢ P) → FromAnd true P Q1 Q2.
 Proof.
   intros [?|?] ?; rewrite /FromAnd.
   - by rewrite always_and_sep_l.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 50643dd05bb32f515983ff54e1e61a3fa1e245a8..a674e9465b56d47c5a9aa341eb9c37d851e5a41b 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -302,7 +302,7 @@ Proof.
 Qed.
 
 Lemma env_spatial_is_nil_persistent Δ :
-  env_spatial_is_nil Δ = true → PersistentP Δ.
+  env_spatial_is_nil Δ = true → Persistent Δ.
 Proof. intros; destruct Δ as [? []]; simplify_eq/=; apply _. Qed.
 Hint Immediate env_spatial_is_nil_persistent : typeclass_instances.
 
@@ -483,33 +483,33 @@ Qed.
 
 Lemma tac_persistent Δ Δ' i p P P' Q :
   envs_lookup i Δ = Some (p, P) →
-  IntoPersistentP p P P' →
+  IntoPersistent p P P' →
   envs_replace i p true (Esnoc Enil i P') Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros ? HP ? <-. rewrite envs_replace_sound //; simpl.
-  by rewrite right_id (into_persistentP _ P) wand_elim_r.
+  by rewrite right_id (into_persistent _ P) wand_elim_r.
 Qed.
 
 (** * Implication and wand *)
 Lemma tac_impl_intro Δ Δ' i P Q :
-  (if env_spatial_is_nil Δ then TCTrue else PersistentP P) →
+  (if env_spatial_is_nil Δ then TCTrue else Persistent P) →
   envs_app false (Esnoc Enil i P) Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ P → Q.
 Proof.
   intros ?? <-. destruct (env_spatial_is_nil Δ) eqn:?.
-  - rewrite (persistentP Δ) envs_app_sound //; simpl.
+  - rewrite (persistent Δ) envs_app_sound //; simpl.
     by rewrite right_id always_wand_impl always_elim.
   - apply impl_intro_l. rewrite envs_app_sound //; simpl.
     by rewrite always_and_sep_l right_id wand_elim_r.
 Qed.
 Lemma tac_impl_intro_persistent Δ Δ' i P P' Q :
-  IntoPersistentP false P P' →
+  IntoPersistent false P P' →
   envs_app true (Esnoc Enil i P') Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ P → Q.
 Proof.
   intros ?? HQ. rewrite envs_app_sound //=; simpl. apply impl_intro_l.
-  rewrite (_ : P = â–¡?false P) // (into_persistentP false P).
+  rewrite (_ : P = â–¡?false P) // (into_persistent false P).
   by rewrite right_id always_and_sep_l wand_elim_r.
 Qed.
 
@@ -522,7 +522,7 @@ Proof.
   intros ? HQ. rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
 Qed.
 Lemma tac_wand_intro_persistent Δ Δ' i P P' Q :
-  IntoPersistentP false P P' →
+  IntoPersistent false P P' →
   envs_app true (Esnoc Enil i P') Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ P -∗ Q.
 Proof.
@@ -608,14 +608,14 @@ Qed.
 
 Lemma tac_specialize_assert_persistent Δ Δ' Δ'' j q P1 P2 R Q :
   envs_lookup_delete j Δ = Some (q, R, Δ') →
-  IntoWand false R P1 P2 → PersistentP P1 →
+  IntoWand false R P1 P2 → Persistent P1 →
   envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'' →
   (Δ' ⊢ P1) → (Δ'' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros [? ->]%envs_lookup_delete_Some ??? HP1 <-.
   rewrite envs_lookup_sound //.
   rewrite -(idemp uPred_and (envs_delete _ _ _)).
-  rewrite {1}HP1 (persistentP P1) always_and_sep_l assoc.
+  rewrite {1}HP1 (persistent P1) always_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.
   by rewrite wand_elim_r.
@@ -623,7 +623,7 @@ Qed.
 
 Lemma tac_specialize_persistent_helper Δ Δ' j q P R Q :
   envs_lookup j Δ = Some (q,P) →
-  (Δ ⊢ R) → PersistentP R →
+  (Δ ⊢ R) → Persistent R →
   envs_replace j q true (Esnoc Enil j R) Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
@@ -659,7 +659,7 @@ Lemma tac_revert_ih Δ P Q {φ : Prop} (Hφ : φ) :
   (of_envs Δ ⊢ Q).
 Proof.
   rewrite /IntoIH. intros HP ? HPQ.
-  by rewrite -(idemp uPred_and Δ) {1}(persistentP Δ) {1}HP // HPQ impl_elim_r.
+  by rewrite -(idemp uPred_and Δ) {1}(persistent Δ) {1}HP // HPQ impl_elim_r.
 Qed.
 
 Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P P' Q :
@@ -676,7 +676,7 @@ Qed.
 Lemma tac_assert_persistent Δ Δ1 Δ2 Δ' lr js j P Q :
   envs_split lr js Δ = Some (Δ1,Δ2) →
   envs_app false (Esnoc Enil j P) Δ = Some Δ' →
-  PersistentP P →
+  Persistent P →
   (Δ1 ⊢ P) → (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros ??? HP <-. rewrite -(idemp uPred_and Δ) {1}envs_split_sound //.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 5295e6dba1d5c212bbf04e5c42e8d4658cf09a9d..df997893a4b8faf46d52cb25c65f63ff94a07338 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -166,7 +166,7 @@ Local Tactic Notation "iPersistent" constr(H) :=
   eapply tac_persistent with _ H _ _ _; (* (i:=H) *)
     [env_reflexivity || fail "iPersistent:" H "not found"
     |apply _ ||
-     let Q := match goal with |- IntoPersistentP _ ?Q _ => Q end in
+     let Q := match goal with |- IntoPersistent _ ?Q _ => Q end in
      fail "iPersistent:" Q "not persistent"
     |env_reflexivity|].
 
@@ -300,7 +300,7 @@ Local Tactic Notation "iIntro" constr(H) :=
   [ (* (?Q → _) *)
     eapply tac_impl_intro with _ H; (* (i:=H) *)
       [env_cbv; apply _ ||
-       let P := lazymatch goal with |- PersistentP ?P => P end in
+       let P := lazymatch goal with |- Persistent ?P => P end in
        fail 1 "iIntro: introducing non-persistent" H ":" P
               "into non-empty spatial context"
       |env_reflexivity || fail "iIntro:" H "not fresh"
@@ -317,14 +317,14 @@ Local Tactic Notation "iIntro" "#" constr(H) :=
   [ (* (?P → _) *)
     eapply tac_impl_intro_persistent with _ H _; (* (i:=H) *)
       [apply _ || 
-       let P := match goal with |- IntoPersistentP _ ?P _ => P end in
+       let P := match goal with |- IntoPersistent _ ?P _ => P end in
        fail 1 "iIntro: " P " not persistent"
       |env_reflexivity || fail 1 "iIntro:" H "not fresh"
       |]
   | (* (?P -∗ _) *)
     eapply tac_wand_intro_persistent with _ H _; (* (i:=H) *)
       [apply _ || 
-       let P := match goal with |- IntoPersistentP _ ?P _ => P end in
+       let P := match goal with |- IntoPersistent _ ?P _ => P end in
        fail 1 "iIntro: " P " not persistent"
       |env_reflexivity || fail 1 "iIntro:" H "not fresh"
       |]
@@ -426,7 +426,7 @@ Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
          [env_reflexivity || fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
          |apply _ ||
-          let Q := match goal with |- PersistentP ?Q => Q end in
+          let Q := match goal with |- Persistent ?Q => Q end in
           fail "iSpecialize:" Q "not persistent"
          |env_reflexivity
          |iFrame Hs_frame; done_if d (*goal*)
@@ -452,7 +452,7 @@ Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
          [env_reflexivity || fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
          |apply _ ||
-          let Q := match goal with |- PersistentP ?Q => Q end in
+          let Q := match goal with |- Persistent ?Q => Q end in
           fail "iSpecialize:" Q "not persistent"
          |env_reflexivity
          |solve [iFrame "∗ #"]
@@ -501,7 +501,7 @@ Tactic Notation "iSpecializeCore" open_constr(t) "as" constr(p) :=
            [env_reflexivity || fail "iSpecialize:" H "not found"
            |iSpecializeArgs H xs; iSpecializePat H pat; last (iExact H)
            |apply _ ||
-            let Q := match goal with |- PersistentP ?Q => Q end in
+            let Q := match goal with |- Persistent ?Q => Q end in
             fail "iSpecialize:" Q "not persistent"
            |env_reflexivity|(* goal *)]
       | false => iSpecializeArgs H xs; iSpecializePat H pat
diff --git a/theories/tests/ipm_paper.v b/theories/tests/ipm_paper.v
index 604f05d26f2dfe417a9c42a43e93c0e60414df92..5fedc7f4cd2cf9a618b7c9d938dcbdbcd2920b3f 100644
--- a/theories/tests/ipm_paper.v
+++ b/theories/tests/ipm_paper.v
@@ -191,7 +191,7 @@ Section counter_proof.
     (∃ N γ, inv N (I γ l) ∧ own γ (Frag n))%I.
 
   (** The main proofs. *)
-  Global Instance C_persistent l n : PersistentP (C l n).
+  Global Instance C_persistent l n : Persistent (C l n).
   Proof. apply _. Qed.
 
   Lemma newcounter_spec :
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index ef633861b4fc3517ad8df26f5369faa4a70cd740..96ceba7824627eec12c63470b98d9e97f7be7473 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -78,7 +78,7 @@ Proof.
   done.
 Qed.
 
-Lemma test_iIntros_persistent P Q `{!PersistentP Q} : (P → Q → P ∗ Q)%I.
+Lemma test_iIntros_persistent P Q `{!Persistent Q} : (P → Q → P ∗ Q)%I.
 Proof. iIntros "H1 H2". by iFrame. Qed.
 
 Lemma test_iIntros_pure (ψ φ : Prop) P : ψ → (⌜ φ ⌝ → P → ⌜ φ ∧ ψ ⌝ ∧ P)%I.
@@ -142,11 +142,11 @@ Proof.
   iSpecialize ("H" $! _ [#10]). done.
 Qed.
 
-Lemma test_eauto_iFramE P Q R `{!PersistentP R} :
+Lemma test_eauto_iFramE P Q R `{!Persistent R} :
   P -∗ Q -∗ R -∗ R ∗ Q ∗ P ∗ R ∨ False.
 Proof. eauto with iFrame. Qed.
 
-Lemma test_iCombine_persistent P Q R `{!PersistentP R} :
+Lemma test_iCombine_persistent P Q R `{!Persistent R} :
   P -∗ Q -∗ R -∗ R ∗ Q ∗ P ∗ R ∨ False.
 Proof. iIntros "HP HQ #HR". iCombine "HR HQ HP HR" as "H". auto. Qed.