From 655cbe71ecc07ff00a59c391ab63204a416c9dfa Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 24 Oct 2017 14:10:28 +0200
Subject: [PATCH] Unify plain and persistent modality.

This way, we do not have to duplicate a lot of theory, and we made sure
that we have all lemmas/class instances for both modalities.
---
 theories/base_logic/big_op.v                  |  38 +-
 theories/base_logic/derived.v                 | 447 ++++++------------
 theories/base_logic/lib/auth.v                |   5 +-
 theories/base_logic/lib/boxes.v               |   2 +-
 .../base_logic/lib/cancelable_invariants.v    |   2 +-
 theories/base_logic/lib/core.v                |  12 +-
 theories/base_logic/lib/counter_examples.v    |   8 +-
 theories/base_logic/lib/fancy_updates.v       |  12 +-
 .../base_logic/lib/fancy_updates_from_vs.v    |   4 +-
 theories/base_logic/lib/fractional.v          |   2 +-
 theories/base_logic/lib/invariants.v          |   2 +-
 theories/base_logic/lib/na_invariants.v       |   2 +-
 theories/base_logic/lib/own.v                 |   2 +-
 theories/base_logic/lib/saved_prop.v          |   3 +-
 theories/base_logic/lib/sts.v                 |   6 +-
 theories/base_logic/lib/wsat.v                |   2 +-
 theories/base_logic/primitive.v               | 112 ++---
 theories/heap_lang/lib/counter.v              |   2 +-
 theories/heap_lang/lib/lock.v                 |   2 +-
 theories/heap_lang/lib/spin_lock.v            |   2 +-
 theories/heap_lang/lib/ticket_lock.v          |   2 +-
 theories/program_logic/adequacy.v             |   4 +-
 theories/proofmode/class_instances.v          | 118 ++---
 theories/proofmode/classes.v                  |   8 +-
 theories/proofmode/coq_tactics.v              |  73 ++-
 theories/proofmode/tactics.v                  |   9 +-
 theories/tests/ipm_paper.v                    |   2 +-
 theories/tests/proofmode.v                    |   6 +-
 28 files changed, 333 insertions(+), 556 deletions(-)

diff --git a/theories/base_logic/big_op.v b/theories/base_logic/big_op.v
index 9b9daea32..5eac49b7c 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, PersistentP true (Φ k x)) →
     ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ (∀ k x, ⌜l !! k = Some x⌝ → Φ k x).
   Proof.
     intros HΦ. apply (anti_symm _).
@@ -149,14 +149,14 @@ Section list.
     by rewrite -always_wand_impl always_elim wand_elim_l.
   Qed.
 
