diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 7389de3a62168f6089396f3a8fad480e160c4c00..8ac0024a12b46796d3aa331e795c75da8a5ccaeb 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -36,9 +36,9 @@ Global Instance uPred_affine : AffineBI (uPredI M) | 0.
 Proof. intros P. rewrite /Affine. by apply bi.pure_intro. Qed.
 
 (* Own and valid derived *)
-Lemma persistently_ownM (a : M) : CoreId a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
+Lemma bare_persistently_ownM (a : M) : CoreId a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
 Proof.
-  intros; apply (anti_symm _); first by rewrite persistently_elim.
+  rewrite affine_bare=>?; apply (anti_symm _); [by rewrite persistently_elim|].
   by rewrite {1}persistently_ownM_core core_id_core.
 Qed.
 Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊢ False.
@@ -47,9 +47,9 @@ Global Instance ownM_mono : Proper (flip (≼) ==> (⊢)) (@uPred_ownM M).
 Proof. intros a b [b' ->]. by rewrite ownM_op sep_elim_l. Qed.
 Lemma ownM_unit' : uPred_ownM ε ⊣⊢ True.
 Proof. apply (anti_symm _); first by apply pure_intro. apply ownM_empty. Qed.
-Lemma persistently_cmra_valid {A : cmraT} (a : A) : □ ✓ a ⊣⊢ ✓ a.
+Lemma bare_persistently_cmra_valid {A : cmraT} (a : A) : □ ✓ a ⊣⊢ ✓ a.
 Proof.
-  intros; apply (anti_symm _); first by rewrite persistently_elim.
+  rewrite affine_bare. intros; apply (anti_symm _); first by rewrite persistently_elim.
   apply:persistently_cmra_valid_1.
 Qed.
 
@@ -98,9 +98,11 @@ Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
 (* Persistence *)
 Global Instance cmra_valid_persistent {A : cmraT} (a : A) :
   Persistent (✓ a : uPred M)%I.
-Proof. by intros; rewrite /Persistent persistently_cmra_valid. Qed.
-Global Instance ownM_persistent : CoreId a → Persistent (@uPred_ownM M a).
-Proof. intros. by rewrite /Persistent persistently_ownM. Qed.
+Proof. rewrite /Persistent. apply persistently_cmra_valid_1. Qed.
+Global Instance ownM_persistent a : CoreId a → Persistent (@uPred_ownM M a).
+Proof.
+  intros. rewrite /Persistent -{2}(core_id_core a). apply persistently_ownM_core.
+Qed.
 
 (* For big ops *)
 Global Instance uPred_ownM_sep_homomorphism :
diff --git a/theories/base_logic/lib/viewshifts.v b/theories/base_logic/lib/viewshifts.v
index 4534a0bd2e067d38ead490e3bde59dac97d1ef91..08f270489ec355809ca72a2906b64e801619e20b 100644
--- a/theories/base_logic/lib/viewshifts.v
+++ b/theories/base_logic/lib/viewshifts.v
@@ -81,5 +81,8 @@ Lemma vs_alloc N P : ▷ P ={↑N}=> inv N P.
 Proof. iIntros "!# HP". by iApply inv_alloc. Qed.
 
 Lemma wand_fupd_alt E1 E2 P Q : (P ={E1,E2}=∗ Q) ⊣⊢ ∃ R, R ∗ (P ∗ R ={E1,E2}=> Q).
-Proof. rewrite bi.wand_alt. by setoid_rewrite bi.persistently_impl_wand. Qed.
+Proof.
+  rewrite bi.wand_alt. do 2 f_equiv. setoid_rewrite bi.affine_bare; last apply _.
+  by rewrite bi.persistently_impl_wand.
+Qed.
 End vs.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 29695fe3578296c4ba79b2afd57b2c057cd3c10d..ecc41121ec23a7c74ea1455a2ff2811b7a5d72e3 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -438,21 +438,21 @@ Proof.
   - (* (P ⊢ Q -∗ R) → P ∗ Q ⊢ R *)
     intros P Q R. unseal=> HPQR. split; intros n x ? (?&?&?&?&?). ofe_subst.
     eapply HPQR; eauto using cmra_validN_op_l.
-  - (* (P ⊢ Q) → □ P ⊢ □ Q *)
+  - (* (P ⊢ Q) → bi_persistently P ⊢ bi_persistently Q *)
     intros P QR HP. unseal; split=> n x ? /=. by apply HP, cmra_core_validN.
-  - (* □ P ⊢ □ □ P *)
+  - (* bi_persistently P ⊢ bi_persistently (bi_persistently P) *)
     intros P. unseal; split=> n x ?? /=. by rewrite cmra_core_idemp.
-  - (* (∀ a, □ Ψ a) ⊢ □ ∀ a, Ψ a *)
+  - (* (∀ a, bi_persistently (Ψ a)) ⊢ bi_persistently (∀ a, Ψ a) *)
     by unseal.
-  - (* □ (∃ a, Ψ a) ⊢ ∃ a, □ Ψ a *)
+  - (* bi_persistently (∃ a, Ψ a) ⊢ ∃ a, bi_persistently (Ψ a) *)
     by unseal.
-  - (* P ⊢ □ emp (ADMISSIBLE) *)
+  - (* P ⊢ bi_persistently emp (ADMISSIBLE) *)
     intros P. unfold uPred_emp; unseal; by split=> n x ? _.
-  - (* □ P ∗ Q ⊢ □ P (ADMISSIBLE) *)
+  - (* bi_persistently P ∗ Q ⊢ bi_persistently P (ADMISSIBLE) *)
     intros P Q. move: (uPred_persistently P)=> P'.
     unseal; split; intros n x ? (x1&x2&?&?&_); ofe_subst;
       eauto using uPred_mono, cmra_includedN_l.
-  - (* □ P ∧ Q ⊢ (emp ∧ P) ∗ Q *)
+  - (* bi_persistently P ∧ Q ⊢ (emp ∧ P) ∗ Q *)
     intros P Q. unseal; split=> n x ? [??]; simpl in *.
     exists (core x), x; rewrite ?cmra_core_l; auto.
 Qed.
@@ -489,9 +489,9 @@ Proof.
   - (* ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q) *)
     intros P Q. unseal; split=> -[|n] x ? /=; [done|intros (x1&x2&Hx&?&?)].
     exists x1, x2; eauto using dist_S.
-  - (* ▷ □ P ⊢ □ ▷ P *)
+  - (* ▷ bi_persistently P ⊢ bi_persistently (▷ P) *)
     by unseal.
-  - (* □ ▷ P ⊢ ▷ □ P *)
+  - (* bi_persistently (▷ P) ⊢ ▷ bi_persistently P *)
     by unseal.
   - (* ▷ P ⊢ ▷ False ∨ (▷ False → P) *)
     intros P. unseal; split=> -[|n] x ? /= HP; [by left|right].
@@ -570,7 +570,8 @@ Proof.
     by rewrite (assoc op _ z1) -(comm op z1) (assoc op z1)
       -(assoc op _ a2) (comm op z1) -Hy1 -Hy2.
 Qed.
-Lemma persistently_ownM_core (a : M) : uPred_ownM a ⊢ □ uPred_ownM (core a).
+Lemma persistently_ownM_core (a : M) :
+  uPred_ownM a ⊢ bi_persistently (uPred_ownM (core a)).
 Proof.
   rewrite /bi_persistently /=. unseal.
   split=> n x Hx /=. by apply cmra_core_monoN.
@@ -601,7 +602,8 @@ Lemma cmra_valid_elim {A : cmraT} (a : A) : ¬ ✓{0} a → ✓ a ⊢ (False : u
 Proof.
   intros Ha. unseal. split=> n x ??; apply Ha, cmra_validN_le with n; auto.
 Qed.
-Lemma persistently_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ □ (✓ a : uPred M).
+Lemma persistently_cmra_valid_1 {A : cmraT} (a : A) :
+  ✓ a ⊢ bi_persistently (✓ a : uPred M).
 Proof. by unseal. Qed.
 Lemma cmra_valid_weaken {A : cmraT} (a b : A) : ✓ (a ⋅ b) ⊢ (✓ a : uPred M).
 Proof. unseal; split=> n x _; apply cmra_validN_op_l. Qed.
diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 03acdf1c7796625ffa9fea8cebcb1a269ca6762f..c0c7cf886a06bbb342d8edaa033665aecf71a8fa 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -126,7 +126,8 @@ Section sep_list.
   Proof. auto using and_intro, big_sepL_mono, and_elim_l, and_elim_r. Qed.
 
   Lemma big_sepL_persistently `{AffineBI PROP} Φ l :
-    (□ [∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, □ Φ k x).
+    (bi_persistently ([∗ list] k↦x ∈ l, Φ k x)) ⊣⊢
+    ([∗ list] k↦x ∈ l, bi_persistently (Φ k x)).
   Proof. apply (big_opL_commute _). Qed.
 
   Lemma big_sepL_forall `{AffineBI PROP} Φ l :
@@ -144,12 +145,12 @@ Section sep_list.
 
   Lemma big_sepL_impl Φ Ψ l :
     ([∗ list] k↦x ∈ l, Φ k x) -∗
-    ⬕ (∀ k x, ⌜l !! k = Some x⌝ → Φ k x -∗ Ψ k x) -∗
+    □ (∀ k x, ⌜l !! k = Some x⌝ → Φ k x -∗ Ψ k x) -∗
     [∗ list] k↦x ∈ l, Ψ k x.
   Proof.
     apply wand_intro_l. revert Φ Ψ. induction l as [|x l IH]=> Φ Ψ /=.
     { by rewrite sep_elim_r. }
-    rewrite bare_persistently_sep_dup -assoc [(⬕ _ ∗ _)%I]comm -!assoc assoc.
+    rewrite bare_persistently_sep_dup -assoc [(□ _ ∗ _)%I]comm -!assoc assoc.
     apply sep_mono.
     - rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl.
       by rewrite bare_persistently_elim wand_elim_l.
@@ -264,7 +265,8 @@ Section and_list.
   Proof. auto using and_intro, big_andL_mono, and_elim_l, and_elim_r. Qed.
 
   Lemma big_andL_persistently Φ l :
-    (□ [∧ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∧ list] k↦x ∈ l, □ Φ k x).
+    (bi_persistently ([∧ list] k↦x ∈ l, Φ k x)) ⊣⊢
+    ([∧ list] k↦x ∈ l, bi_persistently (Φ k x)).
   Proof. apply (big_opL_commute _). Qed.
 
   Lemma big_andL_forall `{AffineBI PROP} Φ l :
@@ -394,7 +396,8 @@ Section gmap.
   Proof. auto using and_intro, big_sepM_mono, and_elim_l, and_elim_r. Qed.
 
   Lemma big_sepM_persistently `{AffineBI PROP} Φ m :
-    (□ [∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, □ Φ k x).
+    (bi_persistently ([∗ map] k↦x ∈ m, Φ k x)) ⊣⊢
+      ([∗ map] k↦x ∈ m, bi_persistently (Φ k x)).
   Proof. apply (big_opM_commute _). Qed.
 
   Lemma big_sepM_forall `{AffineBI PROP} Φ m :
@@ -416,13 +419,13 @@ Section gmap.
 
   Lemma big_sepM_impl Φ Ψ m :
     ([∗ map] k↦x ∈ m, Φ k x) -∗
-    ⬕ (∀ k x, ⌜m !! k = Some x⌝ → Φ k x -∗ Ψ k x) -∗
+    □ (∀ k x, ⌜m !! k = Some x⌝ → Φ k x -∗ Ψ k x) -∗
     [∗ map] k↦x ∈ m, Ψ k x.
   Proof.
     apply wand_intro_l. induction m as [|i x m ? IH] using map_ind.
     { by rewrite sep_elim_r. }
     rewrite !big_sepM_insert // bare_persistently_sep_dup.
-    rewrite -assoc [(⬕ _ ∗ _)%I]comm -!assoc assoc. apply sep_mono.
+    rewrite -assoc [(□ _ ∗ _)%I]comm -!assoc assoc. apply sep_mono.
     - rewrite (forall_elim i) (forall_elim x) pure_True ?lookup_insert //.
       by rewrite True_impl bare_persistently_elim wand_elim_l.
     - rewrite comm -IH /=.
@@ -559,7 +562,7 @@ Section gset.
   Proof. auto using and_intro, big_sepS_mono, and_elim_l, and_elim_r. Qed.
 
   Lemma big_sepS_persistently `{AffineBI PROP} Φ X :
-    □ ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, □ Φ y).
+    bi_persistently ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, bi_persistently (Φ y)).
   Proof. apply (big_opS_commute _). Qed.
 
   Lemma big_sepS_forall `{AffineBI PROP} Φ X :
@@ -577,13 +580,13 @@ Section gset.
 
   Lemma big_sepS_impl Φ Ψ X :
     ([∗ set] x ∈ X, Φ x) -∗
-    ⬕ (∀ x, ⌜x ∈ X⌝ → Φ x -∗ Ψ x) -∗
+    □ (∀ x, ⌜x ∈ X⌝ → Φ x -∗ Ψ x) -∗
     [∗ set] x ∈ X, Ψ x.
   Proof.
     apply wand_intro_l. induction X as [|x X ? IH] using collection_ind_L.
     { by rewrite sep_elim_r. }
     rewrite !big_sepS_insert // bare_persistently_sep_dup.
-    rewrite -assoc [(⬕ _ ∗ _)%I]comm -!assoc assoc. apply sep_mono.
+    rewrite -assoc [(□ _ ∗ _)%I]comm -!assoc assoc. apply sep_mono.
     - rewrite (forall_elim x) pure_True; last set_solver.
       by rewrite True_impl bare_persistently_elim wand_elim_l.
     - rewrite comm -IH /=. apply sep_mono_l, bare_mono, persistently_mono.
@@ -667,7 +670,8 @@ Section gmultiset.
   Proof. auto using and_intro, big_sepMS_mono, and_elim_l, and_elim_r. Qed.
 
   Lemma big_sepMS_persistently `{AffineBI PROP} Φ X :
-    □ ([∗ mset] y ∈ X, Φ y) ⊣⊢ ([∗ mset] y ∈ X, □ Φ y).
+    bi_persistently ([∗ mset] y ∈ X, Φ y) ⊣⊢
+      ([∗ mset] y ∈ X, bi_persistently (Φ y)).
   Proof. apply (big_opMS_commute _). Qed.
 
   Global Instance big_sepMS_empty_persistent Φ :
diff --git a/theories/bi/derived.v b/theories/bi/derived.v
index f350f0599f891a56ea87030380cd5d8c5a45c7b6..94c19e04c528822f914869b77aeff20556a2989a 100644
--- a/theories/bi/derived.v
+++ b/theories/bi/derived.v
@@ -13,7 +13,7 @@ Arguments bi_wand_iff {_} _%I _%I : simpl never.
 Instance: Params (@bi_wand_iff) 1.
 Infix "∗-∗" := bi_wand_iff (at level 95, no associativity) : bi_scope.
 
-Class Persistent {PROP : bi} (P : PROP) := persistent : P ⊢ □ P.
+Class Persistent {PROP : bi} (P : PROP) := persistent : P ⊢ bi_persistently P.
 Arguments Persistent {_} _%I : simpl never.
 Arguments persistent {_} _%I {_}.
 Hint Mode Persistent + ! : typeclass_instances.
@@ -23,8 +23,8 @@ Definition bi_bare {PROP : bi} (P : PROP) : PROP := (emp ∧ P)%I.
 Arguments bi_bare {_} _%I : simpl never.
 Instance: Params (@bi_bare) 1.
 Typeclasses Opaque bi_bare.
-Notation "â–  P" := (bi_bare P) (at level 20, right associativity) : bi_scope.
-Notation "⬕ P" := (■ □ P)%I (at level 20, right associativity) : bi_scope.
+Notation "â–¡ P" := (bi_bare (bi_persistently P))%I
+  (at level 20, right associativity) : bi_scope.
 
 Class Affine {PROP : bi} (Q : PROP) := affine : Q ⊢ emp.
 Arguments Affine {_} _%I : simpl never.
@@ -35,7 +35,7 @@ Class AffineBI (PROP : bi) := absorbing_bi (Q : PROP) : Affine Q.
 Existing Instance absorbing_bi | 0.
 
 Class PositiveBI (PROP : bi) :=
-  positive_bi (P Q : PROP) : ■ (P ∗ Q) ⊢ ■ P ∗ Q.
+  positive_bi (P Q : PROP) : bi_bare (P ∗ Q) ⊢ bi_bare P ∗ Q.
 
 Definition bi_sink {PROP : bi} (P : PROP) : PROP := (True ∗ P)%I.
 Arguments bi_sink {_} _%I : simpl never.
@@ -48,25 +48,19 @@ Arguments Absorbing {_} _%I : simpl never.
 Arguments absorbing {_} _%I.
 
 Definition bi_persistently_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
-  (if p then â–¡ P else P)%I.
+  (if p then bi_persistently P else P)%I.
 Arguments bi_persistently_if {_} !_ _%I /.
 Instance: Params (@bi_persistently_if) 2.
 Typeclasses Opaque bi_persistently_if.
-Notation "â–¡? p P" := (bi_persistently_if p P)
-  (at level 20, p at level 9, P at level 20,
-   right associativity, format "â–¡? p  P") : bi_scope.
 
 Definition bi_bare_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
-  (if p then â–  P else P)%I.
+  (if p then bi_bare P else P)%I.
 Arguments bi_bare_if {_} !_ _%I /.
 Instance: Params (@bi_bare_if) 2.
 Typeclasses Opaque bi_bare_if.
-Notation "â– ? p P" := (bi_bare_if p P)
-  (at level 20, p at level 9, P at level 20,
-   right associativity, format "â– ? p  P") : bi_scope.
-Notation "⬕? p P" := (■?p □?p P)%I
+Notation "â–¡? p P" := (bi_bare_if p (bi_persistently_if p P))%I
   (at level 20, p at level 9, P at level 20,
-   right associativity, format "⬕? p  P") : bi_scope.
+   right associativity, format "â–¡? p  P") : bi_scope.
 
 Fixpoint bi_hexist {PROP : bi} {As} : himpl As PROP → PROP :=
   match As return himpl As PROP → PROP with
@@ -691,53 +685,53 @@ Global Instance bare_flip_mono' :
   Proper (flip (⊢) ==> flip (⊢)) (@bi_bare PROP).
 Proof. solve_proper. Qed.
 
