diff --git a/theories/base_logic/big_op.v b/theories/base_logic/big_op.v
index 5eac49b7c4fb40a49add52f4005f671f213d0fe7..ade91f52da266a9fff66d84c69920946a4b71a8b 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 true (Φ k x)) →
+    (∀ k x, PersistentP Weak (Φ k x)) →
     ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ (∀ k x, ⌜l !! k = Some x⌝ → Φ k x).
   Proof.
     intros HΦ. apply (anti_symm _).
@@ -316,7 +316,7 @@ Section gmap.
   Proof. apply (big_opM_commute _). Qed.
 
   Lemma big_sepM_forall Φ m :
-    (∀ k x, PersistentP true (Φ k x)) →
+    (∀ k x, PersistentP Weak (Φ k x)) →
     ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ (∀ k x, ⌜m !! k = Some x⌝ → Φ k x).
   Proof.
     intros. apply (anti_symm _).
@@ -468,7 +468,7 @@ Section gset.
   Proof. apply (big_opS_commute _). Qed.
 
   Lemma big_sepS_forall Φ X :
-    (∀ x, PersistentP true (Φ x)) → ([∗ set] x ∈ X, Φ x) ⊣⊢ (∀ x, ⌜x ∈ X⌝ → Φ x).
+    (∀ x, PersistentP Weak (Φ x)) → ([∗ set] x ∈ X, Φ x) ⊣⊢ (∀ x, ⌜x ∈ X⌝ → Φ x).
   Proof.
     intros. apply (anti_symm _).
     { apply forall_intro=> x.
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 81c79423e20a290a9a4aaa90ccbccf740bd19161..cc1e5bd4bb77f26a2695e8c0d7234e5ead741ee4 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -16,13 +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} (c p : bool) (P : uPred M) : uPred M :=
+Definition uPred_always_if {M} (c : strength) (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 "â–¡{ 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)
+Notation "â–¡? p P" := (uPred_always_if Weak 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.
@@ -36,7 +36,7 @@ Arguments timelessP {_} _ {_}.
 Hint Mode TimelessP + ! : typeclass_instances.
 Instance: Params (@TimelessP) 1.
 
-Class PersistentP {M} (c : bool) (P : uPred M) := persistentP : P ⊢ □{c} P.
+Class PersistentP {M} (c : strength) (P : uPred M) := persistentP : P ⊢ □{c} P.
 Arguments persistentP {_} _ _ {_}.
 Hint Mode PersistentP + + ! : typeclass_instances.
 Instance: Params (@PersistentP) 2.
@@ -743,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 true) -always_later -always_sep_dup'.
+    by rewrite -!or_intro_l -(always_pure Weak) -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.
@@ -840,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 true) -always_later always_and_sep_l'.
+  rewrite -(always_pure Weak) -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) :
@@ -885,7 +885,7 @@ Global Instance limit_preserving_PersistentP
   NonExpansive Φ → LimitPreserving (λ x, PersistentP c (Φ x)).
 Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
 