-  Global Instance big_sepL_nil_persistent Φ :
-    PersistentP ([∗ list] k↦x ∈ [], Φ k x).
+  Global Instance big_sepL_nil_persistent c Φ :
+    PersistentP c ([∗ 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).
+  Global Instance big_sepL_persistent c Φ l :
+    (∀ k x, PersistentP c (Φ k x)) → PersistentP c ([∗ 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).
+  Global Instance big_sepL_persistent_id c Ps :
+    TCForall (PersistentP c) Ps → PersistentP c ([∗] Ps).
   Proof. induction 1; simpl; apply _. Qed.
 
   Global Instance big_sepL_nil_timeless Φ :
@@ -316,7 +316,7 @@ Section gmap.
   Proof. apply (big_opM_commute _). Qed.
 
   Lemma big_sepM_forall Φ m :
-    (∀ k x, PersistentP (Φ k x)) →
+    (∀ k x, PersistentP true (Φ k x)) →
     ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ (∀ k x, ⌜m !! k = Some x⌝ → Φ k x).
   Proof.
     intros. apply (anti_symm _).
@@ -342,11 +342,11 @@ Section gmap.
     by rewrite -always_wand_impl always_elim wand_elim_l.
   Qed.
 
-  Global Instance big_sepM_empty_persistent Φ :
-    PersistentP ([∗ map] k↦x ∈ ∅, Φ k x).
+  Global Instance big_sepM_empty_persistent c Φ :
+    PersistentP c ([∗ 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).
+  Global Instance big_sepM_persistent c Φ m :
+    (∀ k x, PersistentP c (Φ k x)) → PersistentP c ([∗ 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).
@@ -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, PersistentP true (Φ x)) → ([∗ set] x ∈ X, Φ x) ⊣⊢ (∀ x, ⌜x ∈ X⌝ → Φ x).
   Proof.
     intros. apply (anti_symm _).
     { apply forall_intro=> x.
@@ -490,10 +490,10 @@ 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 c Φ : PersistentP c ([∗ 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).
+  Global Instance big_sepS_persistent c Φ X :
+    (∀ x, PersistentP c (Φ x)) → PersistentP c ([∗ set] x ∈ X, Φ x).
   Proof. rewrite /big_opS. apply _. Qed.
   Global Instance big_sepS_nil_timeless Φ : TimelessP ([∗ set] x ∈ ∅, Φ x).
   Proof. rewrite /big_opS elements_empty. apply _. Qed.
@@ -578,10 +578,10 @@ 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 c Φ : PersistentP c ([∗ 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).
+  Global Instance big_sepMS_persistent c Φ X :
+    (∀ x, PersistentP c (Φ x)) → PersistentP c ([∗ mset] x ∈ X, Φ x).
   Proof. rewrite /big_opMS. apply _. Qed.
   Global Instance big_sepMS_nil_timeless Φ : TimelessP ([∗ mset] x ∈ ∅, Φ x).
   Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed.
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index cdecce17d..81c79423e 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -16,11 +16,13 @@ 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 :=
-  (if p then â–¡ P else P)%I.
+Definition uPred_always_if {M} (c p : bool) (P : uPred M) : uPred M :=
+  (if p then â–¡{c} P else P)%I.
 Instance: Params (@uPred_always_if) 2.
-Arguments uPred_always_if _ !_ _/.
-Notation "â–¡? p P" := (uPred_always_if p P)
+Arguments uPred_always_if _ _ !_ _/.
+Notation "â–¡{ c }? p P" := (uPred_always_if c p P)
+  (at level 20, c at next level, p at level 9, P at level 20, format "â–¡{ c }? p  P").
+Notation "â–¡? p P" := (uPred_always_if true 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.
@@ -34,15 +36,10 @@ Arguments timelessP {_} _ {_}.
 Hint Mode TimelessP + ! : typeclass_instances.
 Instance: Params (@TimelessP) 1.
 
-Class PersistentP {M} (P : uPred M) := persistentP : P ⊢ □ P.
-Arguments persistentP {_} _ {_}.
-Hint Mode PersistentP + ! : typeclass_instances.
-Instance: Params (@PersistentP) 1.
-
-Class PlainP {M} (P : uPred M) := plainP : P ⊢ ☃ P.
-Arguments plainP {_} _ {_}.
-Hint Mode PlainP + ! : typeclass_instances.
-Instance: Params (@PlainP) 1.
+Class PersistentP {M} (c : bool) (P : uPred M) := persistentP : P ⊢ □{c} P.
+Arguments persistentP {_} _ _ {_}.
+Hint Mode PersistentP + + ! : typeclass_instances.
+Instance: Params (@PersistentP) 2.
 
 Module uPred.
 Section derived.
@@ -476,178 +473,105 @@ Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
 Lemma sep_forall_r {A} (Φ : A → uPred M) Q : (∀ a, Φ a) ∗ Q ⊢ ∀ a, Φ a ∗ Q.
 Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
 
-(* Plain modality *)
-Global Instance plainly_mono' : Proper ((⊢) ==> (⊢)) (@uPred_plainly M).
-Proof. intros P Q; apply plainly_mono. Qed.
-Global Instance naugth_flip_mono' :
-  Proper (flip (⊢) ==> flip (⊢)) (@uPred_plainly M).
-Proof. intros P Q; apply plainly_mono. Qed.
+(* The always modality *)
+Global Instance always_mono' c : Proper ((⊢) ==> (⊢)) (@uPred_always M c).
+Proof. intros P Q; apply always_mono. Qed.
+Global Instance always_flip_mono' c :
+  Proper (flip (⊢) ==> flip (⊢)) (@uPred_always M c).
+Proof. intros P Q; apply always_mono. Qed.
 
-Lemma plainly_elim P : ☃ P ⊢ P.
-Proof. by rewrite plainly_elim' always_elim. Qed.
-Hint Resolve plainly_mono plainly_elim.
-Lemma plainly_intro' P Q : (☃ P ⊢ Q) → ☃ P ⊢ ☃ Q.
-Proof. intros <-. apply plainly_idemp. Qed.
-Lemma plainly_idemp P : ☃ ☃ P ⊣⊢ ☃ P.
-Proof. apply (anti_symm _); auto using plainly_idemp. Qed.
+Lemma always_elim c P : □{c} P ⊢ P.
+Proof. destruct c; by rewrite ?always_mask_mono always_elim'. Qed.
+Hint Resolve always_elim always_mono.
+Lemma always_intro' c P Q : (□{c} P ⊢ Q) → □{c} P ⊢ □{c} Q.
+Proof. intros <-. apply always_idemp_2. Qed.
+Lemma always_idemp c P : □{c} □{c} P ⊣⊢ □{c} P.
+Proof. apply (anti_symm _); auto using always_idemp_2. Qed.
 
-Lemma always_plainly P : □ ☃ P ⊣⊢ ☃ P.
+Lemma always_idemp' c P : □ □{c} P ⊣⊢ □{c} P.
 Proof.
   apply (anti_symm _); auto using always_elim.
-  by rewrite -plainly_elim' plainly_idemp.
+  destruct c; [|rewrite -always_mask_mono]; by rewrite always_idemp.
 Qed.
-Lemma plainly_always P : ☃ □ P ⊣⊢ ☃ P.
+Lemma always_idemp'' c P : □{c} □ P ⊣⊢ □{c} P.
 Proof.
-  apply (anti_symm _); auto using plainly_mono, always_elim.
-  by rewrite -plainly_elim' plainly_idemp.
+  apply (anti_symm _); auto using always_elim.
+  destruct c; [|rewrite -always_mask_mono]; by rewrite always_idemp.
 Qed.
 
-Lemma plainly_pure φ : ☃ ⌜φ⌝ ⊣⊢ ⌜φ⌝.
+Lemma always_pure c φ : □{c} ⌜φ⌝ ⊣⊢ ⌜φ⌝.
 Proof.
   apply (anti_symm _); auto.
   apply pure_elim'=> Hφ.
-  trans (∀ x : False, ☃ True : uPred M)%I; [by apply forall_intro|].
-  rewrite plainly_forall_2. auto using plainly_mono, pure_intro.
+  trans (∀ x : False, □{c} True : uPred M)%I; [by apply forall_intro|].
+  rewrite always_forall_2. auto using always_mono, pure_intro.
 Qed.
-Lemma plainly_forall {A} (Ψ : A → uPred M) : (☃ ∀ a, Ψ a) ⊣⊢ (∀ a, ☃ Ψ a).
+Lemma always_forall {A} c (Ψ : A → uPred M) : (□{c} ∀ a, Ψ a) ⊣⊢ (∀ a, □{c} Ψ a).
 Proof.
-  apply (anti_symm _); auto using plainly_forall_2.
+  apply (anti_symm _); auto using always_forall_2.
   apply forall_intro=> x. by rewrite (forall_elim x).
 Qed.
-Lemma plainly_exist {A} (Ψ : A → uPred M) : (☃ ∃ a, Ψ a) ⊣⊢ (∃ a, ☃ Ψ a).
+Lemma always_exist {A} c (Ψ : A → uPred M) : (□{c} ∃ a, Ψ a) ⊣⊢ (∃ a, □{c} Ψ a).
 Proof.
-  apply (anti_symm _); auto using plainly_exist_1.
+  apply (anti_symm _); auto using always_exist_1.
   apply exist_elim=> x. by rewrite (exist_intro x).
 Qed.
-Lemma plainly_and P Q : ☃ (P ∧ Q) ⊣⊢ ☃ P ∧ ☃ Q.
-Proof. rewrite !and_alt plainly_forall. by apply forall_proper=> -[]. Qed.
-Lemma plainly_or P Q : ☃ (P ∨ Q) ⊣⊢ ☃ P ∨ ☃ Q.
-Proof. rewrite !or_alt plainly_exist. by apply exist_proper=> -[]. Qed.
-Lemma plainly_impl P Q : ☃ (P → Q) ⊢ ☃ P → ☃ Q.
+Lemma always_and c P Q : □{c} (P ∧ Q) ⊣⊢ □{c} P ∧ □{c} Q.
+Proof. rewrite !and_alt always_forall. by apply forall_proper=> -[]. Qed.
+Lemma always_or c P Q : □{c} (P ∨ Q) ⊣⊢ □{c} P ∨ □{c} Q.
+Proof. rewrite !or_alt always_exist. by apply exist_proper=> -[]. Qed.
+Lemma always_impl c P Q : □{c} (P → Q) ⊢ □{c} P → □{c} Q.
 Proof.
-  apply impl_intro_l; rewrite -plainly_and.
-  apply plainly_mono, impl_elim with P; auto.
+  apply impl_intro_l; rewrite -always_and.
+  apply always_mono, impl_elim with P; auto.
 Qed.
-Lemma plainly_internal_eq {A:ofeT} (a b : A) : ☃ (a ≡ b) ⊣⊢ a ≡ b.
+Lemma always_internal_eq {A : ofeT} c (a b : A) : □{c} (a ≡ b) ⊣⊢ a ≡ b.
 Proof.
   apply (anti_symm (⊢)); auto using always_elim.
-  apply (internal_eq_rewrite a b (λ b, ☃ (a ≡ b))%I); auto.
+  apply (internal_eq_rewrite a b (λ b, □{c} (a ≡ b))%I); auto.
   { intros n; solve_proper. }
-  rewrite -(internal_eq_refl a) plainly_pure; auto.
+  rewrite -(internal_eq_refl a) always_pure; auto.
 Qed.
-
-Lemma plainly_and_sep_l_1 P Q : ☃ P ∧ Q ⊢ ☃ P ∗ Q.
-Proof. by rewrite -always_plainly always_and_sep_l_1. Qed.
-Lemma plainly_and_sep_l' P Q : ☃ P ∧ Q ⊣⊢ ☃ P ∗ Q.
-Proof. apply (anti_symm (⊢)); auto using plainly_and_sep_l_1. Qed.
-Lemma plainly_and_sep_r' P Q : P ∧ ☃ Q ⊣⊢ P ∗ ☃ Q.
-Proof. by rewrite !(comm _ P) plainly_and_sep_l'. Qed.
-Lemma plainly_sep_dup' P : ☃ P ⊣⊢ ☃ P ∗ ☃ P.
-Proof. by rewrite -plainly_and_sep_l' idemp. Qed.
-
-Lemma plainly_and_sep P Q : ☃ (P ∧ Q) ⊣⊢ ☃ (P ∗ Q).
+Lemma always_and_sep_l' c P Q : □{c} P ∧ Q ⊣⊢ □{c} P ∗ Q.
 Proof.
   apply (anti_symm (⊢)); auto.
-  rewrite -{1}plainly_idemp plainly_and plainly_and_sep_l'; auto.
-Qed.
-Lemma plainly_sep P Q : ☃ (P ∗ Q) ⊣⊢ ☃ P ∗ ☃ Q.
-Proof. by rewrite -plainly_and_sep -plainly_and_sep_l' plainly_and. Qed.
-
-Lemma plainly_wand P Q : ☃ (P -∗ Q) ⊢ ☃ P -∗ ☃ Q.
-Proof. by apply wand_intro_r; rewrite -plainly_sep wand_elim_l. Qed.
-Lemma plainly_wand_impl P Q : ☃ (P -∗ Q) ⊣⊢ ☃ (P → Q).
-Proof.
-  apply (anti_symm (⊢)); [|by rewrite -impl_wand].
-  apply plainly_intro', impl_intro_r.
-  by rewrite plainly_and_sep_l' plainly_elim wand_elim_l.
-Qed.
-Lemma wand_impl_plainly P Q : (☃ P -∗ Q) ⊣⊢ (☃ P → Q).
-Proof.
-  apply (anti_symm (⊢)); [|by rewrite -impl_wand].
-  apply impl_intro_l. by rewrite plainly_and_sep_l' wand_elim_r.
-Qed.
-Lemma plainly_entails_l' P Q : (P ⊢ ☃ Q) → P ⊢ ☃ Q ∗ P.
-Proof. intros; rewrite -plainly_and_sep_l'; auto. Qed.
-Lemma plainly_entails_r' P Q : (P ⊢ ☃ Q) → P ⊢ P ∗ ☃ Q.
-Proof. intros; rewrite -plainly_and_sep_r'; auto. Qed.
-
-Lemma plainly_laterN n P : ☃ ▷^n P ⊣⊢ ▷^n ☃ P.
-Proof. induction n as [|n IH]; simpl; auto. by rewrite plainly_later IH. 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.
-
-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 always_pure φ : □ ⌜φ⌝ ⊣⊢ ⌜φ⌝.
-Proof. by rewrite -plainly_pure always_plainly. Qed.
-Lemma always_forall {A} (Ψ : A → uPred M) : (□ ∀ a, Ψ a) ⊣⊢ (∀ a, □ Ψ a).
-Proof.
-  apply (anti_symm _); auto using always_forall_2.
-  apply forall_intro=> x. by rewrite (forall_elim x).
-Qed.
-Lemma always_exist {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a) ⊣⊢ (∃ a, □ Ψ a).
-Proof.
-  apply (anti_symm _); auto using always_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.
-Proof.
-  apply impl_intro_l; rewrite -always_and.
-  apply always_mono, impl_elim with P; auto.
+  by rewrite -always_idemp' always_and_sep_l_1'.
 Qed.
-Lemma always_internal_eq {A:ofeT} (a b : A) : □ (a ≡ b) ⊣⊢ a ≡ b.
-Proof. by rewrite -plainly_internal_eq always_plainly. 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.
+Lemma always_and_sep_r' c P Q : P ∧ □{c} Q ⊣⊢ P ∗ □{c} Q.
 Proof. by rewrite !(comm _ P) always_and_sep_l'. Qed.
-Lemma always_sep_dup' P : □ P ⊣⊢ □ P ∗ □ P.
+Lemma always_sep_dup' c P : □{c} P ⊣⊢ □{c} P ∗ □{c} P.
 Proof. by rewrite -always_and_sep_l' idemp. Qed.
 
-Lemma always_and_sep P Q : □ (P ∧ Q) ⊣⊢ □ (P ∗ Q).
+Lemma always_and_sep c P Q : □{c} (P ∧ Q) ⊣⊢ □{c} (P ∗ Q).
 Proof.
   apply (anti_symm (⊢)); auto.
   rewrite -{1}always_idemp always_and always_and_sep_l'; auto.
 Qed.
-Lemma always_sep P Q : □ (P ∗ Q) ⊣⊢ □ P ∗ □ Q.
+Lemma always_sep c P Q : □{c} (P ∗ Q) ⊣⊢ □{c} P ∗ □{c} Q.
 Proof. by rewrite -always_and_sep -always_and_sep_l' always_and. Qed.
 
-Lemma always_wand P Q : □ (P -∗ Q) ⊢ □ P -∗ □ Q.
+Lemma always_wand c P Q : □{c} (P -∗ Q) ⊢ □{c} P -∗ □{c} 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 always_wand_impl c P Q : □{c} (P -∗ Q) ⊣⊢ □{c} (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.
 Qed.
-Lemma wand_impl_always P Q : ((□ P) -∗ Q) ⊣⊢ ((□ P) → Q).
+Lemma wand_impl_always c P Q : (□{c} P -∗ Q) ⊣⊢ (□{c} P → Q).
 Proof.
   apply (anti_symm (⊢)); [|by rewrite -impl_wand].
   apply impl_intro_l. by rewrite always_and_sep_l' wand_elim_r.
 Qed.
-Lemma always_entails_l' P Q : (P ⊢ □ Q) → P ⊢ □ Q ∗ P.
+Lemma always_entails_l' c P Q : (P ⊢ □{c} Q) → P ⊢ □{c} Q ∗ P.
 Proof. intros; rewrite -always_and_sep_l'; auto. Qed.
-Lemma always_entails_r' P Q : (P ⊢ □ Q) → P ⊢ P ∗ □ Q.
+Lemma always_entails_r' c P Q : (P ⊢ □{c} Q) → P ⊢ P ∗ □{c} Q.
 Proof. intros; rewrite -always_and_sep_r'; auto. Qed.
 
-Lemma always_laterN n P : □ ▷^n P ⊣⊢ ▷^n □ P.
+Lemma always_laterN c n P : □{c} ▷^n P ⊣⊢ ▷^n □{c} P.
 Proof. induction n as [|n IH]; simpl; auto. by rewrite always_later IH. Qed.
 
-Lemma wand_alt P Q : (P -∗ Q) ⊣⊢ ∃ R, R ∗ □ (P ∗ R → Q).
+Lemma wand_alt c P Q : (P -∗ Q) ⊣⊢ ∃ R, R ∗ □{c} (P ∗ R → Q).
 Proof.
   apply (anti_symm (⊢)).
   - rewrite -(right_id True%I uPred_sep (P -∗ Q)%I) -(exist_intro (P -∗ Q)%I).
@@ -656,7 +580,7 @@ Proof.
   - apply exist_elim=> R. apply wand_intro_l. rewrite assoc -always_and_sep_r'.
     by rewrite always_elim impl_elim_r.
 Qed.
-Lemma impl_alt P Q : (P → Q) ⊣⊢ ∃ R, R ∧ □ (P ∧ R -∗ Q).
+Lemma impl_alt c P Q : (P → Q) ⊣⊢ ∃ R, R ∧ □{c} (P ∧ R -∗ Q).
 Proof.
   apply (anti_symm (⊢)).
   - rewrite -(right_id True%I uPred_and (P → Q)%I) -(exist_intro (P → Q)%I).
@@ -764,31 +688,31 @@ 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).
+Global Instance always_if_ne c p : NonExpansive (@uPred_always_if M c p).
 Proof. solve_proper. Qed.
-Global Instance always_if_proper p : Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_always_if M p).
+Global Instance always_if_proper c p : Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_always_if M c p).
 Proof. solve_proper. Qed.
-Global Instance always_if_mono p : Proper ((⊢) ==> (⊢)) (@uPred_always_if M p).
+Global Instance always_if_mono c p : Proper ((⊢) ==> (⊢)) (@uPred_always_if M c p).
 Proof. solve_proper. Qed.
 
-Lemma always_if_elim p P : □?p P ⊢ P.
+Lemma always_if_elim c p P : □{c}?p P ⊢ P.
 Proof. destruct p; simpl; auto using always_elim. Qed.
-Lemma always_elim_if p P : □ P ⊢ □?p P.
+Lemma always_elim_if c p P : □{c} P ⊢ □{c}?p P.
 Proof. destruct p; simpl; auto using always_elim. Qed.
 
-Lemma always_if_pure p φ : □?p ⌜φ⌝ ⊣⊢ ⌜φ⌝.
+Lemma always_if_pure c p φ : □{c}?p ⌜φ⌝ ⊣⊢ ⌜φ⌝.
 Proof. destruct p; simpl; auto using always_pure. Qed.
-Lemma always_if_and p P Q : □?p (P ∧ Q) ⊣⊢ □?p P ∧ □?p Q.
+Lemma always_if_and c p P Q : □{c}?p (P ∧ Q) ⊣⊢ □{c}?p P ∧ □{c}?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.
+Lemma always_if_or c p P Q : □{c}?p (P ∨ Q) ⊣⊢ □{c}?p P ∨ □{c}?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.
+Lemma always_if_exist {A} c p (Ψ : A → uPred M) : (□{c}?p ∃ a, Ψ a) ⊣⊢ ∃ a, □{c}?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.
+Lemma always_if_sep c p P Q : □{c}?p (P ∗ Q) ⊣⊢ □{c}?p P ∗ □{c}?p Q.
 Proof. destruct p; simpl; auto using always_sep. Qed.
-Lemma always_if_later p P : □?p ▷ P ⊣⊢ ▷ □?p P.
+Lemma always_if_later c p P : □{c}?p ▷ P ⊣⊢ ▷ □{c}?p P.
 Proof. destruct p; simpl; auto using always_later. Qed.
-Lemma always_if_laterN p n P : □?p ▷^n P ⊣⊢ ▷^n □?p P.
+Lemma always_if_laterN c p n P : □{c}?p ▷^n P ⊣⊢ ▷^n □{c}?p P.
 Proof. destruct p; simpl; auto using always_laterN. Qed.
 
 (* True now *)
@@ -819,7 +743,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 -(always_pure true) -always_later -always_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.
@@ -835,11 +759,9 @@ 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.
+Lemma except_0_always c P : ◇ □{c} P ⊣⊢ □{c} ◇ P.
 Proof. by rewrite /uPred_except_0 always_or always_later always_pure. Qed.
-Lemma except_0_plainly P : ◇ ☃ P ⊣⊢ ☃ ◇ P.
-Proof. by rewrite /uPred_except_0 plainly_or plainly_later plainly_pure. Qed.
-Lemma except_0_always_if p P : ◇ □?p P ⊣⊢ □?p ◇ P.
+Lemma except_0_always_if c p P : ◇ □{c}?p P ⊣⊢ □{c}?p ◇ P.
 Proof. destruct p; simpl; auto using except_0_always. Qed.
 Lemma except_0_frame_l P Q : P ∗ ◇ Q ⊢ ◇ (P ∗ Q).
 Proof. by rewrite {1}(except_0_intro P) except_0_sep. Qed.
@@ -858,10 +780,11 @@ 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 plainly_cmra_valid {A : cmraT} (a : A) : ☃ ✓ a ⊣⊢ ✓ a.
-Proof. apply (anti_symm _); auto using plainly_elim, plainly_cmra_valid_1. Qed.
-Lemma always_cmra_valid {A : cmraT} (a : A) : □ ✓ a ⊣⊢ ✓ a.
-Proof. by rewrite -plainly_cmra_valid always_plainly. Qed.
+Lemma always_cmra_valid {A : cmraT} c (a : A) : □{c} ✓ a ⊣⊢ ✓ a.
+Proof.
+  apply (anti_symm _); auto using always_elim.
+  rewrite {1}always_cmra_valid_1'. destruct c; auto using always_mask_mono.
+Qed.
 
 (** * Derived rules *)
 Global Instance bupd_mono' : Proper ((⊢) ==> (⊢)) (@uPred_bupd M).
@@ -917,7 +840,7 @@ 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'.
+  rewrite -(always_pure true) -always_later always_and_sep_l'.
   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) :
@@ -954,151 +877,92 @@ Global Instance from_option_timeless {A} P (Ψ : A → uPred M) (mx : option A)
   (∀ x, TimelessP (Ψ x)) → TimelessP P → TimelessP (from_option Ψ P mx).
 Proof. destruct mx; apply _. Qed.
 
-(* Derived lemmas for plainness *)
-Global Instance PlainP_proper : Proper ((≡) ==> iff) (@PlainP M).
-Proof. solve_proper. Qed.
-Global Instance limit_preserving_PlainP {A:ofeT} `{Cofe A} (Φ : A → uPred M) :
-  NonExpansive Φ → LimitPreserving (λ x, PlainP (Φ x)).
-Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
-
-Lemma plain_persistent P : PlainP P → PersistentP P.
-Proof. rewrite /PlainP /PersistentP => HP. by rewrite {1}HP plainly_elim'. Qed.
-
-Lemma plainly_plainly P `{!PlainP P} : ☃ P ⊣⊢ P.
-Proof. apply (anti_symm (⊢)); eauto. Qed.
-Lemma plainly_intro P Q `{!PlainP P} : (P ⊢ Q) → P ⊢ ☃ Q.
-Proof. rewrite -(plainly_plainly P); apply plainly_intro'. Qed.
-
-Lemma bupd_plain P `{!PlainP P} : (|==> P) ⊢ P.
-Proof. by rewrite -{1}(plainly_plainly P) bupd_plainly. Qed.
-
 (* Derived lemmas for persistence *)
-Global Instance PersistentP_proper : Proper ((≡) ==> iff) (@PersistentP M).
+Global Instance PersistentP_proper c : Proper ((≡) ==> iff) (@PersistentP M c).
 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_PersistentP
+    {A:ofeT} `{Cofe A} c (Φ : A → uPred M) :
+  NonExpansive Φ → LimitPreserving (λ x, PersistentP c (Φ x)).
 Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
 
-Lemma always_always P `{!PersistentP P} : □ P ⊣⊢ P.
+Lemma persistent_mask_weaken P : PersistentP false P → PersistentP true P.
+Proof. rewrite /PersistentP=> HP. by rewrite {1}HP always_mask_mono. Qed.
+
+Lemma always_always c P `{!PersistentP c P} : □{c} 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 c p P `{!PersistentP c P} : □{c}?p P ⊣⊢ P.
 Proof. destruct p; simpl; auto using always_always. Qed.
-Lemma always_intro P Q `{!PersistentP 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.
-Proof. by rewrite -(always_always P) always_and_sep_l'. Qed.
-Lemma always_and_sep_r P Q `{!PersistentP 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.
-Proof. by rewrite -(always_always P) -always_sep_dup'. Qed.
-Lemma always_entails_l P Q `{!PersistentP 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.
-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_intro c P Q `{!PersistentP c P} : (P ⊢ Q) → P ⊢ □{c} Q.
+Proof. rewrite -(always_always c P); apply always_intro'. Qed.
+Lemma always_and_sep_l P Q `{!PersistentP true P} : P ∧ Q ⊣⊢ P ∗ Q.
+Proof. by rewrite -(always_always true P) always_and_sep_l'. Qed.
+Lemma always_and_sep_r P Q `{!PersistentP true Q} : P ∧ Q ⊣⊢ P ∗ Q.
+Proof. by rewrite -(always_always true Q) always_and_sep_r'. Qed.
+Lemma always_sep_dup P `{!PersistentP true P} : P ⊣⊢ P ∗ P.
+Proof. by rewrite -(always_always true P) -always_sep_dup'. Qed.
+Lemma always_entails_l P Q `{!PersistentP true Q} : (P ⊢ Q) → P ⊢ Q ∗ P.
+Proof. by rewrite -(always_always true Q); apply always_entails_l'. Qed.
+Lemma always_entails_r P Q `{!PersistentP true Q} : (P ⊢ Q) → P ⊢ P ∗ Q.
+Proof. by rewrite -(always_always true Q); apply always_entails_r'. Qed.
+Lemma always_impl_wand P `{!PersistentP true 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.
 
-(* Plain *)
-Global Instance pure_plain φ : PlainP (⌜φ⌝ : uPred M)%I.
-Proof. by rewrite /PlainP plainly_pure. Qed.
-Global Instance impl_plain P Q : PlainP P → PlainP Q → PlainP (P → Q).
-Proof.
-  rewrite /PlainP=> HP HQ.
-  by rewrite {2}HP -plainly_impl_plainly -HQ plainly_elim.
-Qed.
-Global Instance wand_plain P Q : PlainP P → PlainP Q → PlainP (P -∗ Q)%I.
-Proof.
-  rewrite /PlainP=> HP HQ.
-  by rewrite {2}HP -{1}(plainly_elim P) !wand_impl_plainly -plainly_impl_plainly -HQ.
-Qed.
-Global Instance plainly_plain P : PlainP (☃ P).
-Proof. by intros; apply plainly_intro'. Qed.
-Global Instance always_plain P : PlainP P → PlainP (□ P).
-Proof. rewrite /PlainP=> HP. by rewrite {1}HP always_plainly plainly_always. Qed.
-Global Instance and_plain P Q :
-  PlainP P → PlainP Q → PlainP (P ∧ Q).
-Proof. by intros; rewrite /PlainP plainly_and; apply and_mono. Qed.
-Global Instance or_plain P Q :
-  PlainP P → PlainP Q → PlainP (P ∨ Q).
-Proof. by intros; rewrite /PlainP plainly_or; apply or_mono. Qed.
-Global Instance sep_plain P Q :
-  PlainP P → PlainP Q → PlainP (P ∗ Q).
-Proof. by intros; rewrite /PlainP plainly_sep; apply sep_mono. Qed.
-Global Instance forall_plain {A} (Ψ : A → uPred M) :
-  (∀ x, PlainP (Ψ x)) → PlainP (∀ x, Ψ x).
-Proof. by intros; rewrite /PlainP plainly_forall; apply forall_mono. Qed.
-Global Instance exist_palin {A} (Ψ : A → uPred M) :
-  (∀ x, PlainP (Ψ x)) → PlainP (∃ x, Ψ x).
-Proof. by intros; rewrite /PlainP plainly_exist; apply exist_mono. Qed.
-Global Instance internal_eq_plain {A : ofeT} (a b : A) :
-  PlainP (a ≡ b : uPred M)%I.
-Proof. by intros; rewrite /PlainP plainly_internal_eq. Qed.
-Global Instance cmra_valid_plain {A : cmraT} (a : A) :
-  PlainP (✓ a : uPred M)%I.
-Proof. by intros; rewrite /PlainP; apply plainly_cmra_valid_1. Qed.
-Global Instance later_plain P : PlainP P → PlainP (▷ P).
-Proof. by intros; rewrite /PlainP plainly_later; apply later_mono. Qed.
-Global Instance except_0_plain P : PlainP P → PlainP (◇ P).
-Proof. by intros; rewrite /PlainP -except_0_plainly; apply except_0_mono. Qed.
-Global Instance laterN_plain n P : PlainP P → PlainP (▷^n P).
-Proof. induction n; apply _. Qed.
-Global Instance from_option_palin {A} P (Ψ : A → uPred M) (mx : option A) :
-  (∀ x, PlainP (Ψ x)) → PlainP P → PlainP (from_option Ψ P mx).
-Proof. destruct mx; apply _. Qed.
+Lemma bupd_persistent P `{!PersistentP false P} : (|==> P) ⊢ P.
+Proof. by rewrite -{1}(always_always false P) bupd_always. Qed.
 
 (* Persistence *)
-Global Instance pure_persistent φ : PersistentP (⌜φ⌝ : uPred M)%I.
+Global Instance pure_persistent c φ : PersistentP c (⌜φ⌝ : uPred M)%I.
 Proof. by rewrite /PersistentP always_pure. Qed.
-Global Instance impl_persistent P Q :
-  PlainP P → PersistentP Q → PersistentP (P → Q).
+Global Instance impl_persistent c P Q :
+  PersistentP false P → PersistentP c Q → PersistentP c (P → Q).
 Proof.
-  rewrite /PlainP /PersistentP=> HP HQ.
-  rewrite {2}HP -always_impl_plainly. by rewrite -HQ plainly_elim.
+  rewrite /PersistentP=> HP HQ.
+  rewrite {2}HP -always_impl_always. by rewrite -HQ always_elim.
 Qed.
-Global Instance wand_persistent P Q :
-  PlainP P → PersistentP Q → PersistentP (P -∗ Q)%I.
+Global Instance wand_persistent c P Q :
+  PersistentP false P → PersistentP c Q → PersistentP c (P -∗ Q)%I.
 Proof.
-  rewrite /PlainP /PersistentP=> HP HQ.
-  by rewrite {2}HP -{1}(plainly_elim P) !wand_impl_plainly -always_impl_plainly -HQ.
+  rewrite /PersistentP=> HP HQ.
+  by rewrite {2}HP -{1}(always_elim false P) !wand_impl_always -always_impl_always -HQ.
 Qed.
-Global Instance plainly_persistent P : PersistentP (☃ P).
-Proof. by rewrite /PersistentP always_plainly. Qed.
-Global Instance always_persistent P : PersistentP (â–¡ P).
-Proof. by intros; apply always_intro'. Qed.
-Global Instance and_persistent P Q :
-  PersistentP P → PersistentP Q → PersistentP (P ∧ Q).
+Global Instance always_persistent c P : PersistentP c (â–¡{c} P).
+Proof. by apply always_intro'. Qed.
+Global Instance always_persistent' c P : PersistentP true (â–¡{c} P).
+Proof. by rewrite /PersistentP always_idemp'. Qed.
+Global Instance and_persistent c P Q :
+  PersistentP c P → PersistentP c Q → PersistentP c (P ∧ Q).
 Proof. by intros; rewrite /PersistentP always_and; apply and_mono. Qed.
-Global Instance or_persistent P Q :
-  PersistentP P → PersistentP Q → PersistentP (P ∨ Q).
+Global Instance or_persistent c P Q :
+  PersistentP c P → PersistentP c Q → PersistentP c (P ∨ Q).
 Proof. by intros; rewrite /PersistentP always_or; apply or_mono. Qed.
-Global Instance sep_persistent P Q :
-  PersistentP P → PersistentP Q → PersistentP (P ∗ Q).
+Global Instance sep_persistent c P Q :
+  PersistentP c P → PersistentP c Q → PersistentP c (P ∗ Q).
 Proof. by intros; rewrite /PersistentP always_sep; apply sep_mono. Qed.
-Global Instance forall_persistent {A} (Ψ : A → uPred M) :
-  (∀ x, PersistentP (Ψ x)) → PersistentP (∀ x, Ψ x).
+Global Instance forall_persistent {A} c (Ψ : A → uPred M) :
+  (∀ x, PersistentP c (Ψ x)) → PersistentP c (∀ x, Ψ x).
 Proof. by intros; rewrite /PersistentP always_forall; apply forall_mono. Qed.
-Global Instance exist_persistent {A} (Ψ : A → uPred M) :
-  (∀ x, PersistentP (Ψ x)) → PersistentP (∃ x, Ψ x).
+Global Instance exist_persistent {A} c (Ψ : A → uPred M) :
+  (∀ x, PersistentP c (Ψ x)) → PersistentP c (∃ x, Ψ x).
 Proof. by intros; rewrite /PersistentP always_exist; apply exist_mono. Qed.
-Global Instance internal_eq_persistent {A : ofeT} (a b : A) :
-  PersistentP (a ≡ b : uPred M)%I.
+Global Instance internal_eq_persistent {A : ofeT} c (a b : A) :
+  PersistentP c (a ≡ b : uPred M)%I.
 Proof. by intros; rewrite /PersistentP always_internal_eq. Qed.
-Global Instance cmra_valid_persistent {A : cmraT} (a : A) :
-  PersistentP (✓ a : uPred M)%I.
+Global Instance cmra_valid_persistent {A : cmraT} c (a : A) :
+  PersistentP c (✓ a : uPred M)%I.
 Proof. by intros; rewrite /PersistentP always_cmra_valid. Qed.
-Global Instance later_persistent P : PersistentP P → PersistentP (▷ P).
+Global Instance later_persistent c P : PersistentP c P → PersistentP c (▷ P).
 Proof. by intros; rewrite /PersistentP always_later; apply later_mono. Qed.
-Global Instance except_0_persistent P : PersistentP P → PersistentP (◇ P).
+Global Instance except_0_persistent c P : PersistentP c P → PersistentP c (◇ P).
 Proof. by intros; rewrite /PersistentP -except_0_always; apply except_0_mono. Qed.
-Global Instance laterN_persistent n P : PersistentP P → PersistentP (▷^n P).
+Global Instance laterN_persistent c n P : PersistentP c P → PersistentP c (▷^n P).
 Proof. induction n; apply _. Qed.
-Global Instance ownM_persistent : Persistent a → PersistentP (@uPred_ownM M a).
+Global Instance ownM_persistent : Persistent a → PersistentP true (@uPred_ownM M a).
 Proof. intros. by rewrite /PersistentP 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).
+Global Instance from_option_persistent {A} c P (Ψ : A → uPred M) (mx : option A) :
+  (∀ x, PersistentP c (Ψ x)) → PersistentP c P → PersistentP c (from_option Ψ P mx).
 Proof. destruct mx; apply _. Qed.
 
 (* For big ops *)
@@ -1109,14 +973,11 @@ 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).
+Global Instance uPred_always_and_homomorphism c :
+  MonoidHomomorphism uPred_and uPred_and (≡) (@uPred_always M c).
 Proof. split; [split; try apply _|]. apply always_and. apply always_pure. Qed.
-Global Instance uPred_plainly_and_homomorphism :
-  MonoidHomomorphism uPred_and uPred_and (≡) (@uPred_plainly M).
-Proof. split; [split; try apply _|]. apply plainly_and. apply plainly_pure. Qed.
-Global Instance uPred_always_if_and_homomorphism b :
-  MonoidHomomorphism uPred_and uPred_and (≡) (@uPred_always_if M b).
+Global Instance uPred_always_if_and_homomorphism c b :
+  MonoidHomomorphism uPred_and uPred_and (≡) (@uPred_always_if M c b).
 Proof. split; [split; try apply _|]. apply always_if_and. apply always_if_pure. Qed.
 Global Instance uPred_later_monoid_and_homomorphism :
   MonoidHomomorphism uPred_and uPred_and (≡) (@uPred_later M).
@@ -1128,14 +989,11 @@ 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).
+Global Instance uPred_always_or_homomorphism c :
+  MonoidHomomorphism uPred_or uPred_or (≡) (@uPred_always M c).
 Proof. split; [split; try apply _|]. apply always_or. apply always_pure. Qed.
-Global Instance uPred_plainly_or_homomorphism :
-  MonoidHomomorphism uPred_or uPred_or (≡) (@uPred_plainly M).
-Proof. split; [split; try apply _|]. apply plainly_or. apply plainly_pure. Qed.
-Global Instance uPred_always_if_or_homomorphism b :
-  MonoidHomomorphism uPred_or uPred_or (≡) (@uPred_always_if M b).
+Global Instance uPred_always_if_or_homomorphism c b :
+  MonoidHomomorphism uPred_or uPred_or (≡) (@uPred_always_if M c b).
 Proof. split; [split; try apply _|]. apply always_if_or. apply always_if_pure. Qed.
 Global Instance uPred_later_monoid_or_homomorphism :
   WeakMonoidHomomorphism uPred_or uPred_or (≡) (@uPred_later M).
@@ -1147,14 +1005,11 @@ 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).
+Global Instance uPred_always_sep_homomorphism c :
+  MonoidHomomorphism uPred_sep uPred_sep (≡) (@uPred_always M c).
 Proof. split; [split; try apply _|]. apply always_sep. apply always_pure. Qed.
-Global Instance uPred_plainly_sep_homomorphism :
-  MonoidHomomorphism uPred_sep uPred_sep (≡) (@uPred_plainly M).
-Proof. split; [split; try apply _|]. apply plainly_sep. apply plainly_pure. Qed.
-Global Instance uPred_always_if_sep_homomorphism b :
-  MonoidHomomorphism uPred_sep uPred_sep (≡) (@uPred_always_if M b).
+Global Instance uPred_always_if_sep_homomorphism c b :
+  MonoidHomomorphism uPred_sep uPred_sep (≡) (@uPred_always_if M c b).
 Proof. split; [split; try apply _|]. apply always_if_sep. apply always_if_pure. Qed.
 Global Instance uPred_later_monoid_sep_homomorphism :
   MonoidHomomorphism uPred_sep uPred_sep (≡) (@uPred_later M).
@@ -1171,11 +1026,11 @@ Proof. split; [split; try apply _|]. apply ownM_op. apply ownM_unit'. Qed.
 End derived.
 End uPred.
 
-(* When declared as an actual instance, [plain_persistent] will give cause
+(* When declared as an actual instance, [persistent_mask_weaken] will give cause
 failing proof searches to take exponential time, as Coq will try to apply it
 the instance at any node in the proof search tree.
 
 To avoid that, we declare it using a [Hint Immediate], so that it will only be
 used at the leaves of the proof search tree, i.e. when the premise of the hint
 can be derived from just the current context. *)
-Hint Immediate uPred.plain_persistent : typeclass_instances.
+Hint Immediate uPred.persistent_mask_weaken : typeclass_instances.
diff --git a/theories/base_logic/lib/auth.v b/theories/base_logic/lib/auth.v
index a46400ae9..67b9ac7dc 100644
--- a/theories/base_logic/lib/auth.v
+++ b/theories/base_logic/lib/auth.v
@@ -32,7 +32,8 @@ Section definitions.
   Proof. solve_proper. Qed.
   Global Instance auth_own_timeless a : TimelessP (auth_own a).
   Proof. apply _. Qed.
-  Global Instance auth_own_persistent a : Persistent a → PersistentP (auth_own a).
+  Global Instance auth_own_persistent a :
+    Persistent a → PersistentP true (auth_own a).
   Proof. apply _. Qed.
 
   Global Instance auth_inv_ne n :
@@ -51,7 +52,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 φ : PersistentP true (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 d41ce60ff..4a3091b1b 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 : PersistentP true (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 83e3629d7..7fda48d80 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -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 : PersistentP true (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 5419422c2..1c1351710 100644
--- a/theories/base_logic/lib/core.v
+++ b/theories/base_logic/lib/core.v
@@ -5,7 +5,7 @@ Import uPred.
 
 (** The "core" of an assertion is its maximal persistent part. *)
 Definition coreP {M : ucmraT} (P : uPred M) : uPred M :=
-  (∀ Q, ☃ (Q → □ Q) → ☃ (P → Q) → Q)%I.
+  (∀ Q, □{false} (Q → □ Q) → □{false} (P → Q) → Q)%I.
 Instance: Params (@coreP) 1.
 Typeclasses Opaque coreP.
 
@@ -16,12 +16,12 @@ Section core.
   Lemma coreP_intro P : P -∗ coreP P.
   Proof. iIntros "HP". iIntros (Q) "_ HPQ". by iApply "HPQ". Qed.
 
-  Global Instance coreP_persistent P : PersistentP (coreP P).
+  Global Instance coreP_persistent P : PersistentP true (coreP P).
   Proof.
     rewrite /coreP /PersistentP. iIntros "HC".
     iApply always_forall. iIntros (Q). (* FIXME: iIntros should apply always_forall automatically. *)
-    iApply always_impl_plainly. iIntros "#HQ".
-    iApply always_impl_plainly. iIntros "#HPQ".
+    iApply always_impl_always. iIntros "#HQ".
+    iApply always_impl_always. iIntros "#HPQ".
     iApply "HQ". iApply "HC"; done.
   Qed.
 
@@ -36,7 +36,7 @@ Section core.
     iApply ("H" $! Q with "[]"); first done. by rewrite HP.
   Qed.
 
-  Lemma coreP_elim P : PersistentP P → coreP P -∗ P.
+  Lemma coreP_elim P : PersistentP true P → coreP P -∗ P.
   Proof. rewrite /coreP. iIntros (?) "HCP". iApply ("HCP" $! P); auto. Qed.
 
   Lemma coreP_wand P Q : (coreP P ⊢ Q) ↔ (P ⊢ □ Q).
@@ -45,6 +45,6 @@ Section core.
     - iIntros (HP) "HP". iDestruct (coreP_intro with "HP") as "#HcP".
       iAlways. by iApply HP.
     - iIntros (HPQ) "HcP". iDestruct (coreP_mono _ _ HPQ with "HcP") as "HcQ".
-      iDestruct (coreP_elim with "HcQ") as "#HQ". done.
+      iApply (coreP_elim with "HcQ").
   Qed.
 End core.
diff --git a/theories/base_logic/lib/counter_examples.v b/theories/base_logic/lib/counter_examples.v
index 6a303b19a..8975da9cb 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, PersistentP true (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).
@@ -67,7 +67,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, PersistentP true (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).
@@ -130,7 +130,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 : PersistentP true (saved γ P) := _.
 
   Lemma saved_alloc (P : gname → iProp) : fupd M1 (∃ γ, saved γ (P γ)).
   Proof.
@@ -163,7 +163,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 : PersistentP true (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.v b/theories/base_logic/lib/fancy_updates.v
index 9e707ab9b..da372ddd1 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -141,7 +141,7 @@ Proof.
   intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
 Qed.
 
-Lemma fupd_plain' {E1 E2 E2'} P Q `{!PlainP P} :
+Lemma fupd_persistent' {E1 E2 E2'} P Q `{!PersistentP false P} :
   E1 ⊆ E2 →
   (Q ={E1, E2'}=∗ P) → (|={E1, E2}=> Q) ⊢ |={E1}=> ((|={E1, E2}=> Q) ∗ P).
 Proof.
@@ -153,27 +153,27 @@ Proof.
   iMod "H" as "(Hws & HE2 & HQ)".
   rewrite ownE_op; trivial; iDestruct "HE2" as "[HE1 HE3]".
   iAssert (â—‡ P)%I with "[HQ Hws HE1]" as "#HP".
-  { iApply bupd_plain; eauto.
+  { iApply bupd_persistent; eauto.
     by iMod ("HQP" with "HQ [$]") as "[_ [_ HP]]". }
   iModIntro. iMod "HP".
   iModIntro; iFrame; auto.
 Qed.
 
-Lemma fupd_plain {E1 E2} P Q `{!PlainP P} :
+Lemma fupd_plain {E1 E2} P Q `{!PersistentP false P} :
   E1 ⊆ E2 → (Q ⊢ P) → (|={E1, E2}=> Q) ⊢ |={E1}=> ((|={E1, E2}=> Q) ∗ P).
 Proof.
   iIntros (HE HQP) "HQ".
-  iApply (fupd_plain' with "HQ"); auto.
+  iApply (fupd_persistent' with "HQ"); auto.
   by iIntros "?"; iApply fupd_intro; iApply HQP.
 Qed.
 
-Lemma later_fupd_plain {E} P `{Hpl: !PlainP P} :
+Lemma later_fupd_plain {E} P `{Hpl: !PersistentP false P} :
   (▷ |={E}=> P) ⊢ |={E}=> ▷ ◇ P.
 Proof.
   iIntros "HP". rewrite fupd_eq /fupd_def.
   iIntros "[Hs He]".
   iAssert (â–· â—‡ P)%I with "[-]" as "#HP'".
-  { iNext. iApply bupd_plain; eauto.
+  { iNext. iApply bupd_persistent; eauto.
     iMod ("HP" with "[$]") as "HP".
     iModIntro. iMod "HP" as "(_&_&HP)". by iModIntro. }
   by iFrame.
diff --git a/theories/base_logic/lib/fancy_updates_from_vs.v b/theories/base_logic/lib/fancy_updates_from_vs.v
index fc505d702..bf27ce2fa 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, PersistentP true (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 →
+  PersistentP true 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 a94ea6989..6bcc01f70 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).
+    PersistentP true 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/invariants.v b/theories/base_logic/lib/invariants.v
index cadd0c88d..664494284 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 : PersistentP true (inv N P).
 Proof. rewrite inv_eq /inv; apply _. Qed.
 
 Lemma fresh_inv_name (E : gset positive) N : ∃ i, i ∉ E ∧ i ∈ (↑N:coPset).
diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index 2f20a514e..d477ea58d 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -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 : PersistentP true (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 4049d8dc2..7c4564260 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -108,7 +108,7 @@ Proof. by rewrite comm -own_valid_r. Qed.
 
 Global Instance own_timeless γ a : Timeless a → TimelessP (own γ a).
 Proof. rewrite !own_eq /own_def; apply _. Qed.
-Global Instance own_core_persistent γ a : Persistent a → PersistentP (own γ a).
+Global Instance own_core_persistent γ a : Persistent a → PersistentP true (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 4002d1d82..04d85dbf3 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -23,7 +23,8 @@ 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 :
+    PersistentP true (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 047d10d32..9d7fde93c 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 φ : PersistentP true (sts_ctx N φ).
   Proof. apply _. Qed.
-  Global Instance sts_own_persistent s : PersistentP (sts_own s ∅).
+  Global Instance sts_own_persistent s : PersistentP true (sts_own s ∅).
   Proof. apply _. Qed.
-  Global Instance sts_ownS_persistent S : PersistentP (sts_ownS S ∅).
+  Global Instance sts_ownS_persistent S : PersistentP true (sts_ownS S ∅).
   Proof. apply _. Qed.
 End definitions.
 
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index 3d658b58f..dfe5c6b2b 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 : PersistentP true (ownI i P).
 Proof. rewrite /ownI. apply _. Qed.
 
 Lemma ownE_empty : (|==> ownE ∅)%I.
diff --git a/theories/base_logic/primitive.v b/theories/base_logic/primitive.v
index 00389a413..d11139da7 100644
--- a/theories/base_logic/primitive.v
+++ b/theories/base_logic/primitive.v
@@ -97,20 +97,15 @@ 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_plainly_def {M} (P : uPred M) : uPred M :=
-  {| uPred_holds n x := P n ε |}.
-Solve Obligations with naive_solver eauto using uPred_closed, ucmra_unit_validN.
-Definition uPred_plainly_aux : seal (@uPred_plainly_def). by eexists. Qed.
-Definition uPred_plainly {M} := unseal uPred_plainly_aux M.
-Definition uPred_plainly_eq :
-  @uPred_plainly = @uPred_plainly_def := seal_eq uPred_plainly_aux.
-
-Program Definition uPred_always_def {M} (P : uPred M) : uPred M :=
-  {| uPred_holds n x := P n (core x) |}.
+Program Definition uPred_always_def {M} (c : bool) (P : uPred M) : uPred M :=
+  {| uPred_holds n x := P n (if c then core x else ε) |}.
 Next Obligation.
-  intros M; naive_solver eauto using uPred_mono, @cmra_core_monoN.
+  intros M []; naive_solver eauto using uPred_mono, @cmra_core_monoN.
+Qed.
+Next Obligation.
+  intros M []; naive_solver eauto using uPred_closed,
+    @cmra_core_validN, ucmra_unit_validN.
 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 :
@@ -184,10 +179,12 @@ 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_plainly P)
-  (at level 20, right associativity) : uPred_scope.
-Notation "â–¡ P" := (uPred_always P)
+Notation "â–¡{ c } P" := (uPred_always c P)
+  (at level 20, c at next level, right associativity, format "â–¡{ c }  P") : uPred_scope.
+
+Notation "â–¡ P" := (â–¡{true} P)%I
   (at level 20, right associativity) : uPred_scope.
+
 Notation "â–· P" := (uPred_later P)
   (at level 20, right associativity) : uPred_scope.
 Infix "≡" := uPred_internal_eq : uPred_scope.
@@ -209,7 +206,7 @@ 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_plainly_eq, uPred_always_eq, uPred_later_eq, uPred_ownM_eq,
+  uPred_always_eq, uPred_later_eq, uPred_ownM_eq,
   uPred_cmra_valid_eq, uPred_bupd_eq).
 Ltac unseal := rewrite !unseal_eqs /=.
 
@@ -306,20 +303,14 @@ Proof.
 Qed.
 Global Instance later_proper' :
   Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_later M) := ne_proper _.
-Global Instance plainly_ne : NonExpansive (@uPred_plainly M).
-Proof.
-  intros n P1 P2 HP.
-  unseal; split=> n' x; split; apply HP; eauto using @ucmra_unit_validN.
-Qed.
-Global Instance plainly_proper :
-  Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_plainly M) := ne_proper _.
-Global Instance always_ne : NonExpansive (@uPred_always M).
+Global Instance always_ne c : NonExpansive (@uPred_always M c).
 Proof.
   intros n P1 P2 HP.
-  unseal; split=> n' x; split; apply HP; eauto using @cmra_core_validN.
+  unseal; split=> n' x; split; apply HP; destruct c;
+    eauto using @cmra_core_validN, @ucmra_unit_validN.
 Qed.
-Global Instance always_proper :
-  Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_always M) := ne_proper _.
+Global Instance always_proper c :
+  Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_always M c) := ne_proper _.
 Global Instance ownM_ne : NonExpansive (@uPred_ownM M).
 Proof.
   intros n a b Ha.
@@ -439,59 +430,46 @@ Proof.
   eapply HPQR; eauto using cmra_validN_op_l.
 Qed.
 
-(* The plain modality *)
-Lemma plainly_mono P Q : (P ⊢ Q) → ☃ P ⊢ ☃ Q.
-Proof. intros HP; unseal; split=> n x ? /=. apply HP, ucmra_unit_validN. Qed.
-Lemma plainly_elim' P : ☃ P ⊢ □ P.
-Proof. unseal; split; simpl; eauto using uPred_mono, @ucmra_unit_leastN. Qed.
-Lemma plainly_idemp P : ☃ P ⊢ ☃ ☃ P.
-Proof. unseal; split=> n x ?? //. Qed.
-
-Lemma plainly_forall_2 {A} (Ψ : A → uPred M) : (∀ a, ☃ Ψ a) ⊢ (☃ ∀ a, Ψ a).
-Proof. by unseal. Qed.
-Lemma plainly_exist_1 {A} (Ψ : A → uPred M) : (☃ ∃ a, Ψ a) ⊢ (∃ a, ☃ Ψ a).
-Proof. by unseal. Qed.
-
-Lemma prop_ext P Q : ☃ ((P → Q) ∧ (Q → P)) ⊢ P ≡ Q.
+(* The always modality *)
+Lemma always_mono c P Q : (P ⊢ Q) → □{c} P ⊢ □{c} Q.
 Proof.
-  unseal; split=> n x ? /= HPQ; split=> n' x' ? HP;
-    split; eapply HPQ; eauto using @ucmra_unit_least.
+  intros HP; unseal; split=> n x ? /=.
+  apply HP; destruct c; auto using ucmra_unit_validN, cmra_core_validN.
 Qed.
-
-(* Always *)
-Lemma always_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 always_mask_mono P : □{false} P ⊢ □ P.
+Proof. unseal; split; simpl; eauto using uPred_mono, @ucmra_unit_leastN. Qed.
+Lemma always_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.
-Proof. unseal; split=> n x ?? /=. by rewrite cmra_core_idemp. Qed.
+Lemma always_idemp_2 c P : □{c} P ⊢ □{c} □{c} P.
+Proof. unseal; split=> n x ?? //=. destruct c; by rewrite ?cmra_core_idemp. Qed.
 
-Lemma always_forall_2 {A} (Ψ : A → uPred M) : (∀ a, □ Ψ a) ⊢ (□ ∀ a, Ψ a).
+Lemma always_forall_2 {A} c (Ψ : A → uPred M) : (∀ a, □{c} Ψ a) ⊢ (□{c} ∀ a, Ψ a).
 Proof. by unseal. Qed.
-Lemma always_exist_1 {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a) ⊢ (∃ a, □ Ψ a).
+Lemma always_exist_1 {A} c (Ψ : A → uPred M) : (□{c} ∃ a, Ψ a) ⊢ (∃ a, □{c} Ψ a).
 Proof. by unseal. Qed.
 
-Lemma always_and_sep_l_1 P Q : □ P ∧ Q ⊢ □ P ∗ Q.
+Lemma prop_ext P Q : □{false} ((P → Q) ∧ (Q → P)) ⊢ P ≡ Q.
 Proof.
-  unseal; split=> n x ? [??]; exists (core x), x; simpl in *.
-  by rewrite cmra_core_l cmra_core_idemp.
+  unseal; split=> n x ? /= HPQ; split=> n' x' ? HP;
+    split; eapply HPQ; eauto using @ucmra_unit_least.
 Qed.
 
-Lemma always_impl_plainly P Q : (☃ P → □ Q) ⊢ □ (☃ P → Q).
+Lemma always_and_sep_l_1' P Q : □{true} P ∧ Q ⊢ □{true} P ∗ Q.
 Proof.
-  unseal; split=> /= n x ? HPQ n' x' ????.
-  eapply uPred_mono with (core x), cmra_included_includedN; auto.
-  apply (HPQ n' x); eauto using cmra_validN_le.
+  unseal; split=> n x ? [??]; exists (core x), x; simpl in *.
+  by rewrite cmra_core_l cmra_core_idemp.
 Qed.
 
-Lemma plainly_impl_plainly P Q : (☃ P → ☃ Q) ⊢ ☃ (☃ P → Q).
+Lemma always_impl_always c P Q : (□{false} P → □{c} Q) ⊢ □{c} (□{false} P → Q).
 Proof.
-  unseal; split=> /= n x ? HPQ n' x' ????.
-  eapply uPred_mono with ε, cmra_included_includedN; auto.
-  apply (HPQ n' x); eauto using cmra_validN_le.
+  unseal; split=> /= n x ? HPQ n' x' ????. destruct c.
+  - eapply uPred_mono with (core x), cmra_included_includedN; auto.
+    apply (HPQ n' x); eauto using cmra_validN_le.
+  - eapply uPred_mono with ε, cmra_included_includedN; auto.
+    apply (HPQ n' x); eauto using cmra_validN_le.
 Qed.
 
 (* Later *)
@@ -526,9 +504,7 @@ Proof.
   intros [|n'] x' ????; [|done].
   eauto using uPred_closed, uPred_mono, cmra_included_includedN.
 Qed.
-Lemma always_later P : □ ▷ P ⊣⊢ ▷ □ P.
-Proof. by unseal. Qed.
-Lemma plainly_later P : ☃ ▷ P ⊣⊢ ▷ ☃ P.
+Lemma always_later c P : □{c} ▷ P ⊣⊢ ▷ □{c} P.
 Proof. by unseal. Qed.
 
 (* Own *)
@@ -565,7 +541,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 plainly_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ ☃ ✓ a.
+Lemma always_cmra_valid_1' {A : cmraT} (a : A) : ✓ a ⊢ □{false} ✓ 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.
@@ -602,7 +578,7 @@ Proof.
   exists (y â‹… x3); split; first by rewrite -assoc.
   exists y; eauto using cmra_includedN_l.
 Qed.
-Lemma bupd_plainly P : (|==> ☃ P) ⊢ P.
+Lemma bupd_always P : (|==> □{false} P) ⊢ P.
 Proof.
   unseal; split => n x Hnx /= Hng.
   destruct (Hng n ε) as [? [_ Hng']]; try rewrite right_id; auto.
diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index 79112c3fa..b2ff00053 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 : PersistentP true (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 720dcc19a..d2f345218 100644
--- a/theories/heap_lang/lib/lock.v
+++ b/theories/heap_lang/lib/lock.v
@@ -14,7 +14,7 @@ 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);
+  is_lock_persistent N γ lk R : PersistentP true (is_lock N γ lk R);
   locked_timeless γ : TimelessP (locked γ);
   locked_exclusive γ : locked γ -∗ locked γ -∗ False;
   (* -- operation specs -- *)
diff --git a/theories/heap_lang/lib/spin_lock.v b/theories/heap_lang/lib/spin_lock.v
index ea19cf82a..ce0a2c556 100644
--- a/theories/heap_lang/lib/spin_lock.v
+++ b/theories/heap_lang/lib/spin_lock.v
@@ -40,7 +40,7 @@ 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 : PersistentP true (is_lock γ l R).
   Proof. apply _. Qed.
   Global Instance locked_timeless γ : TimelessP (locked γ).
   Proof. apply _. Qed.
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index a926ab2ba..672ccddc5 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -59,7 +59,7 @@ 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 : PersistentP true (is_lock γ lk R).
   Proof. apply _. Qed.
   Global Instance locked_timeless γ : TimelessP (locked γ).
   Proof. apply _. Qed.
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index 7dc6fbe67..af281424d 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -106,10 +106,10 @@ Proof.
   iModIntro; iNext; iMod "H" as ">?". by iApply IH.
 Qed.
 
-Lemma bupd_iter_laterN_mono n P Q `{!PlainP Q} :
+Lemma bupd_iter_laterN_mono n P Q `{!PersistentP false Q} :
   (P ⊢ Q) → Nat.iter n (λ P, |==> ▷ P)%I P ⊢ ▷^n Q.
 Proof.
-  intros HPQ. induction n as [|n IH]=> //=. by rewrite IH bupd_plain.
+  intros HPQ. induction n as [|n IH]=> //=. by rewrite IH bupd_persistent.
 Qed.
 
 Lemma bupd_iter_frame_l n R Q :
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 7c2e77980..da52c78ca 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -19,11 +19,8 @@ Global Instance from_assumption_always_r P Q :
   FromAssumption true P Q → FromAssumption true P (□ Q).
 Proof. rewrite /FromAssumption=><-. by rewrite always_always. Qed.
 
-Global Instance from_assumption_plainly_l p P Q :
-  FromAssumption p P Q → FromAssumption p (☃ P) Q.
-Proof. rewrite /FromAssumption=><-. by rewrite plainly_elim. Qed.
-Global Instance from_assumption_always_l p P Q :
-  FromAssumption p P Q → FromAssumption p (□ P) Q.
+Global Instance from_assumption_always_l p c P Q :
+  FromAssumption p P Q → FromAssumption p (□{c} P) Q.
 Proof. rewrite /FromAssumption=><-. by rewrite always_elim. Qed.
 Global Instance from_assumption_later p P Q :
   FromAssumption p P Q → FromAssumption p P (▷ Q)%I.
@@ -51,9 +48,7 @@ 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_plainly P φ : IntoPure P φ → IntoPure (☃ P) φ.
-Proof. rewrite /IntoPure=> ->. by rewrite plainly_pure. Qed.
-Global Instance into_pure_always P φ : IntoPure P φ → IntoPure (□ P) φ.
+Global Instance into_pure_always c P φ : IntoPure P φ → IntoPure (□{c} P) φ.
 Proof. rewrite /IntoPure=> ->. by rewrite always_pure. Qed.
 
 Global Instance into_pure_pure_and (φ1 φ2 : Prop) P1 P2 :
@@ -102,9 +97,7 @@ Proof.
   rewrite -cmra_valid_intro //. auto with I.
 Qed.
 
-Global Instance from_pure_plainly P φ : FromPure P φ → FromPure (☃ P) φ.
-Proof. rewrite /FromPure=> <-. by rewrite plainly_pure. Qed.
-Global Instance from_pure_always P φ : FromPure P φ → FromPure (□ P) φ.
+Global Instance from_pure_always c P φ : FromPure P φ → FromPure (□{c} P) φ.
 Proof. rewrite /FromPure=> <-. by rewrite always_pure. Qed.
 Global Instance from_pure_later P φ : FromPure P φ → FromPure (▷ P) φ.
 Proof. rewrite /FromPure=> ->. apply later_intro. Qed.
@@ -153,15 +146,9 @@ Proof. rewrite /IntoPersistentP /==> ->. by rewrite always_if_always. Qed.
 Global Instance into_persistentP_always P : IntoPersistentP true P P | 1.
 Proof. done. Qed.
 Global Instance into_persistentP_persistent P :
-  PersistentP P → IntoPersistentP false P P | 100.
+  PersistentP true P → IntoPersistentP false P P | 100.
 Proof. done. Qed.
 
-(* FromPersistentP *)
-Global Instance from_persistentP_always P : FromPersistentP false (â–¡ P) P.
-Proof. by rewrite /FromPersistentP. Qed.
-Global Instance from_persistentP_plainly P : FromPersistentP true (☃ P) P.
-Proof. by rewrite /FromPersistentP. Qed.
-
 (* IntoLater *)
 Global Instance into_laterN_later n P Q :
   IntoLaterN n P Q → IntoLaterN' (S n) (▷ P) Q.
@@ -271,11 +258,8 @@ 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_plainly n P Q :
-  FromLaterN n P Q → FromLaterN n (☃ P) (☃ Q).
-Proof. by rewrite /FromLaterN -plainly_laterN=> ->. Qed.
-Global Instance from_later_always n P Q :
-  FromLaterN n P Q → FromLaterN n (□ P) (□ Q).
+Global Instance from_later_always n c P Q :
+  FromLaterN n P Q → FromLaterN n (□{c} P) (□{c} Q).
 Proof. by rewrite /FromLaterN -always_laterN=> ->. Qed.
 
 Global Instance from_later_forall {A} n (Φ Ψ : A → uPred M) :
@@ -326,11 +310,8 @@ 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_plainly p R P Q :
-  IntoWand p R P Q → IntoWand p (☃ R) P Q.
-Proof. rewrite /IntoWand=> ->. by rewrite plainly_elim. Qed.
-Global Instance into_wand_always p R P Q :
-  IntoWand p R P Q → IntoWand p (□ R) P Q.
+Global Instance into_wand_always p c R P Q :
+  IntoWand p R P Q → IntoWand p (□{c} R) P Q.
 Proof. rewrite /IntoWand=> ->. apply always_elim. Qed.
 
 Global Instance into_wand_later p R P Q :
@@ -358,22 +339,16 @@ 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.
+  PersistentP true 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.
+  PersistentP true 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 ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
 Proof. apply mk_from_and_and. by rewrite pure_and. Qed.
-Global Instance from_and_plainly p P Q1 Q2 :
-  FromAnd false P Q1 Q2 → FromAnd p (☃ P) (☃ Q1) (☃ Q2).
-Proof.
-  intros. apply mk_from_and_and.
-  by rewrite plainly_and_sep_l' -plainly_sep -(from_and _ P).
-Qed.
-Global Instance from_and_always p P Q1 Q2 :
-  FromAnd false P Q1 Q2 → FromAnd p (□ P) (□ Q1) (□ Q2).
+Global Instance from_and_always p c P Q1 Q2 :
+  FromAnd false P Q1 Q2 → FromAnd p (□{c} P) (□{c} Q1) (□{c} Q2).
 Proof.
   intros. apply mk_from_and_and.
   by rewrite always_and_sep_l' -always_sep -(from_and _ P).
@@ -410,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) →
+  PersistentP true (Φ 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.
 
@@ -419,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, PersistentP true (Φ 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.
@@ -455,21 +430,16 @@ 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.
+  PersistentP true 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.
+  PersistentP true 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 ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
 Proof. apply mk_into_and_sep. by rewrite pure_and always_and_sep_r. Qed.
-Global Instance into_and_plainly p P Q1 Q2 :
-  IntoAnd true P Q1 Q2 → IntoAnd p (☃ P) (☃ Q1) (☃ Q2).
-Proof.
-  rewrite /IntoAnd=>->. destruct p; by rewrite ?plainly_and always_and_sep_r.
-Qed.
-Global Instance into_and_always p P Q1 Q2 :
-  IntoAnd true P Q1 Q2 → IntoAnd p (□ P) (□ Q1) (□ Q2).
+Global Instance into_and_always p c P Q1 Q2 :
+  IntoAnd true P Q1 Q2 → IntoAnd p (□{c} P) (□{c} Q1) (□{c} Q2).
 Proof.
   rewrite /IntoAnd=>->. destruct p; by rewrite ?always_and always_and_sep_r.
 Qed.
@@ -653,11 +623,8 @@ 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_plainly P Q1 Q2 :
-  FromOr P Q1 Q2 → FromOr (☃ P) (☃ Q1) (☃ Q2).
-Proof. rewrite /FromOr=> <-. by rewrite plainly_or. Qed.
-Global Instance from_or_always P Q1 Q2 :
-  FromOr P Q1 Q2 → FromOr (□ P) (□ Q1) (□ Q2).
+Global Instance from_or_always c P Q1 Q2 :
+  FromOr P Q1 Q2 → FromOr (□{c} P) (□{c} Q1) (□{c} Q2).
 Proof. rewrite /FromOr=> <-. by rewrite always_or. Qed.
 Global Instance from_or_later P Q1 Q2 :
   FromOr P Q1 Q2 → FromOr (▷ P) (▷ Q1) (▷ Q2).
@@ -674,11 +641,8 @@ 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_plainly P Q1 Q2 :
-  IntoOr P Q1 Q2 → IntoOr (☃ P) (☃ Q1) (☃ Q2).
-Proof. rewrite /IntoOr=>->. by rewrite plainly_or. Qed.
-Global Instance into_or_always P Q1 Q2 :
-  IntoOr P Q1 Q2 → IntoOr (□ P) (□ Q1) (□ Q2).
+Global Instance into_or_always c P Q1 Q2 :
+  IntoOr P Q1 Q2 → IntoOr (□{c} P) (□{c} Q1) (□{c} Q2).
 Proof. rewrite /IntoOr=>->. by rewrite always_or. Qed.
 Global Instance into_or_later P Q1 Q2 :
   IntoOr P Q1 Q2 → IntoOr (▷ P) (▷ Q1) (▷ Q2).
@@ -701,11 +665,8 @@ 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_plainly {A} P (Φ : A → uPred M) :
-  FromExist P Φ → FromExist (☃ P) (λ a, ☃ (Φ a))%I.
-Proof. rewrite /FromExist=> <-. by rewrite plainly_exist. Qed.
-Global Instance from_exist_always {A} P (Φ : A → uPred M) :
-  FromExist P Φ → FromExist (□ P) (λ a, □ (Φ a))%I.
+Global Instance from_exist_always {A} c P (Φ : A → uPred M) :
+  FromExist P Φ → FromExist (□{c} P) (λ a, □{c} (Φ a))%I.
 Proof. rewrite /FromExist=> <-. by rewrite always_exist. Qed.
 Global Instance from_exist_later {A} P (Φ : A → uPred M) :
   FromExist P Φ → FromExist (▷ P) (λ a, ▷ (Φ a))%I.
@@ -727,11 +688,8 @@ 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_plainly {A} P (Φ : A → uPred M) :
-  IntoExist P Φ → IntoExist (☃ P) (λ a, ☃ (Φ a))%I.
-Proof. rewrite /IntoExist=> HP. by rewrite HP plainly_exist. Qed.
-Global Instance into_exist_always {A} P (Φ : A → uPred M) :
-  IntoExist P Φ → IntoExist (□ P) (λ a, □ (Φ a))%I.
+Global Instance into_exist_always {A} c P (Φ : A → uPred M) :
+  IntoExist P Φ → IntoExist (□{c} P) (λ a, □{c} (Φ a))%I.
 Proof. rewrite /IntoExist=> HP. by rewrite HP always_exist. Qed.
 Global Instance into_exist_later {A} P (Φ : A → uPred M) :
   IntoExist P Φ → Inhabited A → IntoExist (▷ P) (λ a, ▷ (Φ a))%I.
@@ -746,11 +704,8 @@ 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_plainly {A} P (Φ : A → uPred M) :
-  IntoForall P Φ → IntoForall (☃ P) (λ a, ☃ (Φ a))%I.
-Proof. rewrite /IntoForall=> HP. by rewrite HP plainly_forall. Qed.
-Global Instance into_forall_always {A} P (Φ : A → uPred M) :
-  IntoForall P Φ → IntoForall (□ P) (λ a, □ (Φ a))%I.
+Global Instance into_forall_always {A} c P (Φ : A → uPred M) :
+  IntoForall P Φ → IntoForall (□{c} P) (λ a, □{c} (Φ a))%I.
 Proof. rewrite /IntoForall=> HP. by rewrite HP always_forall. Qed.
 
 (* FromModal *)
@@ -774,20 +729,19 @@ Proof.
   rewrite /ElimModal=> H. apply forall_intro=> a. by rewrite (forall_elim a).
 Qed.
 
-Global Instance elim_modal_plainly P Q : ElimModal (☃ P) P Q Q.
-Proof. intros. by rewrite /ElimModal plainly_elim wand_elim_r. Qed.
-
-Global Instance elim_modal_always P Q : ElimModal (â–¡ P) P Q Q.
+Global Instance elim_modal_always c P Q : ElimModal (â–¡{c} P) P Q Q.
 Proof. intros. by rewrite /ElimModal always_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.
 
-Global Instance elim_modal_bupd_plain_goal P Q : PlainP Q → ElimModal (|==> P) P Q Q.
-Proof. intros. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_plain. Qed.
+Global Instance elim_modal_bupd_plain_goal P Q :
+  PersistentP false Q → ElimModal (|==> P) P Q Q.
+Proof. intros. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_persistent. Qed.
 
-Global Instance elim_modal_bupd_plain P Q : PlainP P → ElimModal (|==> P) P Q Q.
-Proof. intros. by rewrite /ElimModal bupd_plain wand_elim_r. Qed.
+Global Instance elim_modal_bupd_plain P Q :
+  PersistentP false P → ElimModal (|==> P) P Q Q.
+Proof. intros. by rewrite /ElimModal bupd_persistent wand_elim_r. Qed.
 
 Global Instance elim_modal_except_0 P Q : IsExcept0 Q → ElimModal (◇ P) P Q Q.
 Proof.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 80a5bc024..c9bbe4f26 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -32,11 +32,6 @@ Class IntoPersistentP {M} (p : bool) (P Q : uPred M) :=
 Arguments into_persistentP {_} _ _ _ {_}.
 Hint Mode IntoPersistentP + + ! - : typeclass_instances.
 
-Class FromPersistentP {M} (p : bool) (P Q : uPred M) :=
-  from_persistentP : (if p then ☃ Q else □ Q) ⊢ P.
-Arguments from_persistentP {_} _ _ _ {_}.
-Hint Mode FromPersistentP + - ! - : typeclass_instances.
-
 (* The class [IntoLaterN] has only two instances:
 
 - The default instance [IntoLaterN n P P], i.e. [▷^n P -∗ P]
@@ -100,7 +95,8 @@ 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 (PersistentP true Q1) (PersistentP true 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 bd1a3962c..430f0fd04 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -189,8 +189,8 @@ Proof.
   destruct (envs_lookup_delete_list js rp _) as [[[q2 Ps'] ?]|] eqn:?; simplify_eq/=.
   rewrite always_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 //; 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.
 Qed.
 
@@ -302,7 +302,7 @@ Proof.
 Qed.
 
 Lemma env_spatial_is_nil_persistent Δ :
-  env_spatial_is_nil Δ = true → PersistentP Δ.
+  env_spatial_is_nil Δ = true → PersistentP true Δ.
 Proof. intros; destruct Δ as [? []]; simplify_eq/=; apply _. Qed.
 Hint Immediate env_spatial_is_nil_persistent : typeclass_instances.
 
@@ -467,8 +467,8 @@ 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 -(always_elim true Q) -(löb (□ Q)) -always_later.
+  apply impl_intro_l, (always_intro _ _ _).
   rewrite envs_app_sound //; simpl.
   by rewrite right_id always_and_sep_l' wand_elim_r HQ.
 Qed.
@@ -476,56 +476,53 @@ Qed.
 (** * Always *)
 Class IntoPlainEnv (Γ1 Γ2 : env (uPred M)) := {
   into_plain_env_subenv : env_subenv Γ2 Γ1;
-  into_plain_env_plain : PlainP ([∗] Γ2);
+  into_plain_env_plain : PersistentP false ([∗] Γ2);
 }.
 Class IntoPersistentEnvs (p : bool) (Δ1 Δ2 : envs M) := {
   into_persistent_envs_persistent :
-    if p then IntoPlainEnv (env_persistent Δ1) (env_persistent Δ2)
-    else env_persistent Δ1 = env_persistent Δ2;
+    if p then env_persistent Δ1 = env_persistent Δ2
+    else IntoPlainEnv (env_persistent Δ1) (env_persistent Δ2);
   into_persistent_envs_spatial : env_spatial Δ2 = Enil
 }.
 
 Global Instance into_plain_env_nil : IntoPlainEnv Enil Enil.
 Proof. constructor. constructor. simpl; apply _. Qed.
 Global Instance into_plain_env_snoc_plain Γ1 Γ2 i P :
-  PlainP P → IntoPlainEnv Γ1 Γ2 →
+  PersistentP false P → IntoPlainEnv Γ1 Γ2 →
   IntoPlainEnv (Esnoc Γ1 i P) (Esnoc Γ2 i P) | 1.
 Proof. intros ? [??]; constructor. by constructor. simpl; apply _. Qed.
 Global Instance into_plain_env_snoc_skip Γ1 Γ2 i P :
   IntoPlainEnv Γ1 Γ2 → IntoPlainEnv (Esnoc Γ1 i P) Γ2 | 2.
 Proof. intros [??]; constructor. by constructor. done. Qed.
 
-Global Instance into_persistent_envs_false Γp Γs :
-  IntoPersistentEnvs false (Envs Γp Γs) (Envs Γp Enil).
+Global Instance into_persistent_envs_true Γp Γs :
+  IntoPersistentEnvs true (Envs Γp Γs) (Envs Γp Enil).
 Proof. by split. Qed.
-Global Instance into_persistent_envs_true Γp1 Γp2 Γs1 :
+Global Instance into_persistent_envs_false Γp1 Γp2 Γs1 :
   IntoPlainEnv Γp1 Γp2 →
-  IntoPersistentEnvs true (Envs Γp1 Γs1) (Envs Γp2 Enil).
+  IntoPersistentEnvs false (Envs Γp1 Γs1) (Envs Γp2 Enil).
 Proof. by split. Qed.
 
-Lemma into_persistent_envs_sound (p : bool) Δ1 Δ2 :
-  IntoPersistentEnvs p Δ1 Δ2 → Δ1 ⊢ (if p then ☃ Δ2 else □ Δ2).
+Lemma into_persistent_envs_sound c Δ1 Δ2 :
+  IntoPersistentEnvs c Δ1 Δ2 → Δ1 ⊢ □{c} Δ2.
 Proof.
   rewrite /of_envs. destruct Δ1 as [Γp1 Γs1], Δ2 as [Γp2 Γs2]=> -[/= Hp ->].
-  apply pure_elim_sep_l=> Hwf. rewrite sep_elim_l. destruct p; simplify_eq/=.
-  - destruct Hp. rewrite right_id plainly_sep plainly_pure.
-    apply sep_intro_True_l; [apply pure_intro|].
+  apply pure_elim_sep_l=> Hwf /=.
+  rewrite sep_elim_l right_id always_sep always_pure. destruct c; simplify_eq/=.
+  - apply sep_intro_True_l; [apply pure_intro|].
+    destruct Hwf; constructor; simpl; eauto using Enil_wf.
+    by rewrite always_idemp.
+  - destruct Hp. apply sep_intro_True_l; [apply pure_intro|].
     + destruct Hwf; constructor; eauto using Enil_wf, env_subenv_wf.
-    + rewrite always_elim plainly_always plainly_plainly.
+    + rewrite always_idemp'' -(always_idemp' false) (always_always false).
+      apply always_mono.
       by apply big_sepL_submseteq, sublist_submseteq, env_to_list_subenv_proper.
-  - rewrite right_id always_sep always_pure.
-    apply sep_intro_True_l; [apply pure_intro|by rewrite always_always].
-    destruct Hwf; constructor; simpl; eauto using Enil_wf.
 Qed.
 
-Lemma tac_always_intro Δ Δ' p Q Q' :
-  FromPersistentP p Q' Q →
-  IntoPersistentEnvs p Δ Δ' →
-  (Δ' ⊢ Q) → Δ ⊢ Q'.
-Proof.
-  intros ?? HQ. rewrite into_persistent_envs_sound -(from_persistentP _ Q').
-  destruct p; auto using always_mono, plainly_mono.
-Qed.
+Lemma tac_always_intro Δ Δ' c Q :
+  IntoPersistentEnvs c Δ Δ' →
+  (Δ' ⊢ Q) → Δ ⊢ □{c} Q.
+Proof. intros ? <-. by rewrite into_persistent_envs_sound. Qed.
 
 Lemma tac_persistent Δ Δ' i p P P' Q :
   envs_lookup i Δ = Some (p, P) →
@@ -539,12 +536,12 @@ 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 PersistentP true 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 (persistentP true Δ) 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.
@@ -660,22 +657,22 @@ 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 → PersistentP true 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 (persistentP _ 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.
+  rewrite right_id (into_wand _ R) (always_elim_if _ q) -always_if_sep wand_elim_l.
   by rewrite wand_elim_r.
 Qed.
 
 Lemma tac_specialize_persistent_helper Δ Δ' j q P R Q :
   envs_lookup j Δ = Some (q,P) →
-  (Δ ⊢ R) → PersistentP R →
+  (Δ ⊢ R) → PersistentP true R →
   envs_replace j q true (Esnoc Enil j R) Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
@@ -711,7 +708,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}(persistentP true Δ) {1}HP // HPQ impl_elim_r.
 Qed.
 
 Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P P' Q :
@@ -728,7 +725,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 →
+  PersistentP true 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 ded603032..0797a5fa4 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -808,10 +808,8 @@ Local Tactic Notation "iExistDestruct" constr(H)
 (** * Always *)
 Tactic Notation "iAlways":=
   iStartProof;
-  eapply tac_always_intro;
-    [apply _ || fail "iAlways: the goal is not an always modality"
-    |env_cbv; apply _
-    |].
+  eapply tac_always_intro; [env_cbv; apply _|]
+    || fail "iAlways: the goal is not an always modality".
 
 (** * Later *)
 Tactic Notation "iNext" open_constr(n) :=
@@ -1722,8 +1720,7 @@ Hint Extern 0 (_ ⊢ _) => progress iIntros.
 Hint Extern 1 (of_envs _ ⊢ _ ∧ _) => iSplit.
 Hint Extern 1 (of_envs _ ⊢ _ ∗ _) => iSplit.
 Hint Extern 1 (of_envs _ ⊢ ▷ _) => iNext.
-Hint Extern 1 (of_envs _ ⊢ □ _) => iAlways.
-Hint Extern 1 (of_envs _ ⊢ ☃ _) => iAlways.
+Hint Extern 1 (of_envs _ ⊢ □{_} _) => iAlways.
 Hint Extern 1 (of_envs _ ⊢ ∃ _, _) => iExists _.
 Hint Extern 1 (of_envs _ ⊢ |==> _) => iModIntro.
 Hint Extern 1 (of_envs _ ⊢ ◇ _) => iModIntro.
diff --git a/theories/tests/ipm_paper.v b/theories/tests/ipm_paper.v
index 5896d6391..7d6166fc2 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 : PersistentP true (C l n).
   Proof. apply _. Qed.
 
   Lemma newcounter_spec :
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 28e615223..686b10eef 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 `{!PersistentP true 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 `{!PersistentP true 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 `{!PersistentP true R} :
   P -∗ Q -∗ R -∗ R ∗ Q ∗ P ∗ R ∨ False.
 Proof. iIntros "HP HQ #HR". iCombine "HR HQ HP HR" as "H". auto. Qed.
 
-- 
GitLab