-Lemma bare_elim_emp P : ■ P ⊢ emp.
+Lemma bare_elim_emp P : bi_bare P ⊢ emp.
 Proof. rewrite /bi_bare; auto. Qed.
-Lemma bare_elim P : ■ P ⊢ P.
+Lemma bare_elim P : bi_bare P ⊢ P.
 Proof. rewrite /bi_bare; auto. Qed.
-Lemma bare_mono P Q : (P ⊢ Q) → ■ P ⊢ ■ Q.
+Lemma bare_mono P Q : (P ⊢ Q) → bi_bare P ⊢ bi_bare Q.
 Proof. by intros ->. Qed.
-Lemma bare_idemp P : ■ ■ P ⊣⊢ ■ P.
+Lemma bare_idemp P : bi_bare (bi_bare P) ⊣⊢ bi_bare P.
 Proof. by rewrite /bi_bare assoc idemp. Qed.
 
-Lemma bare_intro' P Q : (■ P ⊢ Q) → ■ P ⊢ ■ Q.
+Lemma bare_intro' P Q : (bi_bare P ⊢ Q) → bi_bare P ⊢ bi_bare Q.
 Proof. intros <-. by rewrite bare_idemp. Qed.
 
-Lemma bare_False : ■ False ⊣⊢ False.
+Lemma bare_False : bi_bare False ⊣⊢ False.
 Proof. by rewrite /bi_bare right_absorb. Qed.
-Lemma bare_emp : ■ emp ⊣⊢ emp.
+Lemma bare_emp : bi_bare emp ⊣⊢ emp.
 Proof. by rewrite /bi_bare (idemp bi_and). Qed.
-Lemma bare_or P Q : ■ (P ∨ Q) ⊣⊢ ■ P ∨ ■ Q.
+Lemma bare_or P Q : bi_bare (P ∨ Q) ⊣⊢ bi_bare P ∨ bi_bare Q.
 Proof. by rewrite /bi_bare and_or_l. Qed.
-Lemma bare_and P Q : ■ (P ∧ Q) ⊣⊢ ■ P ∧ ■ Q.
+Lemma bare_and P Q : bi_bare (P ∧ Q) ⊣⊢ bi_bare P ∧ bi_bare Q.
 Proof.
   rewrite /bi_bare -(comm _ P) (assoc _ (_ ∧ _)%I) -!(assoc _ P).
   by rewrite idemp !assoc (comm _ P).
 Qed.
-Lemma bare_sep_2 P Q : ■ P ∗ ■ Q ⊢ ■ (P ∗ Q).
+Lemma bare_sep_2 P Q : bi_bare P ∗ bi_bare Q ⊢ bi_bare (P ∗ Q).
 Proof.
   rewrite /bi_bare. apply and_intro.
   - by rewrite !and_elim_l right_id.
   - by rewrite !and_elim_r.
 Qed.
-Lemma bare_sep `{PositiveBI PROP} P Q : ■ (P ∗ Q) ⊣⊢ ■ P ∗ ■ Q.
+Lemma bare_sep `{PositiveBI PROP} P Q : bi_bare (P ∗ Q) ⊣⊢ bi_bare P ∗ bi_bare Q.
 Proof.
   apply (anti_symm _), bare_sep_2.
-  by rewrite -{1}bare_idemp positive_bi !(comm _ (â–  P)%I) positive_bi.
+  by rewrite -{1}bare_idemp positive_bi !(comm _ (bi_bare P)%I) positive_bi.
 Qed.
-Lemma bare_forall {A} (Φ : A → PROP) : ■ (∀ a, Φ a) ⊢ ∀ a, ■ Φ a.
+Lemma bare_forall {A} (Φ : A → PROP) : bi_bare (∀ a, Φ a) ⊢ ∀ a, bi_bare (Φ a).
 Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed.
-Lemma bare_exist {A} (Φ : A → PROP) : ■ (∃ a, Φ a) ⊣⊢ ∃ a, ■ Φ a.
+Lemma bare_exist {A} (Φ : A → PROP) : bi_bare (∃ a, Φ a) ⊣⊢ ∃ a, bi_bare (Φ a).
 Proof. by rewrite /bi_bare and_exist_l. Qed.
 
-Lemma bare_True_emp : ■ True ⊣⊢ ■ emp.
+Lemma bare_True_emp : bi_bare True ⊣⊢ bi_bare emp.
 Proof. apply (anti_symm _); rewrite /bi_bare; auto. Qed.
 
-Lemma bare_and_l P Q : ■ P ∧ Q ⊣⊢ ■ (P ∧ Q).
+Lemma bare_and_l P Q : bi_bare P ∧ Q ⊣⊢ bi_bare (P ∧ Q).
 Proof. by rewrite /bi_bare assoc. Qed.
-Lemma bare_and_r P Q : P ∧ ■ Q ⊣⊢ ■ (P ∧ Q).
+Lemma bare_and_r P Q : P ∧ bi_bare Q ⊣⊢ bi_bare (P ∧ Q).
 Proof. by rewrite /bi_bare !assoc (comm _ P). Qed.
-Lemma bare_and_lr P Q : ■ P ∧ Q ⊣⊢ P ∧ ■ Q.
+Lemma bare_and_lr P Q : bi_bare P ∧ Q ⊣⊢ P ∧ bi_bare Q.
 Proof. by rewrite bare_and_l bare_and_r. Qed.
 
 (* Properties of the sink modality *)
@@ -796,7 +790,7 @@ Proof. by rewrite /bi_sink !assoc (comm _ P). Qed.
 Lemma sink_sep_lr P Q : ▲ P ∗ Q ⊣⊢ P ∗ ▲ Q.
 Proof. by rewrite sink_sep_l sink_sep_r. Qed.
 
-Lemma bare_sink `{!PositiveBI PROP} P : ■ ▲ P ⊣⊢ ■ P.
+Lemma bare_sink `{!PositiveBI PROP} P : bi_bare (▲ P) ⊣⊢ bi_bare P.
 Proof.
   apply (anti_symm _), bare_mono, sink_intro.
   by rewrite /bi_sink bare_sep bare_True_emp bare_emp left_id.
@@ -823,7 +817,7 @@ Proof. rewrite /Affine=> H. apply exist_elim=> a. by rewrite H. Qed.
 
 Global Instance sep_affine P Q : Affine P → Affine Q → Affine (P ∗ Q).
 Proof. rewrite /Affine=>-> ->. by rewrite left_id. Qed.
-Global Instance bare_affine P : Affine (â–  P).
+Global Instance bare_affine P : Affine (bi_bare P).
 Proof. rewrite /bi_bare. apply _. Qed.
 
 (* Absorbing propositions *)
@@ -859,7 +853,7 @@ Global Instance sink_absorbing P : Absorbing (â–² P).
 Proof. rewrite /bi_sink. apply _. Qed.
 
 (* Properties of affine and absorbing propositions *)
-Lemma affine_bare P `{!Affine P} : ■ P ⊣⊢ P.
+Lemma affine_bare P `{!Affine P} : bi_bare P ⊣⊢ P.
 Proof. rewrite /bi_bare. apply (anti_symm _); auto. Qed.
 Lemma absorbing_sink P `{!Absorbing P} : ▲ P ⊣⊢ P.
 Proof. by apply (anti_symm _), sink_intro. Qed.
@@ -890,7 +884,7 @@ Proof.
 Qed.
 
 
-Lemma bare_intro P Q `{!Affine P} : (P ⊢ Q) → P ⊢ ■ Q.
+Lemma bare_intro P Q `{!Affine P} : (P ⊢ Q) → P ⊢ bi_bare Q.
 Proof. intros <-. by rewrite affine_bare. Qed.
 
 Lemma emp_and P `{!Affine P} : emp ∧ P ⊣⊢ P.
@@ -948,14 +942,15 @@ Global Instance persistently_flip_mono' :
   Proper (flip (⊢) ==> flip (⊢)) (@bi_persistently PROP).
 Proof. intros P Q; apply persistently_mono. Qed.
 
-Lemma sink_persistently P : ▲ □ P ⊣⊢ □ P.
+Lemma sink_persistently P : ▲ bi_persistently P ⊣⊢ bi_persistently P.
 Proof.
   apply (anti_symm _), sink_intro. by rewrite /bi_sink comm persistently_absorbing.
 Qed.
-Global Instance persistently_absorbing P : Absorbing (â–¡ P).
+Global Instance persistently_absorbing P : Absorbing (bi_persistently P).
 Proof. by rewrite /Absorbing sink_persistently. Qed.
 
-Lemma persistently_and_sep_assoc P Q R : □ P ∧ (Q ∗ R) ⊣⊢ (□ P ∧ Q) ∗ R.
+Lemma persistently_and_sep_assoc P Q R :
+  bi_persistently P ∧ (Q ∗ R) ⊣⊢ (bi_persistently P ∧ Q) ∗ R.
 Proof.
   apply (anti_symm (⊢)).
   - rewrite {1}persistently_idemp_2 persistently_and_sep_elim assoc.
@@ -966,111 +961,129 @@ Proof.
     + by rewrite and_elim_l sep_elim_l.
     + by rewrite and_elim_r.
 Qed.
-Lemma persistently_and_emp_elim P : emp ∧ □ P ⊢ P.
+Lemma persistently_and_emp_elim P : emp ∧ bi_persistently P ⊢ P.
 Proof. by rewrite comm persistently_and_sep_elim right_id and_elim_r. Qed.
-Lemma persistently_elim_sink P : □ P ⊢ ▲ P.
+Lemma persistently_elim_sink P : bi_persistently P ⊢ ▲ P.
 Proof.
-  rewrite -(right_id True%I _ (â–¡ _)%I) -{1}(left_id emp%I _ True%I).
+  rewrite -(right_id True%I _ (bi_persistently _)%I) -{1}(left_id emp%I _ True%I).
   by rewrite persistently_and_sep_assoc (comm bi_and) persistently_and_emp_elim comm.
 Qed.
-Lemma persistently_elim P `{!Absorbing P} : □ P ⊢ P.
+Lemma persistently_elim P `{!Absorbing P} : bi_persistently P ⊢ P.
 Proof. by rewrite persistently_elim_sink absorbing_sink. Qed.
 
-Lemma persistently_idemp_1 P : □ □ P ⊢ □ P.
+Lemma persistently_idemp_1 P :
+  bi_persistently (bi_persistently P) ⊢ bi_persistently P.
 Proof. by rewrite persistently_elim_sink sink_persistently. Qed.
-Lemma persistently_idemp P : □ □ P ⊣⊢ □ P.
+Lemma persistently_idemp P :
+  bi_persistently (bi_persistently P) ⊣⊢ bi_persistently P.
 Proof. apply (anti_symm _); auto using persistently_idemp_1, persistently_idemp_2. Qed.
 
-Lemma persistently_intro' P Q : (□ P ⊢ Q) → □ P ⊢ □ Q.
+Lemma persistently_intro' P Q :
+  (bi_persistently P ⊢ Q) → bi_persistently P ⊢ bi_persistently Q.
 Proof. intros <-. apply persistently_idemp_2. Qed.
 
-Lemma persistently_pure φ : □ ⌜φ⌝ ⊣⊢ ⌜φ⌝.
+Lemma persistently_pure φ : bi_persistently ⌜φ⌝ ⊣⊢ ⌜φ⌝.
 Proof.
   apply (anti_symm _); first by rewrite persistently_elim.
   apply pure_elim'=> Hφ.
-  trans (∀ x : False, □ True : PROP)%I; [by apply forall_intro|].
+  trans (∀ x : False, bi_persistently True : PROP)%I; [by apply forall_intro|].
   rewrite persistently_forall_2. auto using persistently_mono, pure_intro.
 Qed.
-Lemma persistently_forall {A} (Ψ : A → PROP) : (□ ∀ a, Ψ a) ⊣⊢ (∀ a, □ Ψ a).
+Lemma persistently_forall {A} (Ψ : A → PROP) :
+  bi_persistently (∀ a, Ψ a) ⊣⊢ ∀ a, bi_persistently (Ψ a).
 Proof.
   apply (anti_symm _); auto using persistently_forall_2.
   apply forall_intro=> x. by rewrite (forall_elim x).
 Qed.
-Lemma persistently_exist {A} (Ψ : A → PROP) : (□ ∃ a, Ψ a) ⊣⊢ (∃ a, □ Ψ a).
+Lemma persistently_exist {A} (Ψ : A → PROP) :
+  bi_persistently (∃ a, Ψ a) ⊣⊢ ∃ a, bi_persistently (Ψ a).
 Proof.
   apply (anti_symm _); auto using persistently_exist_1.
   apply exist_elim=> x. by rewrite (exist_intro x).
 Qed.
-Lemma persistently_and P Q : □ (P ∧ Q) ⊣⊢ □ P ∧ □ Q.
+Lemma persistently_and P Q :
+  bi_persistently (P ∧ Q) ⊣⊢ bi_persistently P ∧ bi_persistently Q.
 Proof. rewrite !and_alt persistently_forall. by apply forall_proper=> -[]. Qed.
-Lemma persistently_or P Q : □ (P ∨ Q) ⊣⊢ □ P ∨ □ Q.
+Lemma persistently_or P Q :
+  bi_persistently (P ∨ Q) ⊣⊢ bi_persistently P ∨ bi_persistently Q.
 Proof. rewrite !or_alt persistently_exist. by apply exist_proper=> -[]. Qed.
-Lemma persistently_impl P Q : □ (P → Q) ⊢ □ P → □ Q.
+Lemma persistently_impl P Q :
+  bi_persistently (P → Q) ⊢ bi_persistently P → bi_persistently Q.
 Proof.
   apply impl_intro_l; rewrite -persistently_and.
   apply persistently_mono, impl_elim with P; auto.
 Qed.
 
-Lemma persistently_internal_eq {A : ofeT} (a b : A) : □ (a ≡ b) ⊣⊢ a ≡ b.
+Lemma persistently_internal_eq {A : ofeT} (a b : A) :
+  bi_persistently (a ≡ b) ⊣⊢ a ≡ b.
 Proof.
   apply (anti_symm (⊢)); first by rewrite persistently_elim.