-Lemma persistent_mask_weaken P : PersistentP false P → PersistentP true P.
+Lemma persistent_strength_weaken P : PersistentP Strong P → PersistentP Weak P.
 Proof. rewrite /PersistentP=> HP. by rewrite {1}HP always_mask_mono. Qed.
 
 Lemma always_always c P `{!PersistentP c P} : □{c} P ⊣⊢ P.
@@ -894,43 +894,43 @@ 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 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).
+Lemma always_and_sep_l P Q `{!PersistentP Weak P} : P ∧ Q ⊣⊢ P ∗ Q.
+Proof. by rewrite -(always_always Weak P) always_and_sep_l'. Qed.
+Lemma always_and_sep_r P Q `{!PersistentP Weak Q} : P ∧ Q ⊣⊢ P ∗ Q.
+Proof. by rewrite -(always_always Weak Q) always_and_sep_r'. Qed.
+Lemma always_sep_dup P `{!PersistentP Weak P} : P ⊣⊢ P ∗ P.
+Proof. by rewrite -(always_always Weak P) -always_sep_dup'. Qed.
+Lemma always_entails_l P Q `{!PersistentP Weak Q} : (P ⊢ Q) → P ⊢ Q ∗ P.
+Proof. by rewrite -(always_always Weak Q); apply always_entails_l'. Qed.
+Lemma always_entails_r P Q `{!PersistentP Weak Q} : (P ⊢ Q) → P ⊢ P ∗ Q.
+Proof. by rewrite -(always_always Weak Q); apply always_entails_r'. Qed.
+Lemma always_impl_wand P `{!PersistentP Weak 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.
 
-Lemma bupd_persistent P `{!PersistentP false P} : (|==> P) ⊢ P.
-Proof. by rewrite -{1}(always_always false P) bupd_always. Qed.
+Lemma bupd_persistent P `{!PersistentP Strong P} : (|==> P) ⊢ P.
+Proof. by rewrite -{1}(always_always Strong P) bupd_always. Qed.
 
 (* Persistence *)
 Global Instance pure_persistent c φ : PersistentP c (⌜φ⌝ : uPred M)%I.
 Proof. by rewrite /PersistentP always_pure. Qed.
 Global Instance impl_persistent c P Q :
-  PersistentP false P → PersistentP c Q → PersistentP c (P → Q).
+  PersistentP Strong P → PersistentP c Q → PersistentP c (P → Q).
 Proof.
   rewrite /PersistentP=> HP HQ.
   rewrite {2}HP -always_impl_always. by rewrite -HQ always_elim.
 Qed.
 Global Instance wand_persistent c P Q :
-  PersistentP false P → PersistentP c Q → PersistentP c (P -∗ Q)%I.
+  PersistentP Strong P → PersistentP c Q → PersistentP c (P -∗ Q)%I.
 Proof.
   rewrite /PersistentP=> HP HQ.
-  by rewrite {2}HP -{1}(always_elim false P) !wand_impl_always -always_impl_always -HQ.
+  by rewrite {2}HP -{1}(always_elim Strong P) !wand_impl_always -always_impl_always -HQ.
 Qed.
 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).
+Global Instance always_persistent' c P : PersistentP Weak (â–¡{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).
@@ -959,7 +959,7 @@ Global Instance except_0_persistent c P : PersistentP c P → PersistentP c (◇
 Proof. by intros; rewrite /PersistentP -except_0_always; apply except_0_mono. Qed.
 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 true (@uPred_ownM M a).
+Global Instance ownM_persistent : Persistent a → PersistentP Weak (@uPred_ownM M a).
 Proof. intros. by rewrite /PersistentP always_ownM. Qed.
 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).
@@ -1033,4 +1033,4 @@ 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.persistent_mask_weaken : typeclass_instances.
+Hint Immediate uPred.persistent_strength_weaken : typeclass_instances.
diff --git a/theories/base_logic/lib/auth.v b/theories/base_logic/lib/auth.v
index 67b9ac7dc56461a8ca52c20e9353bb4dec440090..b33e4f060ee55a923b67edb97829e96cc9d2365d 100644
--- a/theories/base_logic/lib/auth.v
+++ b/theories/base_logic/lib/auth.v
@@ -33,7 +33,7 @@ Section definitions.
   Global Instance auth_own_timeless a : TimelessP (auth_own a).
   Proof. apply _. Qed.
   Global Instance auth_own_persistent a :
-    Persistent a → PersistentP true (auth_own a).
+    Persistent a → PersistentP Weak (auth_own a).
   Proof. apply _. Qed.
 
   Global Instance auth_inv_ne n :
@@ -52,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 true (auth_ctx N f φ).
+  Global Instance auth_ctx_persistent N f φ : PersistentP Weak (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 4a3091b1bda2041e4739681e6f396769c106dce4..addc138b3be447f571d40afe5a422b303c3d8817 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 true (slice N γ P).
+Global Instance slice_persistent γ P : PersistentP Weak (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 7fda48d80c83a3a60a4725cd77e1bcd71aa17c81..d68dfae8e5dc359ff3e623d3b4d58663d39122e1 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 true (cinv N γ P).
+  Global Instance cinv_persistent N γ P : PersistentP Weak (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 1c13517107c4afe6701861936fbea8a5173c1928..31d700f00e487bd4e298178e3b51a65dfe35f31f 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, □{false} (Q → □ Q) → □{false} (P → Q) → Q)%I.
+  (∀ Q, □{Strong} (Q → □ Q) → □{Strong} (P → Q) → Q)%I.
 Instance: Params (@coreP) 1.
 Typeclasses Opaque coreP.
 
@@ -16,7 +16,7 @@ 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 true (coreP P).
+  Global Instance coreP_persistent P : PersistentP Weak (coreP P).
   Proof.
     rewrite /coreP /PersistentP. iIntros "HC".
     iApply always_forall. iIntros (Q). (* FIXME: iIntros should apply always_forall automatically. *)
@@ -36,7 +36,7 @@ Section core.
     iApply ("H" $! Q with "[]"); first done. by rewrite HP.
   Qed.
 
-  Lemma coreP_elim P : PersistentP true P → coreP P -∗ P.
+  Lemma coreP_elim P : PersistentP Weak P → coreP P -∗ P.
   Proof. rewrite /coreP. iIntros (?) "HCP". iApply ("HCP" $! P); auto. Qed.
 
   Lemma coreP_wand P Q : (coreP P ⊢ Q) ↔ (P ⊢ □ Q).
diff --git a/theories/base_logic/lib/counter_examples.v b/theories/base_logic/lib/counter_examples.v
index 8975da9cb84b550a60d64c52a6f7ded468431f0e..fe06dce504f8a576e437b4ebaf1cddd06edff38e 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 true (saved i P).
+  Hypothesis sprop_persistent : ∀ i P, PersistentP Weak (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 true (inv i P).
+  Hypothesis inv_persistent : ∀ i P, PersistentP Weak (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 true (saved γ P) := _.
+  Global Instance saved_persistent γ P : PersistentP Weak (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 true (A i) := _.
+  Global Instance A_persistent i : PersistentP Weak (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 da372ddd1c314b6e58bdbc7b2015a8c9d49dabdf..1199bbb056bbe1898b8c02b80f7c021ddf3821ed 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_persistent' {E1 E2 E2'} P Q `{!PersistentP false P} :
+Lemma fupd_persistent' {E1 E2 E2'} P Q `{!PersistentP Strong P} :
   E1 ⊆ E2 →
   (Q ={E1, E2'}=∗ P) → (|={E1, E2}=> Q) ⊢ |={E1}=> ((|={E1, E2}=> Q) ∗ P).
 Proof.
@@ -159,7 +159,7 @@ Proof.
   iModIntro; iFrame; auto.
 Qed.
 
-Lemma fupd_plain {E1 E2} P Q `{!PersistentP false P} :
+Lemma fupd_plain {E1 E2} P Q `{!PersistentP Strong P} :
   E1 ⊆ E2 → (Q ⊢ P) → (|={E1, E2}=> Q) ⊢ |={E1}=> ((|={E1, E2}=> Q) ∗ P).
 Proof.
   iIntros (HE HQP) "HQ".
@@ -167,7 +167,7 @@ Proof.
   by iIntros "?"; iApply fupd_intro; iApply HQP.
 Qed.
 
-Lemma later_fupd_plain {E} P `{Hpl: !PersistentP false P} :
+Lemma later_fupd_plain {E} P `{Hpl: !PersistentP Strong P} :
   (▷ |={E}=> P) ⊢ |={E}=> ▷ ◇ P.
 Proof.
   iIntros "HP". rewrite fupd_eq /fupd_def.
diff --git a/theories/base_logic/lib/fancy_updates_from_vs.v b/theories/base_logic/lib/fancy_updates_from_vs.v
index bf27ce2fae0ba2a4cbe6aadc17f09c888525c8fb..3e31d2cc3533ba20d0aaa95385a3fe6095ac1427 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 true (P ={E1,E2}=> Q)).
+Context (vs_persistent : ∀ E1 E2 P Q, PersistentP Weak (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 true R →
+  PersistentP Weak 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 6bcc01f705df827e2f924722b81df6ce256ec3a1..3884a49baa6c7381804f3dede47bda984b9db323 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 true P → Fractional (λ _, P).
+    PersistentP Weak 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 664494284a5595c1430e800ca8fd4a35ee6bd56b..5b7ed8e751c16b2831b60b6c8ec9a7841e66514e 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 true (inv N P).
+Global Instance inv_persistent N P : PersistentP Weak (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 d477ea58d88f270f45d653a06e775ea7060c8ce6..4deb1462ca18da4834861465c34e1b1fdf36d75e 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 true (na_inv p N P).
+  Global Instance na_inv_persistent p N P : PersistentP Weak (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 7c456426079c4b00be3dd12ee9a9f5bc06a2b4ce..bfd6249c1db0dd3d7584cd89d8ff5b9285ef2355 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 true (own γ a).
+Global Instance own_core_persistent γ a : Persistent a → PersistentP Weak (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 04d85dbf394cf6bf92e1ddd6edb0918282b03ac6..f4580b421581e871feb0bf1ed4035f35141865b9 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -24,7 +24,7 @@ Section saved_prop.
   Implicit Types γ : gname.
 
   Global Instance saved_prop_persistent γ x :
-    PersistentP true (saved_prop_own γ x).
+    PersistentP Weak (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 9d7fde93cdd828baeedef1c3c94a61fa859b14b0..9d0f7ca2e3b87f74622e8fac7691721076a05998 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 true (sts_ctx N φ).
+  Global Instance sts_ctx_persistent `{!invG Σ} N φ : PersistentP Weak (sts_ctx N φ).
   Proof. apply _. Qed.