-  apply (internal_eq_rewrite' a b (λ b, □ (a ≡ b))%I); auto.
+  apply (internal_eq_rewrite' a b (λ b, bi_persistently (a ≡ b))%I); auto.
   rewrite -(internal_eq_refl emp%I a). apply persistently_emp_intro.
 Qed.
 
-Lemma persistently_sep_dup P : □ P ⊣⊢ □ P ∗ □ P.
+Lemma persistently_sep_dup P :
+  bi_persistently P ⊣⊢ bi_persistently P ∗ bi_persistently P.
 Proof.
   apply (anti_symm _); last by eauto using sep_elim_l with typeclass_instances.
-  rewrite -{1}(idemp bi_and (â–¡ _)%I) -{2}(left_id emp%I _ (â–¡ _)%I).
-  by rewrite persistently_and_sep_assoc and_elim_l.
+  by rewrite -{1}(idemp bi_and (bi_persistently _)%I)
+             -{2}(left_id emp%I _ (bi_persistently _)%I)
+                 persistently_and_sep_assoc and_elim_l.
 Qed.
 
-Lemma persistently_and_sep_l_1 P Q : □ P ∧ Q ⊢ □ P ∗ Q.
+Lemma persistently_and_sep_l_1 P Q : bi_persistently P ∧ Q ⊢ bi_persistently P ∗ Q.
 Proof.
   by rewrite -{1}(left_id emp%I _ Q%I) persistently_and_sep_assoc and_elim_l.
 Qed.
-Lemma persistently_and_sep_r_1 P Q : P ∧ □ Q ⊢ P ∗ □ Q.
+Lemma persistently_and_sep_r_1 P Q : P ∧ bi_persistently Q ⊢ P ∗ bi_persistently Q.
 Proof. by rewrite !(comm _ P) persistently_and_sep_l_1. Qed.
 
-Lemma persistently_True_emp : □ True ⊣⊢ □ emp.
+Lemma persistently_True_emp : bi_persistently True ⊣⊢ bi_persistently emp.
 Proof. apply (anti_symm _); auto using persistently_emp_intro. Qed.
-Lemma persistently_and_sep P Q : □ (P ∧ Q) ⊢ □ (P ∗ Q).
+Lemma persistently_and_sep P Q : bi_persistently (P ∧ Q) ⊢ bi_persistently (P ∗ Q).
 Proof.
   rewrite persistently_and.
   rewrite -{1}persistently_idemp -persistently_and -{1}(left_id emp%I _ Q%I).
   by rewrite persistently_and_sep_assoc (comm bi_and) persistently_and_emp_elim.
 Qed.
 
-Lemma persistently_bare P : □ ■ P ⊣⊢ □ P.
+Lemma persistently_bare P : bi_persistently (bi_bare P) ⊣⊢ bi_persistently P.
 Proof.
   by rewrite /bi_bare persistently_and -persistently_True_emp
              persistently_pure left_id.
 Qed.
 
-Lemma and_sep_persistently P Q : □ P ∧ □ Q ⊣⊢ □ P ∗ □ Q.
+Lemma and_sep_persistently P Q :
+  bi_persistently P ∧ bi_persistently Q ⊣⊢ bi_persistently P ∗ bi_persistently Q.
 Proof.
   apply (anti_symm _).
   - auto using persistently_and_sep_l_1.
   - eauto 10 using sep_elim_l, sep_elim_r with typeclass_instances.
 Qed.
-Lemma persistently_sep_2 P Q : □ P ∗ □ Q ⊢ □ (P ∗ Q).
+Lemma persistently_sep_2 P Q :
+  bi_persistently P ∗ bi_persistently Q ⊢ bi_persistently (P ∗ Q).
 Proof. by rewrite -persistently_and_sep persistently_and -and_sep_persistently. Qed.
-Lemma persistently_sep `{PositiveBI PROP} P Q : □ (P ∗ Q) ⊣⊢ □ P ∗ □ Q.
+Lemma persistently_sep `{PositiveBI PROP} P Q :
+  bi_persistently (P ∗ Q) ⊣⊢ bi_persistently P ∗ bi_persistently Q.
 Proof.
   apply (anti_symm _); auto using persistently_sep_2.
   by rewrite -persistently_bare bare_sep sep_and !bare_elim persistently_and
              and_sep_persistently.
 Qed.
 
-Lemma persistently_wand P Q : □ (P -∗ Q) ⊢ □ P -∗ □ Q.
+Lemma persistently_wand P Q :
+  bi_persistently (P -∗ Q) ⊢ bi_persistently P -∗ bi_persistently Q.
 Proof. apply wand_intro_r. by rewrite persistently_sep_2 wand_elim_l. Qed.
 
-Lemma persistently_entails_l P Q : (P ⊢ □ Q) → P ⊢ □ Q ∗ P.
+Lemma persistently_entails_l P Q :
+  (P ⊢ bi_persistently Q) → P ⊢ bi_persistently Q ∗ P.
 Proof. intros; rewrite -persistently_and_sep_l_1; auto. Qed.
-Lemma persistently_entails_r P Q : (P ⊢ □ Q) → P ⊢ P ∗ □ Q.
+Lemma persistently_entails_r P Q :
+  (P ⊢ bi_persistently Q) → P ⊢ P ∗ bi_persistently Q.
 Proof. intros; rewrite -persistently_and_sep_r_1; auto. Qed.
 
-Lemma persistently_impl_wand_2 P Q : □ (P -∗ Q) ⊢ □ (P → Q).
+Lemma persistently_impl_wand_2 P Q :
+  bi_persistently (P -∗ Q) ⊢ bi_persistently (P → Q).
 Proof.
   apply persistently_intro', impl_intro_r.
   rewrite -{2}(left_id emp%I _ P%I) persistently_and_sep_assoc.
@@ -1080,25 +1093,27 @@ Qed.
 Section persistently_bare_bi.
   Context `{AffineBI PROP}.
 
-  Lemma persistently_emp : □ emp ⊣⊢ emp.
+  Lemma persistently_emp : bi_persistently emp ⊣⊢ emp.
   Proof. by rewrite -!True_emp persistently_pure. Qed.
 
-  Lemma persistently_and_sep_l P Q : □ P ∧ Q ⊣⊢ □ P ∗ Q.
+  Lemma persistently_and_sep_l P Q :
+    bi_persistently P ∧ Q ⊣⊢ bi_persistently P ∗ Q.
   Proof.
     apply (anti_symm (⊢));
       eauto using persistently_and_sep_l_1, sep_and with typeclass_instances.
   Qed.
-  Lemma persistently_and_sep_r P Q : P ∧ □ Q ⊣⊢ P ∗ □ Q.
+  Lemma persistently_and_sep_r P Q : P ∧ bi_persistently Q ⊣⊢ P ∗ bi_persistently Q.
   Proof. by rewrite !(comm _ P) persistently_and_sep_l. Qed.
 
-  Lemma persistently_impl_wand P Q : □ (P → Q) ⊣⊢ □ (P -∗ Q).
+  Lemma persistently_impl_wand P Q :
+    bi_persistently (P → Q) ⊣⊢ bi_persistently (P -∗ Q).
   Proof.
     apply (anti_symm (⊢)); auto using persistently_impl_wand_2.
     apply persistently_intro', wand_intro_l.
     by rewrite -persistently_and_sep_r persistently_elim impl_elim_r.
   Qed.
 
-  Lemma wand_alt P Q : (P -∗ Q) ⊣⊢ ∃ R, R ∗ □ (P ∗ R → Q).
+  Lemma wand_alt P Q : (P -∗ Q) ⊣⊢ ∃ R, R ∗ bi_persistently (P ∗ R → Q).
   Proof.
     apply (anti_symm (⊢)).
     - rewrite -(right_id True%I bi_sep (P -∗ Q)%I) -(exist_intro (P -∗ Q)%I).
@@ -1109,53 +1124,54 @@ Section persistently_bare_bi.
       rewrite assoc -persistently_and_sep_r.
       by rewrite persistently_elim impl_elim_r.
   Qed.
-  Lemma impl_alt P Q : (P → Q) ⊣⊢ ∃ R, R ∧ □ (P ∧ R -∗ Q).
+  Lemma impl_alt P Q : (P → Q) ⊣⊢ ∃ R, R ∧ bi_persistently (P ∧ R -∗ Q).
   Proof.
     apply (anti_symm (⊢)).
     - rewrite -(right_id True%I bi_and (P → Q)%I) -(exist_intro (P → Q)%I).
       apply and_mono_r. rewrite -persistently_pure.
       apply persistently_intro', wand_intro_l.
       by rewrite impl_elim_r persistently_pure right_id.
-    - apply exist_elim=> R. apply impl_intro_l. rewrite assoc persistently_and_sep_r.
-      by rewrite persistently_elim wand_elim_r.
+    - apply exist_elim=> R. apply impl_intro_l.
+      by rewrite assoc persistently_and_sep_r persistently_elim wand_elim_r.
   Qed.
 End persistently_bare_bi.
 
 
 (* The combined bare persistently modality *)
-Lemma bare_persistently_elim P : ⬕ P ⊢ P.
+Lemma bare_persistently_elim P : □ P ⊢ P.
 Proof. apply persistently_and_emp_elim. Qed.
-Lemma bare_persistently_intro' P Q : (⬕ P ⊢ Q) → ⬕ P ⊢ ⬕ Q.
+Lemma bare_persistently_intro' P Q : (□ P ⊢ Q) → □ P ⊢ □ Q.
 Proof. intros <-. by rewrite persistently_bare persistently_idemp. Qed.
 
-Lemma bare_persistently_emp : ⬕ emp ⊣⊢ emp.
+Lemma bare_persistently_emp : □ emp ⊣⊢ emp.
 Proof. by rewrite -persistently_True_emp persistently_pure bare_True_emp bare_emp. Qed.
-Lemma bare_persistently_and P Q : ⬕ (P ∧ Q) ⊣⊢ ⬕ P ∧ ⬕ Q.
+Lemma bare_persistently_and P Q : □ (P ∧ Q) ⊣⊢ □ P ∧ □ Q.
 Proof. by rewrite persistently_and bare_and. Qed.
-Lemma bare_persistently_or P Q : ⬕ (P ∨ Q) ⊣⊢ ⬕ P ∨ ⬕ Q.
+Lemma bare_persistently_or P Q : □ (P ∨ Q) ⊣⊢ □ P ∨ □ Q.
 Proof. by rewrite persistently_or bare_or. Qed.
-Lemma bare_persistently_exist {A} (Φ : A → PROP) : ⬕ (∃ x, Φ x) ⊣⊢ ∃ x, ⬕ Φ x.
+Lemma bare_persistently_exist {A} (Φ : A → PROP) : □ (∃ x, Φ x) ⊣⊢ ∃ x, □ Φ x.
 Proof. by rewrite persistently_exist bare_exist. Qed.
-Lemma bare_persistently_sep_2 P Q : ⬕ P ∗ ⬕ Q ⊢ ⬕ (P ∗ Q).
+Lemma bare_persistently_sep_2 P Q : □ P ∗ □ Q ⊢ □ (P ∗ Q).
 Proof. by rewrite bare_sep_2 persistently_sep_2. Qed.
-Lemma bare_persistently_sep `{PositiveBI PROP} P Q : ⬕ (P ∗ Q) ⊣⊢ ⬕ P ∗ ⬕ Q.
+Lemma bare_persistently_sep `{PositiveBI PROP} P Q : □ (P ∗ Q) ⊣⊢ □ P ∗ □ Q.
 Proof. by rewrite -bare_sep -persistently_sep. Qed.
 
-Lemma bare_persistently_idemp P : ⬕ ⬕ P ⊣⊢ ⬕ P.
+Lemma bare_persistently_idemp P : □ □ P ⊣⊢ □ P.
 Proof. by rewrite persistently_bare persistently_idemp. Qed.
 
-Lemma persistently_and_bare_sep_l P Q : □ P ∧ Q ⊣⊢ ⬕ P ∗ Q.
+Lemma persistently_and_bare_sep_l P Q : bi_persistently P ∧ Q ⊣⊢ □ P ∗ Q.
 Proof.
   apply (anti_symm _).
-  - by rewrite /bi_bare -(comm bi_and (â–¡ P)%I) -persistently_and_sep_assoc left_id.
+  - by rewrite /bi_bare -(comm bi_and (bi_persistently P)%I)
+               -persistently_and_sep_assoc left_id.
   - apply and_intro. by rewrite bare_elim sep_elim_l. by rewrite sep_elim_r.
 Qed.
-Lemma persistently_and_bare_sep_r P Q : P ∧ □ Q ⊣⊢ P ∗ ⬕ Q.
+Lemma persistently_and_bare_sep_r P Q : P ∧ bi_persistently Q ⊣⊢ P ∗ □ Q.
 Proof. by rewrite !(comm _ P) persistently_and_bare_sep_l. Qed.
-Lemma and_sep_bare_persistently P Q : ⬕ P ∧ ⬕ Q ⊣⊢ ⬕ P ∗ ⬕ Q.
+Lemma and_sep_bare_persistently P Q : □ P ∧ □ Q ⊣⊢ □ P ∗ □ Q.
 Proof. by rewrite -persistently_and_bare_sep_l -bare_and bare_and_r. Qed.
 
-Lemma bare_persistently_sep_dup P : ⬕ P ⊣⊢ ⬕ P ∗ ⬕ P.
+Lemma bare_persistently_sep_dup P : □ P ⊣⊢ □ P ∗ □ P.
 Proof. by rewrite -persistently_and_bare_sep_l bare_and_r bare_and idemp. Qed.
 
 (* Conditional bare modality *)
@@ -1169,30 +1185,34 @@ Global Instance bare_if_flip_mono' p :
   Proper (flip (⊢) ==> flip (⊢)) (@bi_bare_if PROP p).
 Proof. solve_proper. Qed.
 
-Lemma bare_if_mono p P Q : (P ⊢ Q) → ■?p P ⊢ ■?p Q.
+Lemma bare_if_mono p P Q : (P ⊢ Q) → bi_bare_if p P ⊢ bi_bare_if p Q.
 Proof. by intros ->. Qed.
 
-Lemma bare_if_elim p P : ■?p P ⊢ P.
+Lemma bare_if_elim p P : bi_bare_if p P ⊢ P.
 Proof. destruct p; simpl; auto using bare_elim. Qed.
-Lemma bare_bare_if p P : ■ P ⊢ ■?p P.
+Lemma bare_bare_if p P : bi_bare P ⊢ bi_bare_if p P.
 Proof. destruct p; simpl; auto using bare_elim. Qed.
-Lemma bare_if_intro' p P Q : (■?p P ⊢ Q) → ■?p P ⊢ ■?p Q.
+Lemma bare_if_intro' p P Q :
+  (bi_bare_if p P ⊢ Q) → bi_bare_if p P ⊢ bi_bare_if p Q.
 Proof. destruct p; simpl; auto using bare_intro'. Qed.
 
-Lemma bare_if_emp p : ■?p emp ⊣⊢ emp.
+Lemma bare_if_emp p : bi_bare_if p emp ⊣⊢ emp.
 Proof. destruct p; simpl; auto using bare_emp. Qed.
-Lemma bare_if_and p P Q : ■?p (P ∧ Q) ⊣⊢ ■?p P ∧ ■?p Q.
+Lemma bare_if_and p P Q : bi_bare_if p (P ∧ Q) ⊣⊢ bi_bare_if p P ∧ bi_bare_if p Q.
 Proof. destruct p; simpl; auto using bare_and. Qed.
-Lemma bare_if_or p P Q : ■?p (P ∨ Q) ⊣⊢ ■?p P ∨ ■?p Q.
+Lemma bare_if_or p P Q : bi_bare_if p (P ∨ Q) ⊣⊢ bi_bare_if p P ∨ bi_bare_if p Q.
 Proof. destruct p; simpl; auto using bare_or. Qed.
-Lemma bare_if_exist {A} p (Ψ : A → PROP) : (■?p ∃ a, Ψ a) ⊣⊢ ∃ a, ■?p Ψ a.
+Lemma bare_if_exist {A} p (Ψ : A → PROP) :
+  bi_bare_if p (∃ a, Ψ a) ⊣⊢ ∃ a, bi_bare_if p (Ψ a).
 Proof. destruct p; simpl; auto using bare_exist. Qed.
-Lemma bare_if_sep_2 p P Q : ■?p P ∗ ■?p Q ⊢ ■?p (P ∗ Q).
+Lemma bare_if_sep_2 p P Q :
+  bi_bare_if p P ∗ bi_bare_if p Q ⊢ bi_bare_if p (P ∗ Q).
 Proof. destruct p; simpl; auto using bare_sep_2. Qed.
-Lemma bare_if_sep `{PositiveBI PROP} p P Q : ■?p (P ∗ Q) ⊣⊢ ■?p P ∗ ■?p Q.
+Lemma bare_if_sep `{PositiveBI PROP} p P Q :
+  bi_bare_if p (P ∗ Q) ⊣⊢ bi_bare_if p P ∗ bi_bare_if p Q.
 Proof. destruct p; simpl; auto using bare_sep. Qed.
 
-Lemma bare_if_idemp p P : ■?p ■?p P ⊣⊢ ■?p P.
+Lemma bare_if_idemp p P : bi_bare_if p (bi_bare_if p P) ⊣⊢ bi_bare_if p P.
 Proof. destruct p; simpl; auto using bare_idemp. Qed.
 
 (* Conditional persistently *)
@@ -1208,50 +1228,59 @@ Global Instance persistently_if_flip_mono' p :
   Proper (flip (⊢) ==> flip (⊢)) (@bi_persistently_if PROP p).
 Proof. solve_proper. Qed.
 
-Lemma persistently_if_mono p P Q : (P ⊢ Q) → ⬕?p P ⊢ ⬕?p Q.
+Lemma persistently_if_mono p P Q :
+  (P ⊢ Q) → bi_persistently_if p P ⊢ bi_persistently_if p Q.
 Proof. by intros ->. Qed.
 
-Lemma persistently_if_pure p φ : □?p ⌜φ⌝ ⊣⊢ ⌜φ⌝.
+Lemma persistently_if_pure p φ : bi_persistently_if p ⌜φ⌝ ⊣⊢ ⌜φ⌝.
 Proof. destruct p; simpl; auto using persistently_pure. Qed.
-Lemma persistently_if_and p P Q : □?p (P ∧ Q) ⊣⊢ □?p P ∧ □?p Q.
+Lemma persistently_if_and p P Q :
+  bi_persistently_if p (P ∧ Q) ⊣⊢ bi_persistently_if p P ∧ bi_persistently_if p Q.
 Proof. destruct p; simpl; auto using persistently_and. Qed.
-Lemma persistently_if_or p P Q : □?p (P ∨ Q) ⊣⊢ □?p P ∨ □?p Q.
+Lemma persistently_if_or p P Q :
+  bi_persistently_if p (P ∨ Q) ⊣⊢ bi_persistently_if p P ∨ bi_persistently_if p Q.
 Proof. destruct p; simpl; auto using persistently_or. Qed.
-Lemma persistently_if_exist {A} p (Ψ : A → PROP) : (□?p ∃ a, Ψ a) ⊣⊢ ∃ a, □?p Ψ a.
+Lemma persistently_if_exist {A} p (Ψ : A → PROP) :
+  (bi_persistently_if p (∃ a, Ψ a)) ⊣⊢ ∃ a, bi_persistently_if p (Ψ a).
 Proof. destruct p; simpl; auto using persistently_exist. Qed.
-Lemma persistently_if_sep_2 p P Q : □?p P ∗ □?p Q ⊢ □?p (P ∗ Q).
+Lemma persistently_if_sep_2 p P Q :
+  bi_persistently_if p P ∗ bi_persistently_if p Q ⊢ bi_persistently_if p (P ∗ Q).
 Proof. destruct p; simpl; auto using persistently_sep_2. Qed.
-Lemma persistently_if_sep `{PositiveBI PROP} p P Q : □?p (P ∗ Q) ⊣⊢ □?p P ∗ □?p Q.
+Lemma persistently_if_sep `{PositiveBI PROP} p P Q :
+  bi_persistently_if p (P ∗ Q) ⊣⊢ bi_persistently_if p P ∗ bi_persistently_if p Q.
 Proof. destruct p; simpl; auto using persistently_sep. Qed.
 
-Lemma persistently_if_idemp p P : □?p □?p P ⊣⊢ □?p P.
+Lemma persistently_if_idemp p P :
+  bi_persistently_if p (bi_persistently_if p P) ⊣⊢ bi_persistently_if p P.
 Proof. destruct p; simpl; auto using persistently_idemp. Qed.
 
 (* Conditional bare persistently *)
-Lemma bare_persistently_if_mono p P Q : (P ⊢ Q) → ⬕?p P ⊢ ⬕?p Q.
+Lemma bare_persistently_if_mono p P Q : (P ⊢ Q) → □?p P ⊢ □?p Q.
 Proof. by intros ->. Qed.
 
-Lemma bare_persistently_if_elim p P : ⬕?p P ⊢ P.
+Lemma bare_persistently_if_elim p P : □?p P ⊢ P.
 Proof. destruct p; simpl; auto using bare_persistently_elim. Qed.
-Lemma bare_persistently_bare_persistently_if p P : ⬕ P ⊢ ⬕?p P.
+Lemma bare_persistently_bare_persistently_if p P : □ P ⊢ □?p P.
 Proof. destruct p; simpl; auto using bare_persistently_elim. Qed.
-Lemma bare_persistently_if_intro' p P Q : (⬕?p P ⊢ Q) → ⬕?p P ⊢ ⬕?p Q.
+Lemma bare_persistently_if_intro' p P Q : (□?p P ⊢ Q) → □?p P ⊢ □?p Q.
 Proof. destruct p; simpl; auto using bare_persistently_intro'. Qed.
 
-Lemma bare_persistently_if_emp p : ⬕?p emp ⊣⊢ emp.
+Lemma bare_persistently_if_emp p : □?p emp ⊣⊢ emp.
 Proof. destruct p; simpl; auto using bare_persistently_emp. Qed.
-Lemma bare_persistently_if_and p P Q : ⬕?p (P ∧ Q) ⊣⊢ ⬕?p P ∧ ⬕?p Q.
+Lemma bare_persistently_if_and p P Q : □?p (P ∧ Q) ⊣⊢ □?p P ∧ □?p Q.
 Proof. destruct p; simpl; auto using bare_persistently_and. Qed.
-Lemma bare_persistently_if_or p P Q : ⬕?p (P ∨ Q) ⊣⊢ ⬕?p P ∨ ⬕?p Q.
+Lemma bare_persistently_if_or p P Q : □?p (P ∨ Q) ⊣⊢ □?p P ∨ □?p Q.
 Proof. destruct p; simpl; auto using bare_persistently_or. Qed.
-Lemma bare_persistently_if_exist {A} p (Ψ : A → PROP) : (⬕?p ∃ a, Ψ a) ⊣⊢ ∃ a, ⬕?p Ψ a.
+Lemma bare_persistently_if_exist {A} p (Ψ : A → PROP) :
+  (□?p ∃ a, Ψ a) ⊣⊢ ∃ a, □?p Ψ a.
 Proof. destruct p; simpl; auto using bare_persistently_exist. Qed.
-Lemma bare_persistently_if_sep_2 p P Q : ⬕?p P ∗ ⬕?p Q ⊢ ⬕?p (P ∗ Q).
+Lemma bare_persistently_if_sep_2 p P Q : □?p P ∗ □?p Q ⊢ □?p (P ∗ Q).
 Proof. destruct p; simpl; auto using bare_persistently_sep_2. Qed.
-Lemma bare_persistently_if_sep `{PositiveBI PROP} p P Q : ⬕?p (P ∗ Q) ⊣⊢ ⬕?p P ∗ ⬕?p Q.
+Lemma bare_persistently_if_sep `{PositiveBI PROP} p P Q :
+  □?p (P ∗ Q) ⊣⊢ □?p P ∗ □?p Q.
 Proof. destruct p; simpl; auto using bare_persistently_sep. Qed.
 
-Lemma bare_persistently_if_idemp p P : ⬕?p ⬕?p P ⊣⊢ ⬕?p P.
+Lemma bare_persistently_if_idemp p P : □?p □?p P ⊣⊢ □?p P.
 Proof. destruct p; simpl; auto using bare_persistently_idemp. Qed.
 
 (* Persistence *)
@@ -1295,9 +1324,9 @@ Global Instance sep_persistent P Q :
   Persistent P → Persistent Q → Persistent (P ∗ Q).
 Proof. intros. by rewrite /Persistent -persistently_sep_2 -!persistent. Qed.
 
-Global Instance persistently_persistent P : Persistent (â–¡ P).
+Global Instance persistently_persistent P : Persistent (bi_persistently P).
 Proof. by rewrite /Persistent persistently_idemp. Qed.
-Global Instance bare_persistent P : Persistent P → Persistent (■ P).
+Global Instance bare_persistent P : Persistent P → Persistent (bi_bare P).
 Proof. rewrite /bi_bare. apply _. Qed.
 Global Instance sink_persistent P : Persistent P → Persistent (▲ P).
 Proof. rewrite /bi_sink. apply _. Qed.
@@ -1307,26 +1336,29 @@ Global Instance from_option_persistent {A} P (Ψ : A → PROP) (mx : option A) :
 Proof. destruct mx; apply _. Qed.
 
 (* Properties of persistent propositions *)
-Lemma persistent_persistently_2 P `{!Persistent P} : P ⊢ □ P.
+Lemma persistent_persistently_2 P `{!Persistent P} : P ⊢ bi_persistently P.
 Proof. done. Qed.
-Lemma persistent_persistently P `{!Persistent P, !Absorbing P} : □ P ⊣⊢ P.
-Proof. apply (anti_symm _); auto using persistent_persistently_2, persistently_elim. Qed.
+Lemma persistent_persistently P `{!Persistent P, !Absorbing P} :
+  bi_persistently P ⊣⊢ P.
+Proof.
+  apply (anti_symm _); auto using persistent_persistently_2, persistently_elim.
+Qed.
 
-Lemma persistently_intro P Q `{!Persistent P} : (P ⊢ Q) → P ⊢ □ Q.
+Lemma persistently_intro P Q `{!Persistent P} : (P ⊢ Q) → P ⊢ bi_persistently Q.
 Proof. intros HP. by rewrite (persistent P) HP. Qed.
-Lemma persistent_and_bare_sep_l_1 P Q `{!Persistent P} : P ∧ Q ⊢ ■ P ∗ Q.
+Lemma persistent_and_bare_sep_l_1 P Q `{!Persistent P} : P ∧ Q ⊢ bi_bare P ∗ Q.
 Proof.
   rewrite {1}(persistent_persistently_2 P) persistently_and_bare_sep_l.
   by rewrite -bare_idemp bare_persistently_elim.
 Qed.
-Lemma persistent_and_bare_sep_r_1 P Q `{!Persistent Q} : P ∧ Q ⊢ P ∗ ■ Q.
+Lemma persistent_and_bare_sep_r_1 P Q `{!Persistent Q} : P ∧ Q ⊢ P ∗ bi_bare Q.
 Proof. by rewrite !(comm _ P) persistent_and_bare_sep_l_1. Qed.
 
 Lemma persistent_and_bare_sep_l P Q `{!Persistent P, !Absorbing P} :
-  P ∧ Q ⊣⊢ ■ P ∗ Q.
+  P ∧ Q ⊣⊢ bi_bare P ∗ Q.
 Proof. by rewrite -(persistent_persistently P) persistently_and_bare_sep_l. Qed.
 Lemma persistent_and_bare_sep_r P Q `{!Persistent Q, !Absorbing Q} :
-  P ∧ Q ⊣⊢ P ∗ ■ Q.
+  P ∧ Q ⊣⊢ P ∗ bi_bare Q.
 Proof. by rewrite -(persistent_persistently Q) persistently_and_bare_sep_r. Qed.
 
 Lemma persistent_and_sep_1 P Q `{HPQ : !TCOr (Persistent P) (Persistent Q)} :
@@ -1345,7 +1377,7 @@ Proof. intros. rewrite -persistent_and_sep_1; auto. Qed.
 Lemma persistent_entails_r P Q `{!Persistent Q} : (P ⊢ Q) → P ⊢ P ∗ Q.
 Proof. intros. rewrite -persistent_and_sep_1; auto. Qed.
 
-Lemma persistent_sink_bare P `{!Persistent P} : P ⊢ ▲ ■ P.
+Lemma persistent_sink_bare P `{!Persistent P} : P ⊢ ▲ bi_bare P.
 Proof.
   by rewrite {1}(persistent_persistently_2 P) -persistently_bare
              persistently_elim_sink.
@@ -1383,11 +1415,15 @@ Global Instance bi_sep_monoid : Monoid (@bi_sep PROP) :=
 
 Global Instance bi_persistently_and_homomorphism :
   MonoidHomomorphism bi_and bi_and (≡) (@bi_persistently PROP).
-Proof. split; [split|]; try apply _. apply persistently_and. apply persistently_pure. Qed.
+Proof.
+  split; [split|]; try apply _. apply persistently_and. apply persistently_pure.
+Qed.
 
 Global Instance bi_persistently_or_homomorphism :
   MonoidHomomorphism bi_or bi_or (≡) (@bi_persistently PROP).
-Proof. split; [split|]; try apply _. apply persistently_or. apply persistently_pure. Qed.
+Proof.
+  split; [split|]; try apply _. apply persistently_or. apply persistently_pure.
+Qed.
 
 Global Instance bi_persistently_sep_weak_homomorphism `{PositiveBI PROP} :
   WeakMonoidHomomorphism bi_sep bi_sep (≡) (@bi_persistently PROP).
@@ -1504,13 +1540,13 @@ Lemma later_wand P Q : ▷ (P -∗ Q) ⊢ ▷ P -∗ ▷ Q.
 Proof. apply wand_intro_l. by rewrite -later_sep wand_elim_r. Qed.
 Lemma later_iff P Q : ▷ (P ↔ Q) ⊢ ▷ P ↔ ▷ Q.
 Proof. by rewrite /bi_iff later_and !later_impl. Qed.
-Lemma later_persistently P : ▷ □ P ⊣⊢ □ ▷ P.
+Lemma later_persistently P : ▷ bi_persistently P ⊣⊢ bi_persistently (▷ P).
 Proof. apply (anti_symm _); auto using later_persistently_1, later_persistently_2. Qed.
-Lemma later_bare_2 P : ■ ▷ P ⊢ ▷ ■ P.
+Lemma later_bare_2 P : bi_bare (▷ P) ⊢ ▷ bi_bare P.
 Proof. rewrite /bi_bare later_and. auto using later_intro. Qed.
-Lemma later_bare_persistently_2 P : ⬕ ▷ P ⊢ ▷ ⬕ P.
+Lemma later_bare_persistently_2 P : □ ▷ P ⊢ ▷ □ P.
 Proof. by rewrite -later_persistently later_bare_2. Qed.
-Lemma later_bare_persistently_if_2 p P : ⬕?p ▷ P ⊢ ▷ ⬕?p P.
+Lemma later_bare_persistently_if_2 p P : □?p ▷ P ⊢ ▷ □?p P.
 Proof. destruct p; simpl; auto using later_bare_persistently_2. Qed.
 Lemma later_sink P : ▷ ▲ P ⊣⊢ ▲ ▷ P.
 Proof. by rewrite /bi_sink later_sep later_True. Qed.
@@ -1574,13 +1610,14 @@ Lemma laterN_wand n P Q : ▷^n (P -∗ Q) ⊢ ▷^n P -∗ ▷^n Q.
 Proof. apply wand_intro_l. by rewrite -laterN_sep wand_elim_r. Qed.
 Lemma laterN_iff n P Q : ▷^n (P ↔ Q) ⊢ ▷^n P ↔ ▷^n Q.
 Proof. by rewrite /bi_iff laterN_and !laterN_impl. Qed.
-Lemma laterN_persistently n P : ▷^n □ P ⊣⊢ □ ▷^n P.
+Lemma laterN_persistently n P :
+  ▷^n bi_persistently P ⊣⊢ bi_persistently (▷^n P).
 Proof. induction n as [|n IH]; simpl; auto. by rewrite IH later_persistently. Qed.
-Lemma laterN_bare_2 n P : ■ ▷^n P ⊢ ▷^n ■ P.
+Lemma laterN_bare_2 n P : bi_bare (▷^n P) ⊢ ▷^n bi_bare P.
 Proof. rewrite /bi_bare laterN_and. auto using laterN_intro. Qed.
-Lemma laterN_bare_persistently_2 n P : ⬕ ▷^n P ⊢ ▷^n ⬕ P.
+Lemma laterN_bare_persistently_2 n P : □ ▷^n P ⊢ ▷^n □ P.
 Proof. by rewrite -laterN_persistently laterN_bare_2. Qed.
-Lemma laterN_bare_persistently_if_2 n p P : ⬕?p ▷^n P ⊢ ▷^n ⬕?p P.
+Lemma laterN_bare_persistently_if_2 n p P : □?p ▷^n P ⊢ ▷^n □?p P.
 Proof. destruct p; simpl; auto using laterN_bare_persistently_2. Qed.
 Lemma laterN_sink n P : ▷^n ▲ P ⊣⊢ ▲ ▷^n P.
 Proof. by rewrite /bi_sink laterN_sep laterN_True. Qed.
@@ -1637,13 +1674,15 @@ Proof.
 Qed.
 Lemma except_0_later P : ◇ ▷ P ⊢ ▷ P.
 Proof. by rewrite /bi_except_0 -later_or False_or. Qed.
-Lemma except_0_persistently P : ◇ □ P ⊣⊢ □ ◇ P.
-Proof. by rewrite /bi_except_0 persistently_or -later_persistently persistently_pure. Qed.
-Lemma except_0_bare_2 P : ■ ◇ P ⊢ ◇ ■ P.
+Lemma except_0_persistently P : ◇ bi_persistently P ⊣⊢ bi_persistently (◇ P).
+Proof.
+  by rewrite /bi_except_0 persistently_or -later_persistently persistently_pure.
+Qed.
+Lemma except_0_bare_2 P : bi_bare (◇ P) ⊢ ◇ bi_bare P.
 Proof. rewrite /bi_bare except_0_and. auto using except_0_intro. Qed.
-Lemma except_0_bare_persistently_2 P : ⬕ ◇ P ⊢ ◇ ⬕ P.
+Lemma except_0_bare_persistently_2 P : □ ◇ P ⊢ ◇ □ P.
 Proof. by rewrite -except_0_persistently except_0_bare_2. Qed.
-Lemma except_0_bare_persistently_if_2 p P : ⬕?p ◇ P ⊢ ◇ ⬕?p P.
+Lemma except_0_bare_persistently_if_2 p P : □?p ◇ P ⊢ ◇ □?p P.
 Proof. destruct p; simpl; auto using except_0_bare_persistently_2. Qed.
 Lemma except_0_sink P : ◇ ▲ P ⊣⊢ ▲ ◇ P.
 Proof. by rewrite /bi_sink except_0_sep except_0_True. Qed.
@@ -1653,7 +1692,7 @@ Proof. by rewrite {1}(except_0_intro P) except_0_sep. Qed.
 Lemma except_0_frame_r P Q : ◇ P ∗ Q ⊢ ◇ (P ∗ Q).
 Proof. by rewrite {1}(except_0_intro Q) except_0_sep. Qed.
 
-Lemma later_bare_1 `{!Timeless (emp%I : PROP)} P : ▷ ■ P ⊢ ◇ ■ ▷ P.
+Lemma later_bare_1 `{!Timeless (emp%I : PROP)} P : ▷ bi_bare P ⊢ ◇ bi_bare (▷ P).
 Proof.
   rewrite /bi_bare later_and (timeless emp%I) except_0_and.
   by apply and_mono, except_0_intro.
@@ -1713,14 +1752,14 @@ Proof.
   - rewrite /bi_except_0; auto.
   - apply exist_elim=> x. rewrite -(exist_intro x); auto.
 Qed.
-Global Instance persistently_timeless P : Timeless P → Timeless (□ P).
+Global Instance persistently_timeless P : Timeless P → Timeless (bi_persistently P).
 Proof.
   intros. rewrite /Timeless /bi_except_0 later_persistently_1.
   by rewrite (timeless P) /bi_except_0 persistently_or {1}persistently_elim.
 Qed.
 
 Global Instance bare_timeless P :
-  Timeless (emp%I : PROP) → Timeless P → Timeless (■ P).
+  Timeless (emp%I : PROP) → Timeless P → Timeless (bi_bare P).
 Proof. rewrite /bi_bare; apply _. Qed.
 Global Instance sink_timeless P : Timeless P → Timeless (▲ P).
 Proof. rewrite /bi_sink; apply _. Qed.
diff --git a/theories/bi/fixpoint.v b/theories/bi/fixpoint.v
index 9a7d141acf815fb07a00201f485c024c3605a52e..075440a9f8d3b647754374019a35f809ffdd2201 100644
--- a/theories/bi/fixpoint.v
+++ b/theories/bi/fixpoint.v
@@ -6,7 +6,7 @@ Import bi.
 (** Least and greatest fixpoint of a monotone function, defined entirely inside
     the logic.  *)
 Class BIMonoPred {PROP : bi} {A : ofeT} (F : (A → PROP) → (A → PROP)) := {
-  bi_mono_pred Φ Ψ : ((□ ∀ x, Φ x -∗ Ψ x) → ∀ x, F Φ x -∗ F Ψ x)%I;
+  bi_mono_pred Φ Ψ : ((bi_persistently (∀ x, Φ x -∗ Ψ x)) → ∀ x, F Φ x -∗ F Ψ x)%I;
   bi_mono_pred_ne Φ : NonExpansive Φ → NonExpansive (F Φ)
 }.
 Arguments bi_mono_pred {_ _ _ _} _ _.
@@ -14,11 +14,11 @@ Local Existing Instance bi_mono_pred_ne.
 
 Definition bi_least_fixpoint {PROP : bi} {A : ofeT}
     (F : (A → PROP) → (A → PROP)) (x : A) : PROP :=
-  (∀ Φ : A -n> PROP, □ (∀ x, F Φ x -∗ Φ x) → Φ x)%I.
+  (∀ Φ : A -n> PROP, bi_persistently (∀ x, F Φ x -∗ Φ x) → Φ x)%I.
 
 Definition bi_greatest_fixpoint {PROP : bi} {A : ofeT}
     (F : (A → PROP) → (A → PROP)) (x : A) : PROP :=
-  (∃ Φ : A -n> PROP, □ (∀ x, Φ x -∗ F Φ x) ∧ Φ x)%I.
+  (∃ Φ : A -n> PROP, bi_persistently (∀ x, Φ x -∗ F Φ x) ∧ Φ x)%I.
 
 Section least.
   Context {PROP : bi} {A : ofeT} (F : (A → PROP) → (A → PROP)) `{!BIMonoPred F}.
@@ -48,13 +48,13 @@ Section least.
   Qed.
 
   Lemma least_fixpoint_ind (Φ : A → PROP) `{!NonExpansive Φ} :
-    ⬕ (∀ y, F Φ y -∗ Φ y) -∗ ∀ x, bi_least_fixpoint F x -∗ Φ x.
+    □ (∀ y, F Φ y -∗ Φ y) -∗ ∀ x, bi_least_fixpoint F x -∗ Φ x.
   Proof.
     iIntros "#HΦ" (x) "HF". by iApply ("HF" $! (CofeMor Φ) with "[#]").
   Qed.
 
   Lemma least_fixpoint_strong_ind (Φ : A → PROP) `{!NonExpansive Φ} :
-    ⬕ (∀ y, F (λ x, Φ x ∧ bi_least_fixpoint F x) y -∗ Φ y) -∗
+    □ (∀ y, F (λ x, Φ x ∧ bi_least_fixpoint F x) y -∗ Φ y) -∗
     ∀ x, bi_least_fixpoint F x -∗ Φ x.
   Proof.
     trans (∀ x, bi_least_fixpoint F x -∗ Φ x ∧ bi_least_fixpoint F x)%I.
@@ -96,6 +96,6 @@ Section greatest.
   Qed.
 
   Lemma greatest_fixpoint_coind (Φ : A → PROP) `{!NonExpansive Φ} :
-    ⬕ (∀ y, Φ y -∗ F Φ y) -∗ ∀ x, Φ x -∗ bi_greatest_fixpoint F x.
+    □ (∀ y, Φ y -∗ F Φ y) -∗ ∀ x, Φ x -∗ bi_greatest_fixpoint F x.
   Proof. iIntros "#HΦ" (x) "Hx". iExists (CofeMor Φ). auto. Qed.
 End greatest.
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 7cafc1e6552f3db5507055f81d92fc98dfc35cd5..ced63e3f6d5cc24f02d2df6f8ce8d5d9b66f3041 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -5,7 +5,6 @@ Reserved Notation "'emp'".
 Reserved Notation "'⌜' φ '⌝'" (at level 1, φ at level 200, format "⌜ φ ⌝").
 Reserved Notation "P ∗ Q" (at level 80, right associativity).
 Reserved Notation "P -∗ Q" (at level 99, Q at level 200, right associativity).
-Reserved Notation "â–¡ P" (at level 20, right associativity).
 Reserved Notation "â–· P" (at level 20, right associativity).
 
 Section bi_mixin.
@@ -39,7 +38,6 @@ Section bi_mixin.
   Local Notation "x ≡ y" := (bi_internal_eq _ x y).
   Local Infix "∗" := bi_sep.
   Local Infix "-∗" := bi_wand.
-  Local Notation "â–¡ P" := (bi_persistently P).
   Local Notation "â–· P" := (bi_later P).
 
   Record BIMixin := {
@@ -100,17 +98,21 @@ Section bi_mixin.
     bi_mixin_wand_elim_l' P Q R : (P ⊢ Q -∗ R) → P ∗ Q ⊢ R;
 
     (* Persistently *)
-    bi_mixin_persistently_mono P Q : (P ⊢ Q) → □ P ⊢ □ Q;
-    bi_mixin_persistently_idemp_2 P : □ P ⊢ □ □ P;
+    bi_mixin_persistently_mono P Q :
+      (P ⊢ Q) → bi_persistently P ⊢ bi_persistently Q;
+    bi_mixin_persistently_idemp_2 P :
+      bi_persistently P ⊢ bi_persistently (bi_persistently P);
 
     bi_mixin_persistently_forall_2 {A} (Ψ : A → PROP) :
-      (∀ a, □ Ψ a) ⊢ □ ∀ a, Ψ a;
+      (∀ a, bi_persistently (Ψ a)) ⊢ bi_persistently (∀ a, Ψ a);
     bi_mixin_persistently_exist_1 {A} (Ψ : A → PROP) :
-      □ (∃ a, Ψ a) ⊢ ∃ a, □ Ψ a;
+      bi_persistently (∃ a, Ψ a) ⊢ ∃ a, bi_persistently (Ψ a);
 
-    bi_mixin_persistently_emp_intro P : P ⊢ □ emp;
-    bi_mixin_persistently_absorbing P Q : □ P ∗ Q ⊢ □ P;
-    bi_mixin_persistently_and_sep_elim P Q : □ P ∧ Q ⊢ (emp ∧ P) ∗ Q;
+    bi_mixin_persistently_emp_intro P : P ⊢ bi_persistently emp;
+    bi_mixin_persistently_absorbing P Q :
+      bi_persistently P ∗ Q ⊢ bi_persistently P;
+    bi_mixin_persistently_and_sep_elim P Q :
+      bi_persistently P ∧ Q ⊢ (emp ∧ P) ∗ Q;
   }.
 
   Record SBIMixin := {
@@ -127,8 +129,10 @@ Section bi_mixin.
       (▷ ∃ a, Φ a) ⊢ ▷ False ∨ (∃ a, ▷ Φ a);
     sbi_mixin_later_sep_1 P Q : ▷ (P ∗ Q) ⊢ ▷ P ∗ ▷ Q;
     sbi_mixin_later_sep_2 P Q : ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q);
-    sbi_mixin_later_persistently_1 P : ▷ □ P ⊢ □ ▷ P;
-    sbi_mixin_later_persistently_2 P : □ ▷ P ⊢ ▷ □ P;
+    sbi_mixin_later_persistently_1 P :
+      ▷ bi_persistently P ⊢ bi_persistently (▷ P);
+    sbi_mixin_later_persistently_2 P :
+      bi_persistently (▷ P) ⊢ ▷ bi_persistently P;
 
     sbi_mixin_later_false_em P : ▷ P ⊢ ▷ False ∨ (▷ False → P);
   }.
@@ -281,7 +285,6 @@ Notation "∀ x .. y , P" :=
   (bi_forall (λ x, .. (bi_forall (λ y, P)) ..)%I) : bi_scope.
 Notation "∃ x .. y , P" :=
   (bi_exist (λ x, .. (bi_exist (λ y, P)) ..)%I) : bi_scope.
-Notation "â–¡ P" := (bi_persistently P) : bi_scope.
 
 Infix "≡" := bi_internal_eq : bi_scope.
 Notation "â–· P" := (bi_later P) : bi_scope.
@@ -399,21 +402,24 @@ Lemma wand_elim_l' P Q R : (P ⊢ Q -∗ R) → P ∗ Q ⊢ R.
 Proof. eapply bi_mixin_wand_elim_l', bi_bi_mixin. Qed.
 
 (* Persistently *)
-Lemma persistently_mono P Q : (P ⊢ Q) → □ P ⊢ □ Q.
+Lemma persistently_mono P Q : (P ⊢ Q) → bi_persistently P ⊢ bi_persistently Q.
 Proof. eapply bi_mixin_persistently_mono, bi_bi_mixin. Qed.
-Lemma persistently_idemp_2 P : □ P ⊢ □ □ P.
+Lemma persistently_idemp_2 P :
+  bi_persistently P ⊢ bi_persistently (bi_persistently P).
 Proof. eapply bi_mixin_persistently_idemp_2, bi_bi_mixin. Qed.
 
-Lemma persistently_forall_2 {A} (Ψ : A → PROP) : (∀ a, □ Ψ a) ⊢ □ ∀ a, Ψ a.
+Lemma persistently_forall_2 {A} (Ψ : A → PROP) :
+  (∀ a, bi_persistently (Ψ a)) ⊢ bi_persistently (∀ a, Ψ a).
 Proof. eapply bi_mixin_persistently_forall_2, bi_bi_mixin. Qed.
-Lemma persistently_exist_1 {A} (Ψ : A → PROP) : □ (∃ a, Ψ a) ⊢ ∃ a, □ Ψ a.
+Lemma persistently_exist_1 {A} (Ψ : A → PROP) :
+  bi_persistently (∃ a, Ψ a) ⊢ ∃ a, bi_persistently (Ψ a).
 Proof. eapply bi_mixin_persistently_exist_1, bi_bi_mixin. Qed.
 
-Lemma persistently_emp_intro P : P ⊢ □ emp.
+Lemma persistently_emp_intro P : P ⊢ bi_persistently emp.
 Proof. eapply bi_mixin_persistently_emp_intro, bi_bi_mixin. Qed.
-Lemma persistently_absorbing P Q : □ P ∗ Q ⊢ □ P.
+Lemma persistently_absorbing P Q : bi_persistently P ∗ Q ⊢ bi_persistently P.
 Proof. eapply (bi_mixin_persistently_absorbing bi_entails), bi_bi_mixin. Qed.
-Lemma persistently_and_sep_elim P Q : □ P ∧ Q ⊢ (emp ∧ P) ∗ Q.
+Lemma persistently_and_sep_elim P Q : bi_persistently P ∧ Q ⊢ (emp ∧ P) ∗ Q.
 Proof. eapply bi_mixin_persistently_and_sep_elim, bi_bi_mixin. Qed.
 End bi_laws.
 
@@ -444,9 +450,9 @@ Lemma later_sep_1 P Q : ▷ (P ∗ Q) ⊢ ▷ P ∗ ▷ Q.
 Proof. eapply sbi_mixin_later_sep_1, sbi_sbi_mixin. Qed.
 Lemma later_sep_2 P Q : ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q).
 Proof. eapply sbi_mixin_later_sep_2, sbi_sbi_mixin. Qed.
-Lemma later_persistently_1 P : ▷ □ P ⊢ □ ▷ P.
+Lemma later_persistently_1 P : ▷ bi_persistently P ⊢ bi_persistently (▷ P).
 Proof. eapply (sbi_mixin_later_persistently_1 bi_entails), sbi_sbi_mixin. Qed.
-Lemma later_persistently_2 P : □ ▷ P ⊢ ▷ □ P.
+Lemma later_persistently_2 P : bi_persistently (▷ P) ⊢ ▷ bi_persistently P.
 Proof. eapply (sbi_mixin_later_persistently_2 bi_entails), sbi_sbi_mixin. Qed.
 
 Lemma later_false_em P : ▷ P ⊢ ▷ False ∨ (▷ False → P).
diff --git a/theories/program_logic/hoare.v b/theories/program_logic/hoare.v
index f465765b473d5b432cc5bc96614bb96f61ff5a48..7ff1a8c9971cc43126864596de37e662d0b1fbef 100644
--- a/theories/program_logic/hoare.v
+++ b/theories/program_logic/hoare.v
@@ -37,7 +37,7 @@ Global Instance ht_proper E :
 Proof. solve_proper. Qed.
 Lemma ht_mono E P P' Φ Φ' e :
   (P ⊢ P') → (∀ v, Φ' v ⊢ Φ v) → {{ P' }} e @ E {{ Φ' }} ⊢ {{ P }} e @ E {{ Φ }}.