-  Global Instance sts_own_persistent s : PersistentP true (sts_own s ∅).
+  Global Instance sts_own_persistent s : PersistentP Weak (sts_own s ∅).
   Proof. apply _. Qed.
-  Global Instance sts_ownS_persistent S : PersistentP true (sts_ownS S ∅).
+  Global Instance sts_ownS_persistent S : PersistentP Weak (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 dfe5c6b2b6e9419e874aa076f4b6ca0c1d513731..782d0b5d1765716235a63e151084125aaf47f99c 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 true (ownI i P).
+Global Instance ownI_persistent i P : PersistentP Weak (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 d11139da7d34b3425c2dfed89beeafdff66183c8..d232e2fe86df07fd0fea7216493c7c372ab1fc16 100644
--- a/theories/base_logic/primitive.v
+++ b/theories/base_logic/primitive.v
@@ -97,8 +97,9 @@ Definition uPred_wand {M} := unseal uPred_wand_aux M.
 Definition uPred_wand_eq :
   @uPred_wand = @uPred_wand_def := seal_eq uPred_wand_aux.
 
-Program Definition uPred_always_def {M} (c : bool) (P : uPred M) : uPred M :=
-  {| uPred_holds n x := P n (if c then core x else ε) |}.
+Inductive strength := Weak | Strong.
+Program Definition uPred_always_def {M} (c : strength) (P : uPred M) : uPred M :=
+  {| uPred_holds n x := P n (if c is Weak return _ then core x else ε) |}.
 Next Obligation.
   intros M []; naive_solver eauto using uPred_mono, @cmra_core_monoN.
 Qed.
@@ -181,10 +182,8 @@ Notation "∃ x .. y , P" :=
   (at level 200, x binder, y binder, right associativity) : uPred_scope.
 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
+Notation "â–¡ P" := (â–¡{Weak} 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.
@@ -436,7 +435,7 @@ Proof.
   intros HP; unseal; split=> n x ? /=.
   apply HP; destruct c; auto using ucmra_unit_validN, cmra_core_validN.
 Qed.
-Lemma always_mask_mono P : □{false} P ⊢ □ P.
+Lemma always_mask_mono P : □{Strong} P ⊢ □ P.
 Proof. unseal; split; simpl; eauto using uPred_mono, @ucmra_unit_leastN. Qed.
 Lemma always_elim' P : □ P ⊢ P.
 Proof.
@@ -451,19 +450,19 @@ Proof. by unseal. Qed.
 Lemma always_exist_1 {A} c (Ψ : A → uPred M) : (□{c} ∃ a, Ψ a) ⊢ (∃ a, □{c} Ψ a).
 Proof. by unseal. Qed.
 
-Lemma prop_ext P Q : □{false} ((P → Q) ∧ (Q → P)) ⊢ P ≡ Q.
+Lemma prop_ext P Q : □{Strong} ((P → Q) ∧ (Q → P)) ⊢ P ≡ Q.
 Proof.
   unseal; split=> n x ? /= HPQ; split=> n' x' ? HP;
     split; eapply HPQ; eauto using @ucmra_unit_least.
 Qed.
 
-Lemma always_and_sep_l_1' P Q : □{true} P ∧ Q ⊢ □{true} P ∗ Q.
+Lemma always_and_sep_l_1' P Q : □ P ∧ Q ⊢ □ P ∗ Q.
 Proof.
   unseal; split=> n x ? [??]; exists (core x), x; simpl in *.
   by rewrite cmra_core_l cmra_core_idemp.
 Qed.
 
-Lemma always_impl_always c P Q : (□{false} P → □{c} Q) ⊢ □{c} (□{false} P → Q).
+Lemma always_impl_always c P Q : (□{Strong} P → □{c} Q) ⊢ □{c} (□{Strong} P → Q).
 Proof.
   unseal; split=> /= n x ? HPQ n' x' ????. destruct c.
   - eapply uPred_mono with (core x), cmra_included_includedN; auto.
@@ -541,7 +540,7 @@ Lemma cmra_valid_intro {A : cmraT} (a : A) : ✓ a → uPred_valid (M:=M) (✓ a
 Proof. unseal=> ?; split=> n x ? _ /=; by apply cmra_valid_validN. Qed.
 Lemma cmra_valid_elim {A : cmraT} (a : A) : ¬ ✓{0} a → ✓ a ⊢ False.
 Proof. unseal=> Ha; split=> n x ??; apply Ha, cmra_validN_le with n; auto. Qed.
-Lemma always_cmra_valid_1' {A : cmraT} (a : A) : ✓ a ⊢ □{false} ✓ a.
+Lemma always_cmra_valid_1' {A : cmraT} (a : A) : ✓ a ⊢ □{Strong} ✓ 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.
@@ -578,7 +577,7 @@ Proof.
   exists (y â‹… x3); split; first by rewrite -assoc.
   exists y; eauto using cmra_includedN_l.
 Qed.
-Lemma bupd_always P : (|==> □{false} P) ⊢ P.
+Lemma bupd_always P : (|==> □{Strong} 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 b2ff000533fb4ce226459059afe1f2e66ade0800..45ac68697f145cf8daa1a049e390d6a08c0d7268 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 true (mcounter l n).
+  Global Instance mcounter_persistent l n : PersistentP Weak (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 d2f345218d428f21fec494a19b830bfd0ee4f72c..e8708c623a0cf984732f8ee8bc680ba09d24047a 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 true (is_lock N γ lk R);
+  is_lock_persistent N γ lk R : PersistentP Weak (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 ce0a2c556758578c227f8174618e0d85af51a42c..2b53d0d7faf3039a281b7677616fd5cb78113afe 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 true (is_lock γ l R).
+  Global Instance is_lock_persistent γ l R : PersistentP Weak (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 672ccddc5fa90ac1031048b012d85dc98a3d2967..fbd3262461cfe345b32be86c32af990bcba1088d 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 true (is_lock γ lk R).
+  Global Instance is_lock_persistent γ lk R : PersistentP Weak (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 af281424dd8e720e57fc79b17f097c3a877d1475..0d82ecfb7abccc89af8fc2f2b1e2987468a9e556 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -106,7 +106,7 @@ Proof.
   iModIntro; iNext; iMod "H" as ">?". by iApply IH.
 Qed.
 
-Lemma bupd_iter_laterN_mono n P Q `{!PersistentP false Q} :
+Lemma bupd_iter_laterN_mono n P Q `{!PersistentP Strong Q} :
   (P ⊢ Q) → Nat.iter n (λ P, |==> ▷ P)%I P ⊢ ▷^n Q.
 Proof.
   intros HPQ. induction n as [|n IH]=> //=. by rewrite IH bupd_persistent.
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index da52c78ca671dbbe954bfda1830c8b14eccd935a..25f4e7ede745a677cf31aab8c677c8e5d8af451b 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -146,7 +146,7 @@ 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 true P → IntoPersistentP false P P | 100.
+  PersistentP Weak P → IntoPersistentP 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 true P1 → FromAnd true (P1 ∗ P2) P1 P2 | 9.
+  PersistentP Weak 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 true P2 → FromAnd true (P1 ∗ P2) P1 P2 | 10.
+  PersistentP Weak 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 true (Φ 0 x) →
+  PersistentP Weak (Φ 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 true (Φ k y)) →
+  (∀ k y, PersistentP Weak (Φ 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 true P → IntoAnd false (P ∧ Q) P Q.
+  PersistentP Weak 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 true Q → IntoAnd false (P ∧ Q) P Q.
+  PersistentP Weak 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 ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
@@ -736,11 +736,11 @@ 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 :
-  PersistentP false Q → ElimModal (|==> P) P Q Q.
+  PersistentP Strong 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 :
-  PersistentP false P → ElimModal (|==> P) P Q Q.
+  PersistentP Strong 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.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index c9bbe4f26109788a4a7e5f1b7205faa0e4627c75..44e3ff4cbdecd04a256273a0503727a7f6483d8d 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -95,7 +95,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 true Q1) (PersistentP true Q2) →
+  Or (PersistentP Weak Q1) (PersistentP Weak Q2) →
   (Q1 ∗ Q2 ⊢ P) → FromAnd true P Q1 Q2.
 Proof.
   intros [?|?] ?; rewrite /FromAnd.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 430f0fd0457d38cb1986b151e9d3d231c738b1fe..8fb3cedf7c7e1afc2dde3b36d9450c86a13e05c6 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 true Δ.
+  env_spatial_is_nil Δ = true → PersistentP Weak Δ.
 Proof. intros; destruct Δ as [? []]; simplify_eq/=; apply _. Qed.
 Hint Immediate env_spatial_is_nil_persistent : typeclass_instances.
 
@@ -467,7 +467,7 @@ Lemma tac_löb Δ Δ' i Q :
   envs_app true (Esnoc Enil i (▷ Q)%I) Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
-  intros ?? HQ. rewrite -(always_elim true Q) -(löb (□ Q)) -always_later.
+  intros ?? HQ. rewrite -(always_elim Weak 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.
@@ -476,11 +476,11 @@ Qed.
 (** * Always *)
 Class IntoPlainEnv (Γ1 Γ2 : env (uPred M)) := {
   into_plain_env_subenv : env_subenv Γ2 Γ1;
-  into_plain_env_plain : PersistentP false ([∗] Γ2);
+  into_plain_env_plain : PersistentP Strong ([∗] Γ2);
 }.
-Class IntoPersistentEnvs (p : bool) (Δ1 Δ2 : envs M) := {
+Class IntoPersistentEnvs (c : strength) (Δ1 Δ2 : envs M) := {
   into_persistent_envs_persistent :
-    if p then env_persistent Δ1 = env_persistent Δ2
+    if c is Weak then env_persistent Δ1 = env_persistent Δ2
     else IntoPlainEnv (env_persistent Δ1) (env_persistent Δ2);
   into_persistent_envs_spatial : env_spatial Δ2 = Enil
 }.
@@ -488,19 +488,19 @@ Class IntoPersistentEnvs (p : bool) (Δ1 Δ2 : envs M) := {
 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 :
-  PersistentP false P → IntoPlainEnv Γ1 Γ2 →
+  PersistentP Strong 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_true Γp Γs :
-  IntoPersistentEnvs true (Envs Γp Γs) (Envs Γp Enil).
+Global Instance into_persistent_envs_weak Γp Γs :
+  IntoPersistentEnvs Weak (Envs Γp Γs) (Envs Γp Enil).
 Proof. by split. Qed.
-Global Instance into_persistent_envs_false Γp1 Γp2 Γs1 :
+Global Instance into_persistent_envs_strong Γp1 Γp2 Γs1 :
   IntoPlainEnv Γp1 Γp2 →
-  IntoPersistentEnvs false (Envs Γp1 Γs1) (Envs Γp2 Enil).
+  IntoPersistentEnvs Strong (Envs Γp1 Γs1) (Envs Γp2 Enil).
 Proof. by split. Qed.
 
 Lemma into_persistent_envs_sound c Δ1 Δ2 :
@@ -514,7 +514,7 @@ Proof.
     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_idemp'' -(always_idemp' false) (always_always false).
+    + rewrite always_idemp'' -(always_idemp' Strong) (always_always Strong).
       apply always_mono.
       by apply big_sepL_submseteq, sublist_submseteq, env_to_list_subenv_proper.
 Qed.
@@ -536,12 +536,12 @@ Qed.
 
 (** * Implication and wand *)
 Lemma tac_impl_intro Δ Δ' i P Q :
-  (if env_spatial_is_nil Δ then TCTrue else PersistentP true P) →
+  (if env_spatial_is_nil Δ then TCTrue else PersistentP Weak P) →
   envs_app false (Esnoc Enil i P) Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ P → Q.
 Proof.
   intros ?? <-. destruct (env_spatial_is_nil Δ) eqn:?.
-  - rewrite (persistentP true Δ) envs_app_sound //; simpl.
+  - rewrite (persistentP Weak Δ) 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.
@@ -657,7 +657,7 @@ 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 true P1 →
+  IntoWand false R P1 P2 → PersistentP Weak P1 →
   envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'' →
   (Δ' ⊢ P1) → (Δ'' ⊢ Q) → Δ ⊢ Q.
 Proof.
@@ -672,7 +672,7 @@ Qed.
 
 Lemma tac_specialize_persistent_helper Δ Δ' j q P R Q :
   envs_lookup j Δ = Some (q,P) →
-  (Δ ⊢ R) → PersistentP true R →
+  (Δ ⊢ R) → PersistentP Weak R →
   envs_replace j q true (Esnoc Enil j R) Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
@@ -708,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 true Δ) {1}HP // HPQ impl_elim_r.
+  by rewrite -(idemp uPred_and Δ) {1}(persistentP Weak Δ) {1}HP // HPQ impl_elim_r.
 Qed.
 
 Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P P' Q :
@@ -725,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 true P →
+  PersistentP Weak P →
   (Δ1 ⊢ P) → (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros ??? HP <-. rewrite -(idemp uPred_and Δ) {1}envs_split_sound //.
diff --git a/theories/tests/ipm_paper.v b/theories/tests/ipm_paper.v
index 7d6166fc21b0833e8d29b2af48442f18ca9dfd21..d6f566df940244f2ccbd3e93c059e97f396d2231 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 true (C l n).
+  Global Instance C_persistent l n : PersistentP Weak (C l n).
   Proof. apply _. Qed.
 
   Lemma newcounter_spec :
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 686b10eef40facb5eaf373feedc87ba69ffdb306..ace2531174888a4274af4e41e2eedfaff805d8c1 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 true Q} : (P → Q → P ∗ Q)%I.
+Lemma test_iIntros_persistent P Q `{!PersistentP Weak 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 true R} :
+Lemma test_eauto_iFramE P Q R `{!PersistentP Weak R} :
   P -∗ Q -∗ R -∗ R ∗ Q ∗ P ∗ R ∨ False.
 Proof. eauto with iFrame. Qed.
 
-Lemma test_iCombine_persistent P Q R `{!PersistentP true R} :
+Lemma test_iCombine_persistent P Q R `{!PersistentP Weak R} :
   P -∗ Q -∗ R -∗ R ∗ Q ∗ P ∗ R ∨ False.
 Proof. iIntros "HP HQ #HR". iCombine "HR HQ HP HR" as "H". auto. Qed.