-Proof. by intros; apply persistently_mono, wand_mono, wp_mono. Qed.
+Proof. intros. by apply bare_mono, persistently_mono, wand_mono, wp_mono. Qed.
 Global Instance ht_mono' E :
   Proper (flip (⊢) ==> eq ==> pointwise_relation _ (⊢) ==> (⊢)) (ht E).
 Proof. solve_proper. Qed.
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 4449a272b5a39953f5061fca252cd53ce909ddab..96a456cb61a4ed7758dd5f07f0e2ae6612e8f501 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -12,19 +12,19 @@ Global Instance into_internal_eq_internal_eq {A : ofeT} (x y : A) :
   @IntoInternalEq PROP A (x ≡ y) x y.
 Proof. by rewrite /IntoInternalEq. Qed.
 Global Instance into_internal_eq_bare {A : ofeT} (x y : A) P :
-  IntoInternalEq P x y → IntoInternalEq (■ P) x y.
+  IntoInternalEq P x y → IntoInternalEq (bi_bare P) x y.
 Proof. rewrite /IntoInternalEq=> ->. by rewrite bare_elim. Qed.
 Global Instance into_internal_eq_sink {A : ofeT} (x y : A) P :
   IntoInternalEq P x y → IntoInternalEq (▲ P) x y.
 Proof. rewrite /IntoInternalEq=> ->. by rewrite sink_internal_eq. Qed.
 Global Instance into_internal_eq_persistently {A : ofeT} (x y : A) P :
-  IntoInternalEq P x y → IntoInternalEq (□ P) x y.
+  IntoInternalEq P x y → IntoInternalEq (bi_persistently P) x y.
 Proof. rewrite /IntoInternalEq=> ->. by rewrite persistently_elim. Qed.
 
 (* FromBare *)
 Global Instance from_bare_affine P : Affine P → FromBare P P.
 Proof. intros. by rewrite /FromBare bare_elim. Qed.
-Global Instance from_bare_default P : FromBare (â–  P) P | 100.
+Global Instance from_bare_default P : FromBare (bi_bare P) P | 100.
 Proof. by rewrite /FromBare. Qed.
 
 (* IntoSink *)
@@ -40,29 +40,29 @@ Global Instance from_assumption_exact p P : FromAssumption p P P | 0.
 Proof. by rewrite /FromAssumption /= bare_persistently_if_elim. Qed.
 
 Global Instance from_assumption_persistently_r P Q :
-  FromAssumption true P Q → FromAssumption true P (□ Q).
+  FromAssumption true P Q → FromAssumption true P (bi_persistently Q).
 Proof.
   rewrite /FromAssumption /= =><-.
   by rewrite -{1}bare_persistently_idemp bare_elim.
 Qed.
 Global Instance from_assumption_bare_r P Q :
-  FromAssumption true P Q → FromAssumption true P (■ Q).
+  FromAssumption true P Q → FromAssumption true P (bi_bare Q).
 Proof. rewrite /FromAssumption /= =><-. by rewrite bare_idemp. Qed.
 Global Instance from_assumption_sink_r p P Q :
   FromAssumption p P Q → FromAssumption p P (▲ Q).
 Proof. rewrite /FromAssumption /= =><-. apply sink_intro. Qed.
 
 Global Instance from_assumption_bare_persistently_l p P Q :
-  FromAssumption true P Q → FromAssumption p (⬕ P) Q.
+  FromAssumption true P Q → FromAssumption p (□ P) Q.
 Proof. rewrite /FromAssumption /= =><-. by rewrite bare_persistently_if_elim. Qed.
 Global Instance from_assumption_persistently_l_true P Q :
-  FromAssumption true P Q → FromAssumption true (□ P) Q.
+  FromAssumption true P Q → FromAssumption true (bi_persistently P) Q.
 Proof. rewrite /FromAssumption /= =><-. by rewrite persistently_idemp. Qed.
 Global Instance from_assumption_persistently_l_false `{AffineBI PROP} P Q :
-  FromAssumption true P Q → FromAssumption false (□ P) Q.
+  FromAssumption true P Q → FromAssumption false (bi_persistently P) Q.
 Proof. rewrite /FromAssumption /= =><-. by rewrite affine_bare. Qed.
 Global Instance from_assumption_bare_l_true p P Q :
-  FromAssumption p P Q → FromAssumption p (■ P) Q.
+  FromAssumption p P Q → FromAssumption p (bi_bare P) Q.
 Proof. rewrite /FromAssumption /= =><-. by rewrite bare_elim. Qed.
 
 Global Instance from_assumption_forall {A} p (Φ : A → PROP) Q x :
@@ -101,11 +101,11 @@ Global Instance into_pure_pure_wand (φ1 φ2 : Prop) P1 P2 :
   FromPure P1 φ1 → IntoPure P2 φ2 → IntoPure (P1 -∗ P2) (φ1 → φ2).
 Proof. rewrite /FromPure /IntoPure=> <- ->. by rewrite pure_impl impl_wand_2. Qed.
 
-Global Instance into_pure_bare P φ : IntoPure P φ → IntoPure (■ P) φ.
+Global Instance into_pure_bare P φ : IntoPure P φ → IntoPure (bi_bare P) φ.
 Proof. rewrite /IntoPure=> ->. apply bare_elim. Qed.
 Global Instance into_pure_sink P φ : IntoPure P φ → IntoPure (▲ P) φ.
 Proof. rewrite /IntoPure=> ->. by rewrite sink_pure. Qed.
-Global Instance into_pure_persistently P φ : IntoPure P φ → IntoPure (□ P) φ.
+Global Instance into_pure_persistently P φ : IntoPure P φ → IntoPure (bi_persistently P) φ.
 Proof. rewrite /IntoPure=> ->. apply: persistently_elim. Qed.
 
 (* FromPure *)
@@ -142,20 +142,24 @@ Proof.
   by rewrite pure_wand_forall pure_impl pure_impl_forall.
 Qed.
 
-Global Instance from_pure_persistently P φ : FromPure P φ → FromPure (□ P) φ.
+Global Instance from_pure_persistently P φ :
+  FromPure P φ → FromPure (bi_persistently P) φ.
 Proof. rewrite /FromPure=> <-. by rewrite persistently_pure. Qed.
+Global Instance from_pure_bare P φ `{!Affine P} :
+  FromPure P φ → FromPure (bi_bare P) φ.
+Proof. by rewrite /FromPure affine_bare. Qed.
 Global Instance from_pure_sink P φ : FromPure P φ → FromPure (▲ P) φ.
 Proof. rewrite /FromPure=> <-. by rewrite sink_pure. Qed.
 
 (* IntoPersistent *)
 Global Instance into_persistent_persistently p P Q :
-  IntoPersistent true P Q → IntoPersistent p (□ P) Q | 0.
+  IntoPersistent true P Q → IntoPersistent p (bi_persistently P) Q | 0.
 Proof.
   rewrite /IntoPersistent /= => ->.
   destruct p; simpl; auto using persistently_idemp_1.
 Qed.
 Global Instance into_persistent_bare p P Q :
-  IntoPersistent p P Q → IntoPersistent p (■ P) Q | 0.
+  IntoPersistent p P Q → IntoPersistent p (bi_bare P) Q | 0.
 Proof. rewrite /IntoPersistent /= => <-. by rewrite bare_elim. Qed.
 Global Instance into_persistent_here P : IntoPersistent true P P | 1.
 Proof. by rewrite /IntoPersistent. Qed.
@@ -167,12 +171,12 @@ Proof. intros. by rewrite /IntoPersistent. Qed.
 Global Instance from_persistent_here P : FromPersistent false false P P | 1.
 Proof. by rewrite /FromPersistent. Qed.
 Global Instance from_persistent_persistently a P Q :
-  FromPersistent a false P Q → FromPersistent false true (□ P) Q | 0.
+  FromPersistent a false P Q → FromPersistent false true (bi_persistently P) Q | 0.
 Proof.
   rewrite /FromPersistent /= => <-. by destruct a; rewrite /= ?persistently_bare.
 Qed.
 Global Instance from_persistent_bare a p P Q :
-  FromPersistent a p P Q → FromPersistent true p (■ P) Q | 0.
+  FromPersistent a p P Q → FromPersistent true p (bi_bare P) Q | 0.
 Proof. rewrite /FromPersistent /= => <-. destruct a; by rewrite /= ?bare_idemp. Qed.
 
 (* IntoWand *)
@@ -227,14 +231,14 @@ Global Instance into_wand_forall {A} p q (Φ : A → PROP) P Q x :
 Proof. rewrite /IntoWand=> <-. by rewrite (forall_elim x). Qed.
 
 Global Instance into_wand_persistently_true q R P Q :
-  IntoWand true q R P Q → IntoWand true q (□ R) P Q.
+  IntoWand true q R P Q → IntoWand true q (bi_persistently R) P Q.
 Proof. by rewrite /IntoWand /= persistently_idemp. Qed.
 Global Instance into_wand_persistently_false `{!AffineBI PROP} q R P Q :
-  IntoWand false q R P Q → IntoWand false q (□ R) P Q.
+  IntoWand false q R P Q → IntoWand false q (bi_persistently R) P Q.
 Proof. by rewrite /IntoWand persistently_elim. Qed.
 
 Global Instance into_wand_bare_persistently p q R P Q :
-  IntoWand p q R P Q → IntoWand p q (⬕ R) P Q.
+  IntoWand p q R P Q → IntoWand p q (□ R) P Q.
 Proof. by rewrite /IntoWand bare_persistently_elim. Qed.
 
 (* FromAnd *)
@@ -260,10 +264,12 @@ Global Instance from_and_pure φ ψ : @FromAnd PROP ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜
 Proof. by rewrite /FromAnd pure_and. Qed.
 
 Global Instance from_and_persistently P Q1 Q2 :
-  FromAnd P Q1 Q2 → FromAnd (□ P) (□ Q1) (□ Q2).
+  FromAnd P Q1 Q2 →
+  FromAnd (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
 Proof. rewrite /FromAnd=> <-. by rewrite persistently_and. Qed.
 Global Instance from_and_persistently_sep P Q1 Q2 :
-  FromSep P Q1 Q2 → FromAnd (□ P) (□ Q1) (□ Q2) | 11.
+  FromSep P Q1 Q2 →
+  FromAnd (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2) | 11.
 Proof. rewrite /FromAnd=> <-. by rewrite -persistently_and persistently_and_sep. Qed.
 
 Global Instance from_and_big_sepL_cons_persistent {A} (Φ : nat → A → PROP) x l :
@@ -288,13 +294,14 @@ Global Instance from_sep_pure φ ψ : @FromSep PROP ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜
 Proof. by rewrite /FromSep pure_and sep_and. Qed.
 
 Global Instance from_sep_bare P Q1 Q2 :
-  FromSep P Q1 Q2 → FromSep (■ P) (■ Q1) (■ Q2).
+  FromSep P Q1 Q2 → FromSep (bi_bare P) (bi_bare Q1) (bi_bare Q2).
 Proof. rewrite /FromSep=> <-. by rewrite bare_sep_2. Qed.
 Global Instance from_sep_sink P Q1 Q2 :
   FromSep P Q1 Q2 → FromSep (▲ P) (▲ Q1) (▲ Q2).
 Proof. rewrite /FromSep=> <-. by rewrite sink_sep. Qed.
 Global Instance from_sep_persistently P Q1 Q2 :
-  FromSep P Q1 Q2 → FromSep (□ P) (□ Q1) (□ Q2).
+  FromSep P Q1 Q2 →
+  FromSep (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
 Proof. rewrite /FromSep=> <-. by rewrite persistently_sep_2. Qed.
 
 Global Instance from_sep_big_sepL_cons {A} (Φ : nat → A → PROP) x l :
@@ -322,20 +329,23 @@ Proof.
 Qed.
 
 Global Instance into_and_sep `{PositiveBI PROP} P Q : IntoAnd true (P ∗ Q) P Q.
-Proof. by rewrite /IntoAnd /= persistently_sep -and_sep_persistently persistently_and. Qed.
+Proof.
+  by rewrite /IntoAnd /= persistently_sep -and_sep_persistently persistently_and.
+Qed.
 
 Global Instance into_and_pure p φ ψ : @IntoAnd PROP p ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
 Proof. by rewrite /IntoAnd pure_and bare_persistently_if_and. Qed.
 
 Global Instance into_and_bare p P Q1 Q2 :
-  IntoAnd p P Q1 Q2 → IntoAnd p (■ P) (■ Q1) (■ Q2).
+  IntoAnd p P Q1 Q2 → IntoAnd p (bi_bare P) (bi_bare Q1) (bi_bare Q2).
 Proof.
   rewrite /IntoAnd. destruct p; simpl.
   - by rewrite -bare_and !persistently_bare.
   - intros ->. by rewrite bare_and.
 Qed.
 Global Instance into_and_persistently p P Q1 Q2 :
-  IntoAnd p P Q1 Q2 → IntoAnd p (□ P) (□ Q1) (□ Q2).
+  IntoAnd p P Q1 Q2 →
+  IntoAnd p (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
 Proof.
   rewrite /IntoAnd /=. destruct p; simpl.
   - by rewrite -persistently_and !persistently_idemp.
@@ -348,7 +358,7 @@ Proof. by rewrite /IntoSep. Qed.
 
 Inductive AndIntoSep : PROP → PROP → PROP → PROP → Prop :=
   | and_into_sep_affine P Q Q' : Affine P → FromBare Q' Q → AndIntoSep P P Q Q'
-  | and_into_sep P Q : AndIntoSep P (â–  P)%I Q Q.
+  | and_into_sep P Q : AndIntoSep P (bi_bare P)%I Q Q.
 Existing Class AndIntoSep.
 Global Existing Instance and_into_sep_affine | 0.
 Global Existing Instance and_into_sep | 2.
@@ -374,14 +384,15 @@ Qed.
 Global Instance into_sep_pure φ ψ : @IntoSep PROP ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
 Proof. by rewrite /IntoSep pure_and persistent_and_sep_1. Qed.
 
-(* FIXME: This instance is kind of strange, it just gets rid of the â– . Also, it
+(* FIXME: This instance is kind of strange, it just gets rid of the bi_bare. Also, it
 overlaps with `into_sep_bare_later`, and hence has lower precedence. *)
 Global Instance into_sep_bare P Q1 Q2 :
-  IntoSep P Q1 Q2 → IntoSep (■ P) Q1 Q2 | 20.
+  IntoSep P Q1 Q2 → IntoSep (bi_bare P) Q1 Q2 | 20.
 Proof. rewrite /IntoSep /= => ->. by rewrite bare_elim. Qed.
 
 Global Instance into_sep_persistently `{PositiveBI PROP} P Q1 Q2 :
-  IntoSep P Q1 Q2 → IntoSep (□ P) (□ Q1) (□ Q2).
+  IntoSep P Q1 Q2 →
+  IntoSep (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
 Proof. rewrite /IntoSep /= => ->. by rewrite persistently_sep. Qed.
 
 (* We use [IsCons] and [IsApp] to make sure that [frame_big_sepL_cons] and
@@ -404,13 +415,14 @@ Proof. by rewrite /FromOr. Qed.
 Global Instance from_or_pure φ ψ : @FromOr PROP ⌜φ ∨ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
 Proof. by rewrite /FromOr pure_or. Qed.
 Global Instance from_or_bare P Q1 Q2 :
-  FromOr P Q1 Q2 → FromOr (■ P) (■ Q1) (■ Q2).
+  FromOr P Q1 Q2 → FromOr (bi_bare P) (bi_bare Q1) (bi_bare Q2).
 Proof. rewrite /FromOr=> <-. by rewrite bare_or. Qed.
 Global Instance from_or_sink P Q1 Q2 :
   FromOr P Q1 Q2 → FromOr (▲ P) (▲ Q1) (▲ Q2).
 Proof. rewrite /FromOr=> <-. by rewrite sink_or. Qed.
 Global Instance from_or_persistently P Q1 Q2 :
-  FromOr P Q1 Q2 → FromOr (□ P) (□ Q1) (□ Q2).
+  FromOr P Q1 Q2 →
+  FromOr (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
 Proof. rewrite /FromOr=> <-. by rewrite persistently_or. Qed.
 
 (* IntoOr *)
@@ -419,13 +431,14 @@ Proof. by rewrite /IntoOr. Qed.
 Global Instance into_or_pure φ ψ : @IntoOr PROP ⌜φ ∨ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
 Proof. by rewrite /IntoOr pure_or. Qed.
 Global Instance into_or_bare P Q1 Q2 :
-  IntoOr P Q1 Q2 → IntoOr (■ P) (■ Q1) (■ Q2).
+  IntoOr P Q1 Q2 → IntoOr (bi_bare P) (bi_bare Q1) (bi_bare Q2).
 Proof. rewrite /IntoOr=>->. by rewrite bare_or. Qed.
 Global Instance into_or_sink P Q1 Q2 :
   IntoOr P Q1 Q2 → IntoOr (▲ P) (▲ Q1) (▲ Q2).
 Proof. rewrite /IntoOr=>->. by rewrite sink_or. Qed.
 Global Instance into_or_persistently P Q1 Q2 :
-  IntoOr P Q1 Q2 → IntoOr (□ P) (□ Q1) (□ Q2).
+  IntoOr P Q1 Q2 →
+  IntoOr (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
 Proof. rewrite /IntoOr=>->. by rewrite persistently_or. Qed.
 
 (* FromExist *)
@@ -435,13 +448,13 @@ Global Instance from_exist_pure {A} (φ : A → Prop) :
   @FromExist PROP A ⌜∃ x, φ x⌝ (λ a, ⌜φ a⌝)%I.
 Proof. by rewrite /FromExist pure_exist. Qed.
 Global Instance from_exist_bare {A} P (Φ : A → PROP) :
-  FromExist P Φ → FromExist (■ P) (λ a, ■ (Φ a))%I.
+  FromExist P Φ → FromExist (bi_bare P) (λ a, bi_bare (Φ a))%I.
 Proof. rewrite /FromExist=> <-. by rewrite bare_exist. Qed.
 Global Instance from_exist_sink {A} P (Φ : A → PROP) :
   FromExist P Φ → FromExist (▲ P) (λ a, ▲ (Φ a))%I.
 Proof. rewrite /FromExist=> <-. by rewrite sink_exist. Qed.
 Global Instance from_exist_persistently {A} P (Φ : A → PROP) :
-  FromExist P Φ → FromExist (□ P) (λ a, □ (Φ a))%I.
+  FromExist P Φ → FromExist (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
 Proof. rewrite /FromExist=> <-. by rewrite persistently_exist. Qed.
 
 (* IntoExist *)
@@ -451,7 +464,7 @@ Global Instance into_exist_pure {A} (φ : A → Prop) :
   @IntoExist PROP A ⌜∃ x, φ x⌝ (λ a, ⌜φ a⌝)%I.
 Proof. by rewrite /IntoExist pure_exist. Qed.
 Global Instance into_exist_bare {A} P (Φ : A → PROP) :
-  IntoExist P Φ → IntoExist (■ P) (λ a, ■ (Φ a))%I.
+  IntoExist P Φ → IntoExist (bi_bare P) (λ a, bi_bare (Φ a))%I.
 Proof. rewrite /IntoExist=> HP. by rewrite HP bare_exist. Qed.
 Global Instance into_exist_and_pure P Q φ :
   IntoPureT P φ → IntoExist (P ∧ Q) (λ _ : φ, Q).
@@ -470,17 +483,17 @@ Global Instance into_exist_sink {A} P (Φ : A → PROP) :
   IntoExist P Φ → IntoExist (▲ P) (λ a, ▲ (Φ a))%I.
 Proof. rewrite /IntoExist=> HP. by rewrite HP sink_exist. Qed.
 Global Instance into_exist_persistently {A} P (Φ : A → PROP) :
-  IntoExist P Φ → IntoExist (□ P) (λ a, □ (Φ a))%I.
+  IntoExist P Φ → IntoExist (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
 Proof. rewrite /IntoExist=> HP. by rewrite HP persistently_exist. Qed.
 
 (* IntoForall *)
 Global Instance into_forall_forall {A} (Φ : A → PROP) : IntoForall (∀ a, Φ a) Φ.
 Proof. by rewrite /IntoForall. Qed.
 Global Instance into_forall_bare {A} P (Φ : A → PROP) :
-  IntoForall P Φ → IntoForall (■ P) (λ a, ■ (Φ a))%I.
+  IntoForall P Φ → IntoForall (bi_bare P) (λ a, bi_bare (Φ a))%I.
 Proof. rewrite /IntoForall=> HP. by rewrite HP bare_forall. Qed.
 Global Instance into_forall_persistently {A} P (Φ : A → PROP) :
-  IntoForall P Φ → IntoForall (□ P) (λ a, □ (Φ a))%I.
+  IntoForall P Φ → IntoForall (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
 Proof. rewrite /IntoForall=> HP. by rewrite HP persistently_forall. Qed.
 
 (* FromForall *)
@@ -505,8 +518,11 @@ Proof.
   - by rewrite (into_pure P) -pure_wand_forall wand_elim_l.
 Qed.
 
+Global Instance from_forall_bare `{AffineBI PROP} {A} P (Φ : A → PROP) :
+  FromForall P Φ → FromForall (bi_bare P)%I (λ a, bi_bare (Φ a))%I.
+Proof. rewrite /FromForall=> <-. rewrite affine_bare. by setoid_rewrite bare_elim. Qed.
 Global Instance from_forall_persistently {A} P (Φ : A → PROP) :
-  FromForall P Φ → FromForall (□ P)%I (λ a, □ (Φ a))%I.
+  FromForall P Φ → FromForall (bi_persistently P)%I (λ a, bi_persistently (Φ a))%I.
 Proof. rewrite /FromForall=> <-. by rewrite persistently_forall. Qed.
 
 (* ElimModal *)
@@ -531,9 +547,10 @@ Global Instance frame_here_absorbing p R : Absorbing R → Frame p R R True | 0.
 Proof. intros. by rewrite /Frame bare_persistently_if_elim sep_elim_l. Qed.
 Global Instance frame_here p R : Frame p R R emp | 1.
 Proof. intros. by rewrite /Frame bare_persistently_if_elim sep_elim_l. Qed.
-Global Instance frame_bare_here_absorbing p R : Absorbing R → Frame p (■ R) R True | 0.
+Global Instance frame_bare_here_absorbing p R :
+  Absorbing R → Frame p (bi_bare R) R True | 0.
 Proof. intros. by rewrite /Frame bare_persistently_if_elim bare_elim sep_elim_l. Qed.
-Global Instance frame_bare_here p R : Frame p (â–  R) R emp | 1.
+Global Instance frame_bare_here p R : Frame p (bi_bare R) R emp | 1.
 Proof. intros. by rewrite /Frame bare_persistently_if_elim bare_elim sep_elim_l. Qed.
 
 Global Instance frame_here_pure p φ Q : FromPure Q φ → Frame p ⌜φ⌝ Q True.
@@ -592,11 +609,11 @@ Global Instance make_and_true_r P : MakeAnd P True P.
 Proof. by rewrite /MakeAnd right_id. Qed.
 Global Instance make_and_emp_l P : Affine P → MakeAnd emp P P.
 Proof. intros. by rewrite /MakeAnd emp_and. Qed.
-Global Instance make_and_emp_l_bare P : MakeAnd emp P (â–  P) | 10.
+Global Instance make_and_emp_l_bare P : MakeAnd emp P (bi_bare P) | 10.
 Proof. intros. by rewrite /MakeAnd. Qed.
 Global Instance make_and_emp_r P : Affine P → MakeAnd P emp P.
 Proof. intros. by rewrite /MakeAnd and_emp. Qed.
-Global Instance make_and_emp_r_bare P : MakeAnd P emp (â–  P) | 10.
+Global Instance make_and_emp_r_bare P : MakeAnd P emp (bi_bare P) | 10.
 Proof. intros. by rewrite /MakeAnd comm. Qed.
 Global Instance make_and_default P Q : MakeAnd P Q (P ∧ Q) | 100.
 Proof. by rewrite /MakeAnd. Qed.
@@ -661,17 +678,17 @@ Proof.
   by rewrite assoc (comm _ P1) -assoc wand_elim_r.
 Qed.
 
-Class MakeBare (P Q : PROP) := make_bare : ■ P ⊣⊢ Q.
+Class MakeBare (P Q : PROP) := make_bare : bi_bare P ⊣⊢ Q.
 Arguments MakeBare _%I _%I.
 Global Instance make_bare_True : MakeBare True emp | 0.
 Proof. by rewrite /MakeBare bare_True_emp bare_emp. Qed.
 Global Instance make_bare_affine P : Affine P → MakeBare P P | 1.
 Proof. intros. by rewrite /MakeBare affine_bare. Qed.
-Global Instance make_bare_default P : MakeBare P (â–  P) | 100.
+Global Instance make_bare_default P : MakeBare P (bi_bare P) | 100.
 Proof. by rewrite /MakeBare. Qed.
 
 Global Instance frame_bare R P Q Q' :
-  Frame true R P Q → MakeBare Q Q' → Frame true R (■ P) Q'.
+  Frame true R P Q → MakeBare Q Q' → Frame true R (bi_bare P) Q'.
 Proof.
   rewrite /Frame /MakeBare=> <- <- /=.
   by rewrite -{1}bare_idemp bare_sep_2.
@@ -691,17 +708,17 @@ Global Instance frame_sink p R P Q Q' :
   Frame p R P Q → MakeSink Q Q' → Frame p R (▲ P) Q'.
 Proof. rewrite /Frame /MakeSink=> <- <- /=. by rewrite sink_sep_r. Qed.
 
-Class MakePersistently (P Q : PROP) := make_persistently : □ P ⊣⊢ Q.
+Class MakePersistently (P Q : PROP) := make_persistently : bi_persistently P ⊣⊢ Q.
 Arguments MakePersistently _%I _%I.
 Global Instance make_persistently_true : MakePersistently True True.
 Proof. by rewrite /MakePersistently persistently_pure. Qed.
 Global Instance make_persistently_emp : MakePersistently emp True.
 Proof. by rewrite /MakePersistently -persistently_True_emp persistently_pure. Qed.
-Global Instance make_persistently_default P : MakePersistently P (â–¡ P) | 100.
+Global Instance make_persistently_default P : MakePersistently P (bi_persistently P) | 100.
 Proof. by rewrite /MakePersistently. Qed.
 
 Global Instance frame_persistently R P Q Q' :
-  Frame true R P Q → MakePersistently Q Q' → Frame true R (□ P) Q'.
+  Frame true R P Q → MakePersistently Q Q' → Frame true R (bi_persistently P) Q'.
 Proof.
   rewrite /Frame /MakePersistently=> <- <- /=. rewrite -persistently_and_bare_sep_l.
   by rewrite -persistently_sep_2 -persistently_and_sep_l_1 persistently_bare
@@ -755,7 +772,7 @@ Global Instance into_wand_later_args p q R P Q :
   IntoWand p q R P Q → IntoWand' p q R (▷ P) (▷ Q).
 Proof.
   rewrite /IntoWand' /IntoWand /= => HR.
-  by rewrite !later_bare_persistently_if_2 (later_intro (⬕?p R)%I) -later_wand HR.
+  by rewrite !later_bare_persistently_if_2 (later_intro (â–¡?p R)%I) -later_wand HR.
 Qed.
 
 Global Instance into_wand_laterN n p q R P Q :
@@ -768,7 +785,7 @@ Global Instance into_wand_laterN_args n p q R P Q :
   IntoWand p q R P Q → IntoWand' p q R (▷^n P) (▷^n Q).
 Proof.
   rewrite /IntoWand' /IntoWand /= => HR.
-  by rewrite !laterN_bare_persistently_if_2 (laterN_intro _ (⬕?p R)%I) -laterN_wand HR.
+  by rewrite !laterN_bare_persistently_if_2 (laterN_intro _ (â–¡?p R)%I) -laterN_wand HR.
 Qed.
 
 (* FromAnd *)
@@ -826,12 +843,13 @@ Proof. rewrite /IntoSep=> ->. by rewrite except_0_sep. Qed.
 
 (* FIXME: This instance is overly specific, generalize it. *)
 Global Instance into_sep_bare_later `{!Timeless (emp%I : PROP)} P Q1 Q2 :
-  Affine Q1 → Affine Q2 → IntoSep P Q1 Q2 → IntoSep (■ ▷ P) (■ ▷ Q1) (■ ▷ Q2).
+  Affine Q1 → Affine Q2 → IntoSep P Q1 Q2 →
+  IntoSep (bi_bare (â–· P)) (bi_bare (â–· Q1)) (bi_bare (â–· Q2)).
 Proof.
   rewrite /IntoSep /= => ?? ->.
   rewrite -{1}(affine_bare Q1) -{1}(affine_bare Q2) later_sep !later_bare_1.
   rewrite -except_0_sep /bi_except_0 bare_or. apply or_elim, bare_elim.
-  rewrite -(idemp bi_and (â–  â–· False)%I) persistent_and_sep_1.
+  rewrite -(idemp bi_and (bi_bare (â–· False))%I) persistent_and_sep_1.
   by rewrite -(False_elim Q1) -(False_elim Q2).
 Qed.
 
@@ -913,11 +931,13 @@ Proof. by rewrite /IntoExcept0. Qed.
 Global Instance into_timeless_later_if p P : Timeless P → IntoExcept0 (▷?p P) P.
 Proof. rewrite /IntoExcept0. destruct p; auto using except_0_intro. Qed.
 
-Global Instance into_timeless_bare P Q : IntoExcept0 P Q → IntoExcept0 (■ P) (■ Q).
+Global Instance into_timeless_bare P Q :
+  IntoExcept0 P Q → IntoExcept0 (bi_bare P) (bi_bare Q).
 Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_bare_2. Qed.
 Global Instance into_timeless_sink P Q : IntoExcept0 P Q → IntoExcept0 (▲ P) (▲ Q).
 Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_sink. Qed.
-Global Instance into_timeless_persistently P Q : IntoExcept0 P Q → IntoExcept0 (□ P) (□ Q).
+Global Instance into_timeless_persistently P Q :
+  IntoExcept0 P Q → IntoExcept0 (bi_persistently P) (bi_persistently Q).
 Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_persistently. Qed.
 
 (* ElimModal *)
@@ -971,7 +991,7 @@ Global Instance frame_except_0 p R P Q Q' :
   Frame p R P Q → MakeExcept0 Q Q' → Frame p R (◇ P) Q'.
 Proof.
   rewrite /Frame /MakeExcept0=><- <-.
-  by rewrite except_0_sep -(except_0_intro (⬕?p R)%I).
+  by rewrite except_0_sep -(except_0_intro (â–¡?p R)%I).
 Qed.
 
 (* IntoLater *)
@@ -1014,13 +1034,13 @@ Global Instance into_laterN_exist {A} n (Φ Ψ : A → PROP) :
 Proof. rewrite /IntoLaterN' /IntoLaterN -laterN_exist_2=> ?. by apply exist_mono. Qed.
 
 Global Instance into_later_bare n P Q :
-  IntoLaterN n P Q → IntoLaterN n (■ P) (■ Q).
+  IntoLaterN n P Q → IntoLaterN n (bi_bare P) (bi_bare Q).
 Proof. rewrite /IntoLaterN=> ->. by rewrite laterN_bare_2. Qed.
 Global Instance into_later_sink n P Q :
   IntoLaterN n P Q → IntoLaterN n (▲ P) (▲ Q).
 Proof. rewrite /IntoLaterN=> ->. by rewrite laterN_sink. Qed.
 Global Instance into_later_persistently n P Q :
-  IntoLaterN n P Q → IntoLaterN n (□ P) (□ Q).
+  IntoLaterN n P Q → IntoLaterN n (bi_persistently P) (bi_persistently Q).
 Proof. rewrite /IntoLaterN=> ->. by rewrite laterN_persistently. Qed.
 
 Global Instance into_laterN_sep_l n P1 P2 Q1 Q2 :
@@ -1093,8 +1113,11 @@ 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_bare n P Q `{AffineBI PROP} :
+  FromLaterN n P Q → FromLaterN n (bi_bare P) (bi_bare Q).
+Proof. rewrite /FromLaterN=><-. by rewrite bare_elim affine_bare. Qed.
 Global Instance from_later_persistently n P Q :
-  FromLaterN n P Q → FromLaterN n (□ P) (□ Q).
+  FromLaterN n P Q → FromLaterN n (bi_persistently P) (bi_persistently Q).
 Proof. by rewrite /FromLaterN laterN_persistently=> ->. Qed.
 Global Instance from_later_sink n P Q :
   FromLaterN n P Q → FromLaterN n (▲ P) (▲ Q).
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index ca815691fa66cf6d09e5f38b81a4d2d9a9a99eac..4090d497a38ac14b0d7481ddbdafc1c39c62c0c9 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -3,7 +3,7 @@ Set Default Proof Using "Type".
 Import bi.
 
 Class FromAssumption {PROP : bi} (p : bool) (P Q : PROP) :=
-  from_assumption : ⬕?p P ⊢ Q.
+  from_assumption : □?p P ⊢ Q.
 Arguments FromAssumption {_} _ _%I _%I : simpl never.
 Arguments from_assumption {_} _ _%I _%I {_}.
 (* No need to restrict Hint Mode, we have a default instance that will always
@@ -50,19 +50,19 @@ Arguments from_pure {_} _%I _%type_scope {_}.
 Hint Mode FromPure + ! - : typeclass_instances.
 
 Class IntoPersistent {PROP : bi} (p : bool) (P Q : PROP) :=
-  into_persistent : □?p P ⊢ □ Q.
+  into_persistent : bi_persistently_if p P ⊢ bi_persistently Q.
 Arguments IntoPersistent {_} _ _%I _%I : simpl never.
 Arguments into_persistent {_} _ _%I _%I {_}.
 Hint Mode IntoPersistent + + ! - : typeclass_instances.
 
 Class FromPersistent {PROP : bi} (a p : bool) (P Q : PROP) :=
-  from_persistent : ■?a □?p Q ⊢ P.
+  from_persistent : bi_bare_if a (bi_persistently_if p Q) ⊢ P.
 Arguments FromPersistent {_} _ _ _%I _%I : simpl never.
 Arguments from_persistent {_} _ _ _%I _%I {_}.
 Hint Mode FromPersistent + - - ! - : typeclass_instances.
 
 Class FromBare {PROP : bi} (P Q : PROP) :=
-  from_bare : ■ Q ⊢ P.
+  from_bare : bi_bare Q ⊢ P.
 Arguments FromBare {_} _%I _%type_scope : simpl never.
 Arguments from_bare {_} _%I _%type_scope {_}.
 Hint Mode FromBare + ! - : typeclass_instances.
@@ -91,7 +91,7 @@ Converting an assumption [R] into a wand [P -∗ Q] is done in three stages:
 - Instantiate the premise of the wand or implication.
 *)
 Class IntoWand {PROP : bi} (p q : bool) (R P Q : PROP) :=
-  into_wand : ⬕?p R ⊢ ⬕?q P -∗ Q.
+  into_wand : □?p R ⊢ □?q P -∗ Q.
 Arguments IntoWand {_} _ _ _%I _%I _%I : simpl never.
 Arguments into_wand {_} _ _ _%I _%I _%I {_}.
 Hint Mode IntoWand + + + ! - - : typeclass_instances.
@@ -122,7 +122,7 @@ Hint Mode FromAnd + ! - - : typeclass_instances.
 Hint Mode FromAnd + - ! ! : typeclass_instances. (* For iCombine *)
 
 Class IntoAnd {PROP : bi} (p : bool) (P Q1 Q2 : PROP) :=
-  into_and : ⬕?p P ⊢ ⬕?p (Q1 ∧ Q2).
+  into_and : □?p P ⊢ □?p (Q1 ∧ Q2).
 Arguments IntoAnd {_} _ _%I _%I _%I : simpl never.
 Arguments into_and {_} _ _%I _%I _%I {_}.
 Hint Mode IntoAnd + + ! - - : typeclass_instances.
@@ -196,13 +196,13 @@ Proof. done. Qed.
 Instance is_app_app {A} (l1 l2 : list A) : IsApp (l1 ++ l2) l1 l2.
 Proof. done. Qed.
 
-Class Frame {PROP : bi} (p : bool) (R P Q : PROP) := frame : ⬕?p R ∗ Q ⊢ P.
+Class Frame {PROP : bi} (p : bool) (R P Q : PROP) := frame : □?p R ∗ Q ⊢ P.
 Arguments Frame {_} _ _%I _%I _%I.
 Arguments frame {_ _} _%I _%I _%I {_}.
 Hint Mode Frame + + ! ! - : typeclass_instances.
 
 Class MaybeFrame {PROP : bi} (p : bool) (R P Q : PROP) :=
-  maybe_frame : ⬕?p R ∗ Q ⊢ P.
+  maybe_frame : □?p R ∗ Q ⊢ P.
 Arguments MaybeFrame {_} _ _%I _%I _%I.
 Arguments maybe_frame {_} _%I _%I _%I {_}.
 Hint Mode MaybeFrame + + ! ! - : typeclass_instances.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 2c65ec85025bdd58789324d03af887774a8b7291..0dbfee39609c40284e2bacbaeebf835437ebed00 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -22,7 +22,7 @@ Record envs_wf {PROP} (Δ : envs PROP) := {
 }.
 
 Coercion of_envs {PROP} (Δ : envs PROP) : PROP :=
-  (⌜envs_wf Δ⌝ ∧ ⬕ [∧] env_persistent Δ ∗ [∗] env_spatial Δ)%I.
+  (⌜envs_wf Δ⌝ ∧ □ [∧] env_persistent Δ ∗ [∗] env_spatial Δ)%I.
 Instance: Params (@of_envs) 1.
 Arguments of_envs : simpl never.
 
@@ -126,7 +126,7 @@ Implicit Types Δ : envs PROP.
 Implicit Types P Q : PROP.
 
 Lemma of_envs_eq Δ :
-  of_envs Δ = (⌜envs_wf Δ⌝ ∧ ⬕ [∧] env_persistent Δ ∗ [∗] env_spatial Δ)%I.
+  of_envs Δ = (⌜envs_wf Δ⌝ ∧ □ [∧] env_persistent Δ ∗ [∗] env_spatial Δ)%I.
 Proof. done. Qed.
 
 Lemma envs_lookup_delete_Some Δ Δ' i p P :
@@ -139,7 +139,7 @@ Proof.
 Qed.
 
 Lemma envs_lookup_sound Δ i p P :
-  envs_lookup i Δ = Some (p,P) → Δ ⊢ ⬕?p P ∗ envs_delete i p Δ.
+  envs_lookup i Δ = Some (p,P) → Δ ⊢ □?p P ∗ envs_delete i p Δ.
 Proof.
   rewrite /envs_lookup /envs_delete /of_envs=>?. apply pure_elim_l=> Hwf.
   destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
@@ -153,7 +153,7 @@ Proof.
     rewrite (env_lookup_perm Γs) //=. by rewrite !assoc -(comm _ P).
 Qed.
 Lemma envs_lookup_persistent_sound Δ i P :
-  envs_lookup i Δ = Some (true,P) → Δ ⊢ ⬕ P ∗ Δ.
+  envs_lookup i Δ = Some (true,P) → Δ ⊢ □ P ∗ Δ.
 Proof.
   intros. rewrite -persistently_and_bare_sep_l. apply and_intro; last done.
   rewrite envs_lookup_sound //; simpl.
@@ -161,25 +161,25 @@ Proof.
 Qed.
 
 Lemma envs_lookup_split Δ i p P :
-  envs_lookup i Δ = Some (p,P) → Δ ⊢ ⬕?p P ∗ (⬕?p P -∗ Δ).
+  envs_lookup i Δ = Some (p,P) → Δ ⊢ □?p P ∗ (□?p P -∗ Δ).
 Proof.
   rewrite /envs_lookup /of_envs=>?. apply pure_elim_l=> Hwf.
   destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
   - rewrite pure_True // left_id.
     rewrite (env_lookup_perm Γp) //= bare_persistently_and and_sep_bare_persistently.
-    cancel [⬕ P]%I. apply wand_intro_l. solve_sep_entails.
+    cancel [â–¡ P]%I. apply wand_intro_l. solve_sep_entails.
   - destruct (Γs !! i) eqn:?; simplify_eq/=.
     rewrite (env_lookup_perm Γs) //=. rewrite pure_True // left_id.
     cancel [P]. apply wand_intro_l. solve_sep_entails.
 Qed.
 
 Lemma envs_lookup_delete_sound Δ Δ' i p P :
-  envs_lookup_delete i Δ = Some (p,P,Δ') → Δ ⊢ ⬕?p P ∗ Δ'.
+  envs_lookup_delete i Δ = Some (p,P,Δ') → Δ ⊢ □?p P ∗ Δ'.
 Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound. Qed.
 
 Lemma envs_lookup_delete_list_sound Δ Δ' js rp p Ps :
   envs_lookup_delete_list js rp Δ = Some (p,Ps,Δ') →
-  Δ ⊢ ⬕?p [∗] Ps ∗ Δ'.
+  Δ ⊢ □?p [∗] Ps ∗ Δ'.
 Proof.
   revert Δ Δ' p Ps. induction js as [|j js IH]=> Δ Δ'' p Ps ?; simplify_eq/=.
   { by rewrite bare_persistently_emp left_id. }
@@ -209,7 +209,7 @@ Proof.
 Qed.
 
 Lemma envs_snoc_sound Δ p i P :
-  envs_lookup i Δ = None → Δ ⊢ ⬕?p P -∗ envs_snoc Δ p i P.
+  envs_lookup i Δ = None → Δ ⊢ □?p P -∗ envs_snoc Δ p i P.
 Proof.
   rewrite /envs_lookup /envs_snoc /of_envs=> ?; apply pure_elim_l=> Hwf.
   destruct Δ as [Γp Γs], (Γp !! i) eqn:?, (Γs !! i) eqn:?; simplify_eq/=.
@@ -225,7 +225,7 @@ Proof.
 Qed.
 
 Lemma envs_app_sound Δ Δ' p Γ :
-  envs_app p Γ Δ = Some Δ' → Δ ⊢ (if p then ⬕ [∧] Γ else [∗] Γ) -∗ Δ'.
+  envs_app p Γ Δ = Some Δ' → Δ ⊢ (if p then □ [∧] Γ else [∗] Γ) -∗ Δ'.
 Proof.
   rewrite /of_envs /envs_app=> ?; apply pure_elim_l=> Hwf.
   destruct Δ as [Γp Γs], p; simplify_eq/=.
@@ -248,12 +248,12 @@ Proof.
 Qed.
 
 Lemma envs_app_singleton_sound Δ Δ' p j Q :
-  envs_app p (Esnoc Enil j Q) Δ = Some Δ' → Δ ⊢ ⬕?p Q -∗ Δ'.
+  envs_app p (Esnoc Enil j Q) Δ = Some Δ' → Δ ⊢ □?p Q -∗ Δ'.
 Proof. move=> /envs_app_sound. destruct p; by rewrite /= right_id. Qed.
 
 Lemma envs_simple_replace_sound' Δ Δ' i p Γ :
   envs_simple_replace i p Γ Δ = Some Δ' →
-  envs_delete i p Δ ⊢ (if p then ⬕ [∧] Γ else [∗] Γ) -∗ Δ'.
+  envs_delete i p Δ ⊢ (if p then □ [∧] Γ else [∗] Γ) -∗ Δ'.
 Proof.
   rewrite /envs_simple_replace /envs_delete /of_envs=> ?.
   apply pure_elim_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=.
@@ -277,25 +277,25 @@ Qed.
 
 Lemma envs_simple_replace_singleton_sound' Δ Δ' i p j Q :
   envs_simple_replace i p (Esnoc Enil j Q) Δ = Some Δ' →
-  envs_delete i p Δ ⊢ ⬕?p Q -∗ Δ'.
+  envs_delete i p Δ ⊢ □?p Q -∗ Δ'.
 Proof. move=> /envs_simple_replace_sound'. destruct p; by rewrite /= right_id. Qed.
 
 Lemma envs_simple_replace_sound Δ Δ' i p P Γ :
   envs_lookup i Δ = Some (p,P) → envs_simple_replace i p Γ Δ = Some Δ' →
-  Δ ⊢ ⬕?p P ∗ ((if p then ⬕ [∧] Γ else [∗] Γ) -∗ Δ').
+  Δ ⊢ □?p P ∗ ((if p then □ [∧] Γ else [∗] Γ) -∗ Δ').
 Proof. intros. by rewrite envs_lookup_sound// envs_simple_replace_sound'//. Qed.
 
 Lemma envs_simple_replace_singleton_sound Δ Δ' i p P j Q :
   envs_lookup i Δ = Some (p,P) →
   envs_simple_replace i p (Esnoc Enil j Q) Δ = Some Δ' →
-  Δ ⊢ ⬕?p P ∗ (⬕?p Q -∗ Δ').
+  Δ ⊢ □?p P ∗ (□?p Q -∗ Δ').
 Proof.
   intros. by rewrite envs_lookup_sound// envs_simple_replace_singleton_sound'//.
 Qed.
 
 Lemma envs_replace_sound' Δ Δ' i p q Γ :
   envs_replace i p q Γ Δ = Some Δ' →
-  envs_delete i p Δ ⊢ (if q then ⬕ [∧] Γ else [∗] Γ) -∗ Δ'.
+  envs_delete i p Δ ⊢ (if q then □ [∧] Γ else [∗] Γ) -∗ Δ'.
 Proof.
   rewrite /envs_replace; destruct (eqb _ _) eqn:Hpq.
   - apply eqb_prop in Hpq as ->. apply envs_simple_replace_sound'.
@@ -304,18 +304,18 @@ Qed.
 
 Lemma envs_replace_singleton_sound' Δ Δ' i p q j Q :
   envs_replace i p q (Esnoc Enil j Q) Δ = Some Δ' →
-  envs_delete i p Δ ⊢ ⬕?q Q -∗ Δ'.
+  envs_delete i p Δ ⊢ □?q Q -∗ Δ'.
 Proof. move=> /envs_replace_sound'. destruct q; by rewrite /= ?right_id. Qed.
 
 Lemma envs_replace_sound Δ Δ' i p q P Γ :
   envs_lookup i Δ = Some (p,P) → envs_replace i p q Γ Δ = Some Δ' →
-  Δ ⊢ ⬕?p P ∗ ((if q then ⬕ [∧] Γ else [∗] Γ) -∗ Δ').
+  Δ ⊢ □?p P ∗ ((if q then □ [∧] Γ else [∗] Γ) -∗ Δ').
 Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.
 
 Lemma envs_replace_singleton_sound Δ Δ' i p q P j Q :
   envs_lookup i Δ = Some (p,P) →
   envs_replace i p q (Esnoc Enil j Q) Δ = Some Δ' →
-  Δ ⊢ ⬕?p P ∗ (⬕?q Q -∗ Δ').
+  Δ ⊢ □?p P ∗ (□?q Q -∗ Δ').
 Proof. intros. by rewrite envs_lookup_sound// envs_replace_singleton_sound'//. Qed.
 
 Lemma envs_lookup_envs_clear_spatial Δ j :
@@ -336,7 +336,7 @@ Proof.
 Qed.
 
 Lemma env_spatial_is_nil_bare_persistently Δ :
-  env_spatial_is_nil Δ = true → Δ ⊢ ⬕ Δ.
+  env_spatial_is_nil Δ = true → Δ ⊢ □ Δ.
 Proof.
   intros. unfold of_envs; destruct Δ as [? []]; simplify_eq/=.
   rewrite !right_id {1}bare_and_r persistently_and.
@@ -387,7 +387,8 @@ Proof.
   rewrite {2}envs_clear_spatial_sound.
   rewrite (env_spatial_is_nil_bare_persistently (envs_clear_spatial _)) //.
   rewrite -persistently_and_bare_sep_l.
-  rewrite (and_elim_l (â–¡ _)%I) persistently_and_bare_sep_r bare_persistently_elim.
+  rewrite (and_elim_l (bi_persistently _)%I)
+          persistently_and_bare_sep_r bare_persistently_elim.
   destruct (envs_split_go _ _) as [[Δ1' Δ2']|] eqn:HΔ; [|done].
   apply envs_split_go_sound in HΔ as ->; last first.
   { intros j P. by rewrite envs_lookup_envs_clear_spatial=> ->. }
@@ -546,15 +547,16 @@ Proof.
   destruct p; simpl.
   - by rewrite -(into_persistent _ P) /= wand_elim_r.
   - destruct HPQ.
-    + rewrite -(affine_bare P) (_ : P = â–¡?false P)%I // (into_persistent _ P).
-      by rewrite wand_elim_r.
-    + rewrite (_ : P = â–¡?false P)%I // (into_persistent _ P).
-      by rewrite {1}(persistent_sink_bare (â–¡ _)%I) sink_sep_l wand_elim_r HQ.
+    + rewrite -(affine_bare P) (_ : P = bi_persistently_if false P)%I //
+              (into_persistent _ P) wand_elim_r //.
+    + rewrite (_ : P = bi_persistently_if false P)%I // (into_persistent _ P).
+      by rewrite {1}(persistent_sink_bare (bi_persistently _)%I)
+                 sink_sep_l wand_elim_r HQ.
 Qed.
 
 (** * Implication and wand *)
 Lemma envs_app_singleton_sound_foo Δ Δ' p j Q :
-  envs_app p (Esnoc Enil j Q) Δ = Some Δ' → Δ ∗ ⬕?p Q ⊢ Δ'.
+  envs_app p (Esnoc Enil j Q) Δ = Some Δ' → Δ ∗ □?p Q ⊢ Δ'.
 Proof. intros. apply wand_elim_l'. eapply envs_app_singleton_sound. eauto. Qed.
 
 Lemma tac_impl_intro Δ Δ' i P P' Q :
@@ -577,7 +579,7 @@ Lemma tac_impl_intro_persistent Δ Δ' i P P' Q :
   (Δ' ⊢ Q) → Δ ⊢ P → Q.
 Proof.
   intros ?? <-. rewrite envs_app_singleton_sound //; simpl. apply impl_intro_l.
-  rewrite (_ : P = â–¡?false P)%I // (into_persistent false P).
+  rewrite (_ : P = bi_persistently_if false P)%I // (into_persistent false P).
   by rewrite persistently_and_bare_sep_l wand_elim_r.
 Qed.
 Lemma tac_pure_impl_intro Δ (φ ψ : Prop) :
@@ -604,10 +606,11 @@ Lemma tac_wand_intro_persistent Δ Δ' i P P' Q :
 Proof.
   intros ? HPQ ? HQ. rewrite envs_app_singleton_sound //; simpl.
   apply wand_intro_l. destruct HPQ.
-  - rewrite -(affine_bare P) (_ : P = â–¡?false P)%I // (into_persistent _ P).
-    by rewrite wand_elim_r.
+  - rewrite -(affine_bare P) (_ : P = bi_persistently_if false P)%I //
+            (into_persistent _ P) wand_elim_r //.
   - rewrite (_ : P = â–¡?false P)%I // (into_persistent _ P).
-    by rewrite {1}(persistent_sink_bare (â–¡ _)%I) sink_sep_l wand_elim_r HQ.
+    by rewrite {1}(persistent_sink_bare (bi_persistently _)%I) sink_sep_l
+               wand_elim_r HQ.
 Qed.
 Lemma tac_wand_intro_pure Δ P φ Q :
   IntoPure P φ →
@@ -727,15 +730,15 @@ Lemma tac_specialize_persistent_helper Δ Δ'' j q P R R' Q :
 Proof.
   intros ? HR ? Hpos ? <-. rewrite -(idemp bi_and Δ) {1}HR.
   rewrite envs_replace_singleton_sound //; destruct q; simpl.
-  - rewrite (_ : R = â–¡?false R)%I // (into_persistent _ R) sink_persistently.
-    by rewrite sep_elim_r persistently_and_bare_sep_l wand_elim_r.
-  - rewrite (absorbing_sink R) (_ : R = â–¡?false R)%I // (into_persistent _ R).
-    by rewrite sep_elim_r persistently_and_bare_sep_l wand_elim_r.
+  - by rewrite (_ : R = bi_persistently_if false R)%I // (into_persistent _ R)
+         sink_persistently sep_elim_r persistently_and_bare_sep_l wand_elim_r.
+  - by rewrite (absorbing_sink R) (_ : R = bi_persistently_if false R)%I //
+       (into_persistent _ R) sep_elim_r persistently_and_bare_sep_l wand_elim_r.
 Qed.
 
 Lemma tac_revert Δ Δ' i p P Q :
   envs_lookup_delete i Δ = Some (p,P,Δ') →
-  (Δ' ⊢ (if p then ⬕ P else P) -∗ Q) → Δ ⊢ Q.
+  (Δ' ⊢ (if p then □ P else P) -∗ Q) → Δ ⊢ Q.
 Proof.
   intros ? HQ. rewrite envs_lookup_delete_sound //; simpl.
   rewrite HQ. destruct p; simpl; auto using wand_elim_r.
@@ -755,12 +758,12 @@ Proof. rewrite /IntoIH=> HΔ ?. apply impl_intro_l, pure_elim_l. auto. Qed.
 Lemma tac_revert_ih Δ P Q {φ : Prop} (Hφ : φ) :
   IntoIH φ Δ P →
   env_spatial_is_nil Δ = true →
-  (of_envs Δ ⊢ □ P → Q) →
+  (of_envs Δ ⊢ bi_persistently P → Q) →
   (of_envs Δ ⊢ Q).
 Proof.
   rewrite /IntoIH. intros HP ? HPQ.
   rewrite (env_spatial_is_nil_bare_persistently Δ) //.
-  rewrite -(idemp bi_and (⬕ Δ)%I) {1}HP // HPQ.
+  rewrite -(idemp bi_and (□ Δ)%I) {1}HP // HPQ.
   by rewrite -{1}persistently_idemp !bare_persistently_elim impl_elim_r.
 Qed.
 
@@ -859,9 +862,9 @@ Proof.
   rewrite HP HPxy (bare_persistently_if_elim _ (_ ≡ _)%I) sep_elim_l.
   rewrite persistent_and_bare_sep_r -assoc. apply wand_elim_r'.
   rewrite -persistent_and_bare_sep_r. apply impl_elim_r'. destruct lr.
-  - apply (internal_eq_rewrite x y (λ y, ⬕?q Φ y -∗ Δ')%I). solve_proper.
+  - apply (internal_eq_rewrite x y (λ y, □?q Φ y -∗ Δ')%I). solve_proper.
   - rewrite internal_eq_sym.
-    eapply (internal_eq_rewrite y x (λ y, ⬕?q Φ y -∗ Δ')%I). solve_proper.
+    eapply (internal_eq_rewrite y x (λ y, □?q Φ y -∗ Δ')%I). solve_proper.
 Qed.
 
 (** * Conjunction splitting *)
@@ -1081,7 +1084,7 @@ Lemma tac_löb Δ Δ' i Q :
 Proof.
   intros ?? HQ. rewrite (env_spatial_is_nil_bare_persistently Δ) //.
   rewrite -(persistently_and_emp_elim Q). apply and_intro; first apply: affine.
-  rewrite -(löb (□ Q)%I) later_persistently. apply impl_intro_l.
+  rewrite -(löb (bi_persistently Q)%I) later_persistently. apply impl_intro_l.
   rewrite envs_app_singleton_sound //; simpl; rewrite HQ.
   rewrite persistently_and_bare_sep_l -{1}bare_persistently_idemp bare_persistently_sep_2.
   by rewrite wand_elim_r bare_elim.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index ad1b54ad75a6c1e552fbc9c776d1248971100593..a97e6ba1d3d41f6d3bf87720cb9611a3b41db7b1 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -1270,9 +1270,9 @@ Instance copy_destruct_impl {PROP : bi} (P Q : PROP) :
 Instance copy_destruct_wand {PROP : bi} (P Q : PROP) :
   CopyDestruct Q → CopyDestruct (P -∗ Q).
 Instance copy_destruct_bare {PROP : bi} (P : PROP) :
-  CopyDestruct P → CopyDestruct (■ P).
+  CopyDestruct P → CopyDestruct (bi_bare P).
 Instance copy_destruct_persistently {PROP : bi} (P : PROP) :
-  CopyDestruct P → CopyDestruct (□ P).
+  CopyDestruct P → CopyDestruct (bi_persistently P).
 
 Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic(tac) :=
   let hyp_name :=
@@ -1770,8 +1770,8 @@ 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 _ ⊢ bi_persistently _) => iAlways.
+Hint Extern 1 (of_envs _ ⊢ bi_bare _) => iAlways.
 Hint Extern 1 (of_envs _ ⊢ ∃ _, _) => iExists _.
 Hint Extern 1 (of_envs _ ⊢ ◇ _) => iModIntro.
 Hint Extern 1 (of_envs _ ⊢ _ ∨ _) => iLeft.
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index c704ba30c1b1ccc80654e72f00e4b13990c548e8..327767326caf59db56d50f95a5f42c12bf3fa3f0 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -6,7 +6,7 @@ Section tests.
 Context {PROP : sbi}.
 Implicit Types P Q R : PROP.
 
-Lemma demo_0 P Q : ⬕ (P ∨ Q) -∗ (∀ x, ⌜x = 0⌝ ∨ ⌜x = 1⌝) → (Q ∨ P).
+Lemma demo_0 P Q : □ (P ∨ Q) -∗ (∀ x, ⌜x = 0⌝ ∨ ⌜x = 1⌝) → (Q ∨ P).
 Proof.
   iIntros "H #H2". iDestruct "H" as "###H".
   (* should remove the disjunction "H" *)
@@ -44,7 +44,7 @@ Lemma test_unfold_constants : bar.
 Proof. iIntros (P) "HP //". Qed.
 
 Lemma test_iRewrite {A : ofeT} (x y : A) P :
-  ⬕ (∀ z, P -∗ ■ (z ≡ y)) -∗ (P -∗ P ∧ (x,x) ≡ (y,x)).
+  □ (∀ z, P -∗ bi_bare (z ≡ y)) -∗ (P -∗ P ∧ (x,x) ≡ (y,x)).
 Proof.
   iIntros "#H1 H2".
   iRewrite (bi.internal_eq_sym x x with "[# //]").
@@ -53,7 +53,7 @@ Proof.
 Qed.
 
 Lemma test_iDestruct_and_emp P Q `{!Persistent P, !Persistent Q} :
-  P ∧ emp -∗ emp ∧ Q -∗ ■ (P ∗ Q).
+  P ∧ emp -∗ emp ∧ Q -∗ bi_bare (P ∗ Q).
 Proof. iIntros "[#? _] [_ #?]". auto. Qed.
 
 Lemma test_iIntros_persistent P Q `{!Persistent Q} : (P → Q → P ∧ Q)%I.
@@ -110,17 +110,17 @@ Lemma test_iSpecialize_tc P : (∀ x y z : gset positive, P) -∗ P.
 Proof. iIntros "H". iSpecialize ("H" $! ∅ {[ 1%positive ]} ∅). done. Qed.
 
 Lemma test_iFrame_pure {A : ofeT} (φ : Prop) (y z : A) :
-  φ → ■ ⌜y ≡ z⌝ -∗ (⌜ φ ⌝ ∧ ⌜ φ ⌝ ∧ y ≡ z : PROP).
+  φ → bi_bare ⌜y ≡ z⌝ -∗ (⌜ φ ⌝ ∧ ⌜ φ ⌝ ∧ y ≡ z : PROP).
 Proof. iIntros (Hv) "#Hxy". iFrame (Hv) "Hxy". Qed.
 
 Lemma test_iAssert_modality P : ◇ False -∗ ▷ P.
 Proof.
   iIntros "HF".
-  iAssert (â–  False)%I with "[> -]" as %[].
+  iAssert (bi_bare False)%I with "[> -]" as %[].
   by iMod "HF".
 Qed.
 
-Lemma test_iMod_bare_timeless P `{!Timeless P} : ■ ▷ P -∗ ◇ ■ P.
+Lemma test_iMod_bare_timeless P `{!Timeless P} : bi_bare (▷ P) -∗ ◇ bi_bare P.
 Proof. iIntros "H". iMod "H". done. Qed.
 
 Lemma test_iAssumption_False P : False -∗ P.
@@ -166,17 +166,17 @@ Lemma test_iNext_quantifier {A} (Φ : A → A → PROP) :
 Proof. iIntros "H". iNext. done. Qed.
 
 Lemma test_iFrame_persistent (P Q : PROP) :
-  ⬕ P -∗ Q -∗ □ (P ∗ P) ∗ (P ∗ Q ∨ Q).
+  □ P -∗ Q -∗ bi_persistently (P ∗ P) ∗ (P ∗ Q ∨ Q).
 Proof. iIntros "#HP". iFrame "HP". iIntros "$". Qed.
 
-Lemma test_iSplit_persistently P Q : ⬕ P -∗ □ (P ∗ P).
+Lemma test_iSplit_persistently P Q : □ P -∗ bi_persistently (P ∗ P).
 Proof. iIntros "#?". by iSplit. Qed.
 
-Lemma test_iSpecialize_persistent P Q : ⬕ P -∗ (□ P → Q) -∗ Q.
+Lemma test_iSpecialize_persistent P Q : □ P -∗ (bi_persistently P → Q) -∗ Q.
 Proof. iIntros "#HP HPQ". by iSpecialize ("HPQ" with "HP"). Qed.
 
 Lemma test_iDestruct_persistent P (Φ : nat → PROP) `{!∀ x, Persistent (Φ x)}:
-  ⬕ (P -∗ ∃ x, Φ x) -∗
+  □ (P -∗ ∃ x, Φ x) -∗
   P -∗ ∃ x, Φ x ∗ P.
 Proof.
   iIntros "#H HP". iDestruct ("H" with "HP") as (x) "#H2". eauto with iFrame.
@@ -189,7 +189,7 @@ Proof.
 Qed.
 
 Lemma test_iInduction_wf (x : nat) P Q :
-  ⬕ P -∗ Q -∗ ⌜ (x + 0 = x)%nat ⌝.
+  □ P -∗ Q -∗ ⌜ (x + 0 = x)%nat ⌝.
 Proof.
   iIntros "#HP HQ".
   iInduction (lt_wf x) as [[|x] _] "IH"; simpl; first done.
@@ -220,22 +220,24 @@ Lemma test_iIntros_let P :
   ∀ Q, let R := emp%I in P -∗ R -∗ Q -∗ P ∗ Q.
 Proof. iIntros (Q R) "$ _ $". Qed.
 
-Lemma test_foo P Q : ■ ▷ (Q ≡ P) -∗ ■ ▷ Q -∗ ■ ▷ P.
+Lemma test_foo P Q : bi_bare (▷ (Q ≡ P)) -∗ bi_bare (▷ Q) -∗ bi_bare (▷ P).
 Proof.
   iIntros "#HPQ HQ !#". iNext. by iRewrite "HPQ" in "HQ".
 Qed.
 
 Lemma test_iIntros_modalities `(!Absorbing P) :
-  (□ ▷ ∀  x : nat, ⌜ x = 0 ⌝ → ⌜ x = 0 ⌝ -∗ False -∗ P -∗ P)%I.
+  (bi_persistently (▷ ∀  x : nat, ⌜ x = 0 ⌝ → ⌜ x = 0 ⌝ -∗ False -∗ P -∗ P))%I.
 Proof.
   iIntros (x ??).
   iIntros "* **". (* Test that fast intros do not work under modalities *)
   iIntros ([]).
 Qed.
 
-Lemma test_iNext_affine P Q : ■ ▷ (Q ≡ P) -∗ ■ ▷ Q -∗ ■ ▷ P.
+Lemma test_iNext_affine P Q :
+  bi_bare (▷ (Q ≡ P)) -∗ bi_bare (▷ Q) -∗ bi_bare (▷ P).
 Proof. iIntros "#HPQ HQ !#". iNext. by iRewrite "HPQ" in "HQ". Qed.
 
-Lemma test_iAlways P Q R : ⬕ P -∗ □ Q → R -∗ □ ■ ■ P ∗ ■ □ Q.
+Lemma test_iAlways P Q R :
+  □ P -∗ bi_persistently Q → R -∗ bi_persistently (bi_bare (bi_bare P)) ∗ □ Q.
 Proof. iIntros "#HP #HQ HR". iSplitL. iAlways. done. iAlways. done. Qed.
 End tests.