diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 8ac0024a12b46796d3aa331e795c75da8a5ccaeb..86ec1a0464158da40033db47eed1bbfe7a24e001 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 bare_persistently_ownM (a : M) : CoreId a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
+Lemma affinely_persistently_ownM (a : M) : CoreId a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
 Proof.
-  rewrite affine_bare=>?; apply (anti_symm _); [by rewrite persistently_elim|].
+  rewrite affine_affinely=>?; 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 bare_persistently_cmra_valid {A : cmraT} (a : A) : □ ✓ a ⊣⊢ ✓ a.
+Lemma affinely_persistently_cmra_valid {A : cmraT} (a : A) : □ ✓ a ⊣⊢ ✓ a.
 Proof.
-  rewrite affine_bare. intros; apply (anti_symm _); first by rewrite persistently_elim.
+  rewrite affine_affinely. intros; apply (anti_symm _); first by rewrite persistently_elim.
   apply:persistently_cmra_valid_1.
 Qed.
 
diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index e5976b34062d1a36c5440466c663427bcfdf8fa7..f2dcfddb06594baa6a1488ca5042991a8483f3b2 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -157,14 +157,14 @@ Section proofmode_classes.
     IntoWand false false R P Q →
     IntoWand p q (|={E}=> R) (|={E}=> P) (|={E}=> Q).
   Proof.
-    rewrite /IntoWand /= => HR. rewrite !bare_persistently_if_elim HR.
+    rewrite /IntoWand /= => HR. rewrite !affinely_persistently_if_elim HR.
     apply wand_intro_l. by rewrite fupd_sep wand_elim_r.
   Qed.
 
   Global Instance into_wand_fupd_persistent E1 E2 p q R P Q :
     IntoWand false q R P Q → IntoWand p q (|={E1,E2}=> R) P (|={E1,E2}=> Q).
   Proof.
-    rewrite /IntoWand /= => HR. rewrite bare_persistently_if_elim HR.
+    rewrite /IntoWand /= => HR. rewrite affinely_persistently_if_elim HR.
     apply wand_intro_l. by rewrite fupd_frame_l wand_elim_r.
   Qed.
 
@@ -172,7 +172,7 @@ Section proofmode_classes.
     IntoWand p false R P Q → IntoWand' p q R (|={E1,E2}=> P) (|={E1,E2}=> Q).
   Proof.
     rewrite /IntoWand' /IntoWand /= => ->.
-    apply wand_intro_l. by rewrite bare_persistently_if_elim fupd_wand_r.
+    apply wand_intro_l. by rewrite affinely_persistently_if_elim fupd_wand_r.
   Qed.
 
   Global Instance from_sep_fupd E P Q1 Q2 :
diff --git a/theories/base_logic/lib/viewshifts.v b/theories/base_logic/lib/viewshifts.v
index 08f270489ec355809ca72a2906b64e801619e20b..94f101889e54c2bc6f4d6f423dcdd5a0a8b126bb 100644
--- a/theories/base_logic/lib/viewshifts.v
+++ b/theories/base_logic/lib/viewshifts.v
@@ -82,7 +82,7 @@ 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. do 2 f_equiv. setoid_rewrite bi.affine_bare; last apply _.
+  rewrite bi.wand_alt. do 2 f_equiv. setoid_rewrite bi.affine_affinely; last apply _.
   by rewrite bi.persistently_impl_wand.
 Qed.
 End vs.
diff --git a/theories/base_logic/proofmode.v b/theories/base_logic/proofmode.v
index 40f79a6a760b468bc7c03b9c612711001397988a..3e0f907a3f01877663b0511198841c7f559fc173 100644
--- a/theories/base_logic/proofmode.v
+++ b/theories/base_logic/proofmode.v
@@ -31,14 +31,14 @@ Qed.
 Global Instance into_wand_bupd p q R P Q :
   IntoWand false false R P Q → IntoWand p q (|==> R) (|==> P) (|==> Q).
 Proof.
-  rewrite /IntoWand /= => HR. rewrite !bare_persistently_if_elim HR.
+  rewrite /IntoWand /= => HR. rewrite !affinely_persistently_if_elim HR.
   apply wand_intro_l. by rewrite bupd_sep wand_elim_r.
 Qed.
 
 Global Instance into_wand_bupd_persistent p q R P Q :
   IntoWand false q R P Q → IntoWand p q (|==> R) P (|==> Q).
 Proof.
-  rewrite /IntoWand /= => HR. rewrite bare_persistently_if_elim HR.
+  rewrite /IntoWand /= => HR. rewrite affinely_persistently_if_elim HR.
   apply wand_intro_l. by rewrite bupd_frame_l wand_elim_r.
 Qed.
 
@@ -46,7 +46,7 @@ Global Instance into_wand_bupd_args p q R P Q :
   IntoWand p false R P Q → IntoWand' p q R (|==> P) (|==> Q).
 Proof.
   rewrite /IntoWand' /IntoWand /= => ->.
-  apply wand_intro_l. by rewrite bare_persistently_if_elim bupd_wand_r.
+  apply wand_intro_l. by rewrite affinely_persistently_if_elim bupd_wand_r.
 Qed.
 
 (* FromOp *)
@@ -85,7 +85,7 @@ Qed.
 Global Instance into_and_ownM p (a b1 b2 : M) :
   IsOp a b1 b2 → IntoAnd p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
 Proof.
-  intros. apply bare_persistently_if_mono. by rewrite (is_op a) ownM_op sep_and.
+  intros. apply affinely_persistently_if_mono. by rewrite (is_op a) ownM_op sep_and.
 Qed.
 
 Global Instance into_sep_ownM (a b1 b2 : M) :
diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index c0c7cf886a06bbb342d8edaa033665aecf71a8fa..291994248cfd58a4d6434b9b6ffd7eacbb89418b 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -150,12 +150,12 @@ Section sep_list.
   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 affinely_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.
+      by rewrite affinely_persistently_elim wand_elim_l.
     - rewrite comm -(IH (Φ ∘ S) (Ψ ∘ S)) /=.
-      apply sep_mono_l, bare_mono, persistently_mono.
+      apply sep_mono_l, affinely_mono, persistently_mono.
       apply forall_intro=> k. by rewrite (forall_elim (S k)).
   Qed.
 
@@ -424,12 +424,12 @@ Section gmap.
   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 !big_sepM_insert // affinely_persistently_sep_dup.
     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.
+      by rewrite True_impl affinely_persistently_elim wand_elim_l.
     - rewrite comm -IH /=.
-      apply sep_mono_l, bare_mono, persistently_mono, forall_mono=> k.
+      apply sep_mono_l, affinely_mono, persistently_mono, forall_mono=> k.
       apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
       rewrite lookup_insert_ne; last by intros ?; simplify_map_eq.
       by rewrite pure_True // True_impl.
@@ -585,11 +585,11 @@ Section gset.
   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 !big_sepS_insert // affinely_persistently_sep_dup.
     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.
+      by rewrite True_impl affinely_persistently_elim wand_elim_l.
+    - rewrite comm -IH /=. apply sep_mono_l, affinely_mono, persistently_mono.
       apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
       by rewrite pure_True ?True_impl; last set_solver.
   Qed.
diff --git a/theories/bi/derived.v b/theories/bi/derived.v
index 94c19e04c528822f914869b77aeff20556a2989a..04534f3d0b5abef4c3252ec87fc84615a691875c 100644
--- a/theories/bi/derived.v
+++ b/theories/bi/derived.v
@@ -19,11 +19,11 @@ Arguments persistent {_} _%I {_}.
 Hint Mode Persistent + ! : typeclass_instances.
 Instance: Params (@Persistent) 1.
 
-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 (bi_persistently P))%I
+Definition bi_affinely {PROP : bi} (P : PROP) : PROP := (emp ∧ P)%I.
+Arguments bi_affinely {_} _%I : simpl never.
+Instance: Params (@bi_affinely) 1.
+Typeclasses Opaque bi_affinely.
+Notation "â–¡ P" := (bi_affinely (bi_persistently P))%I
   (at level 20, right associativity) : bi_scope.
 
 Class Affine {PROP : bi} (Q : PROP) := affine : Q ⊢ emp.
@@ -35,13 +35,13 @@ Class AffineBI (PROP : bi) := absorbing_bi (Q : PROP) : Affine Q.
 Existing Instance absorbing_bi | 0.
 
 Class PositiveBI (PROP : bi) :=
-  positive_bi (P Q : PROP) : bi_bare (P ∗ Q) ⊢ bi_bare P ∗ Q.
+  positive_bi (P Q : PROP) : bi_affinely (P ∗ Q) ⊢ bi_affinely P ∗ Q.
 
-Definition bi_sink {PROP : bi} (P : PROP) : PROP := (True ∗ P)%I.
-Arguments bi_sink {_} _%I : simpl never.
-Instance: Params (@bi_sink) 1.
-Typeclasses Opaque bi_sink.
-Notation "â–² P" := (bi_sink P) (at level 20, right associativity) : bi_scope.
+Definition bi_absorbingly {PROP : bi} (P : PROP) : PROP := (True ∗ P)%I.
+Arguments bi_absorbingly {_} _%I : simpl never.
+Instance: Params (@bi_absorbingly) 1.
+Typeclasses Opaque bi_absorbingly.
+Notation "â–² P" := (bi_absorbingly P) (at level 20, right associativity) : bi_scope.
 
 Class Absorbing {PROP : bi} (P : PROP) := absorbing : ▲ P ⊢ P.
 Arguments Absorbing {_} _%I : simpl never.
@@ -53,12 +53,12 @@ Arguments bi_persistently_if {_} !_ _%I /.
 Instance: Params (@bi_persistently_if) 2.
 Typeclasses Opaque bi_persistently_if.
 
-Definition bi_bare_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
-  (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 (bi_persistently_if p P))%I
+Definition bi_affinely_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
+  (if p then bi_affinely P else P)%I.
+Arguments bi_affinely_if {_} !_ _%I /.
+Instance: Params (@bi_affinely_if) 2.
+Typeclasses Opaque bi_affinely_if.
+Notation "â–¡? p P" := (bi_affinely_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.
 
@@ -674,126 +674,130 @@ Proof.
   intros. apply (anti_symm _); auto using discrete_eq_1, pure_internal_eq.
 Qed.
 
-(* Properties of the bare modality *)
-Global Instance bare_ne : NonExpansive (@bi_bare PROP).
+(* Properties of the affinely modality *)
+Global Instance affinely_ne : NonExpansive (@bi_affinely PROP).
 Proof. solve_proper. Qed.
-Global Instance bare_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@bi_bare PROP).
+Global Instance affinely_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@bi_affinely PROP).
 Proof. solve_proper. Qed.
-Global Instance bare_mono' : Proper ((⊢) ==> (⊢)) (@bi_bare PROP).
+Global Instance affinely_mono' : Proper ((⊢) ==> (⊢)) (@bi_affinely PROP).
 Proof. solve_proper. Qed.
-Global Instance bare_flip_mono' :
-  Proper (flip (⊢) ==> flip (⊢)) (@bi_bare PROP).
+Global Instance affinely_flip_mono' :
+  Proper (flip (⊢) ==> flip (⊢)) (@bi_affinely PROP).
 Proof. solve_proper. Qed.
 
-Lemma bare_elim_emp P : bi_bare P ⊢ emp.
-Proof. rewrite /bi_bare; auto. Qed.
-Lemma bare_elim P : bi_bare P ⊢ P.
-Proof. rewrite /bi_bare; auto. Qed.
-Lemma bare_mono P Q : (P ⊢ Q) → bi_bare P ⊢ bi_bare Q.
+Lemma affinely_elim_emp P : bi_affinely P ⊢ emp.
+Proof. rewrite /bi_affinely; auto. Qed.
+Lemma affinely_elim P : bi_affinely P ⊢ P.
+Proof. rewrite /bi_affinely; auto. Qed.
+Lemma affinely_mono P Q : (P ⊢ Q) → bi_affinely P ⊢ bi_affinely Q.
 Proof. by intros ->. Qed.
-Lemma bare_idemp P : bi_bare (bi_bare P) ⊣⊢ bi_bare P.
-Proof. by rewrite /bi_bare assoc idemp. Qed.
+Lemma affinely_idemp P : bi_affinely (bi_affinely P) ⊣⊢ bi_affinely P.
+Proof. by rewrite /bi_affinely assoc idemp. Qed.
 
-Lemma bare_intro' P Q : (bi_bare P ⊢ Q) → bi_bare P ⊢ bi_bare Q.
-Proof. intros <-. by rewrite bare_idemp. Qed.
+Lemma affinely_intro' P Q : (bi_affinely P ⊢ Q) → bi_affinely P ⊢ bi_affinely Q.
+Proof. intros <-. by rewrite affinely_idemp. Qed.
 
-Lemma bare_False : bi_bare False ⊣⊢ False.
-Proof. by rewrite /bi_bare right_absorb. Qed.
-Lemma bare_emp : bi_bare emp ⊣⊢ emp.
-Proof. by rewrite /bi_bare (idemp bi_and). Qed.
-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 : bi_bare (P ∧ Q) ⊣⊢ bi_bare P ∧ bi_bare Q.
+Lemma affinely_False : bi_affinely False ⊣⊢ False.
+Proof. by rewrite /bi_affinely right_absorb. Qed.
+Lemma affinely_emp : bi_affinely emp ⊣⊢ emp.
+Proof. by rewrite /bi_affinely (idemp bi_and). Qed.
+Lemma affinely_or P Q : bi_affinely (P ∨ Q) ⊣⊢ bi_affinely P ∨ bi_affinely Q.
+Proof. by rewrite /bi_affinely and_or_l. Qed.
+Lemma affinely_and P Q : bi_affinely (P ∧ Q) ⊣⊢ bi_affinely P ∧ bi_affinely Q.
 Proof.
-  rewrite /bi_bare -(comm _ P) (assoc _ (_ ∧ _)%I) -!(assoc _ P).
+  rewrite /bi_affinely -(comm _ P) (assoc _ (_ ∧ _)%I) -!(assoc _ P).
   by rewrite idemp !assoc (comm _ P).
 Qed.
-Lemma bare_sep_2 P Q : bi_bare P ∗ bi_bare Q ⊢ bi_bare (P ∗ Q).
+Lemma affinely_sep_2 P Q : bi_affinely P ∗ bi_affinely Q ⊢ bi_affinely (P ∗ Q).
 Proof.
-  rewrite /bi_bare. apply and_intro.
+  rewrite /bi_affinely. apply and_intro.
   - by rewrite !and_elim_l right_id.
   - by rewrite !and_elim_r.
 Qed.
-Lemma bare_sep `{PositiveBI PROP} P Q : bi_bare (P ∗ Q) ⊣⊢ bi_bare P ∗ bi_bare Q.
+Lemma affinely_sep `{PositiveBI PROP} P Q :
+  bi_affinely (P ∗ Q) ⊣⊢ bi_affinely P ∗ bi_affinely Q.
 Proof.
-  apply (anti_symm _), bare_sep_2.
-  by rewrite -{1}bare_idemp positive_bi !(comm _ (bi_bare P)%I) positive_bi.
+  apply (anti_symm _), affinely_sep_2.
+  by rewrite -{1}affinely_idemp positive_bi !(comm _ (bi_affinely P)%I) positive_bi.
 Qed.
-Lemma bare_forall {A} (Φ : A → PROP) : bi_bare (∀ a, Φ a) ⊢ ∀ a, bi_bare (Φ a).
+Lemma affinely_forall {A} (Φ : A → PROP) :
+  bi_affinely (∀ a, Φ a) ⊢ ∀ a, bi_affinely (Φ a).
 Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed.
-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 : bi_bare True ⊣⊢ bi_bare emp.
-Proof. apply (anti_symm _); rewrite /bi_bare; auto. Qed.
-
-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 ∧ bi_bare Q ⊣⊢ bi_bare (P ∧ Q).
-Proof. by rewrite /bi_bare !assoc (comm _ P). Qed.
-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 *)
-Global Instance sink_ne : NonExpansive (@bi_sink PROP).
+Lemma affinely_exist {A} (Φ : A → PROP) :
+  bi_affinely (∃ a, Φ a) ⊣⊢ ∃ a, bi_affinely (Φ a).
+Proof. by rewrite /bi_affinely and_exist_l. Qed.
+
+Lemma affinely_True_emp : bi_affinely True ⊣⊢ bi_affinely emp.
+Proof. apply (anti_symm _); rewrite /bi_affinely; auto. Qed.
+
+Lemma affinely_and_l P Q : bi_affinely P ∧ Q ⊣⊢ bi_affinely (P ∧ Q).
+Proof. by rewrite /bi_affinely assoc. Qed.
+Lemma affinely_and_r P Q : P ∧ bi_affinely Q ⊣⊢ bi_affinely (P ∧ Q).
+Proof. by rewrite /bi_affinely !assoc (comm _ P). Qed.
+Lemma affinely_and_lr P Q : bi_affinely P ∧ Q ⊣⊢ P ∧ bi_affinely Q.
+Proof. by rewrite affinely_and_l affinely_and_r. Qed.
+
+(* Properties of the absorbingly modality *)
+Global Instance absorbingly_ne : NonExpansive (@bi_absorbingly PROP).
 Proof. solve_proper. Qed.
-Global Instance sink_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@bi_sink PROP).
+Global Instance absorbingly_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@bi_absorbingly PROP).
 Proof. solve_proper. Qed.
-Global Instance sink_mono' : Proper ((⊢) ==> (⊢)) (@bi_sink PROP).
+Global Instance absorbingly_mono' : Proper ((⊢) ==> (⊢)) (@bi_absorbingly PROP).
 Proof. solve_proper. Qed.
-Global Instance sink_flip_mono' :
-  Proper (flip (⊢) ==> flip (⊢)) (@bi_sink PROP).
+Global Instance absorbingly_flip_mono' :
+  Proper (flip (⊢) ==> flip (⊢)) (@bi_absorbingly PROP).
 Proof. solve_proper. Qed.
 
-Lemma sink_intro P : P ⊢ ▲ P.
-Proof. by rewrite /bi_sink -True_sep_2. Qed.
-Lemma sink_mono P Q : (P ⊢ Q) → ▲ P ⊢ ▲ Q.
+Lemma absorbingly_intro P : P ⊢ ▲ P.
+Proof. by rewrite /bi_absorbingly -True_sep_2. Qed.
+Lemma absorbingly_mono P Q : (P ⊢ Q) → ▲ P ⊢ ▲ Q.
 Proof. by intros ->. Qed.
-Lemma sink_idemp P : ▲ ▲ P ⊣⊢ ▲ P.
+Lemma absorbingly_idemp P : ▲ ▲ P ⊣⊢ ▲ P.
 Proof.
-  apply (anti_symm _), sink_intro.
-  rewrite /bi_sink assoc. apply sep_mono; auto.
+  apply (anti_symm _), absorbingly_intro.
+  rewrite /bi_absorbingly assoc. apply sep_mono; auto.
 Qed.
 
-Lemma sink_pure φ : ▲ ⌜ φ ⌝ ⊣⊢ ⌜ φ ⌝.
+Lemma absorbingly_pure φ : ▲ ⌜ φ ⌝ ⊣⊢ ⌜ φ ⌝.
 Proof.
-  apply (anti_symm _), sink_intro.
+  apply (anti_symm _), absorbingly_intro.
   apply wand_elim_r', pure_elim'=> ?. apply wand_intro_l; auto.
 Qed.
-Lemma sink_or P Q : ▲ (P ∨ Q) ⊣⊢ ▲ P ∨ ▲ Q.
-Proof. by rewrite /bi_sink sep_or_l. Qed.
-Lemma sink_and P Q : ▲ (P ∧ Q) ⊢ ▲ P ∧ ▲ Q.
-Proof. apply and_intro; apply sink_mono; auto. Qed.
-Lemma sink_forall {A} (Φ : A → PROP) : ▲ (∀ a, Φ a) ⊢ ∀ a, ▲ Φ a.
+Lemma absorbingly_or P Q : ▲ (P ∨ Q) ⊣⊢ ▲ P ∨ ▲ Q.
+Proof. by rewrite /bi_absorbingly sep_or_l. Qed.
+Lemma absorbingly_and P Q : ▲ (P ∧ Q) ⊢ ▲ P ∧ ▲ Q.
+Proof. apply and_intro; apply absorbingly_mono; auto. Qed.
+Lemma absorbingly_forall {A} (Φ : A → PROP) : ▲ (∀ a, Φ a) ⊢ ∀ a, ▲ Φ a.
 Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed.
-Lemma sink_exist {A} (Φ : A → PROP) : ▲ (∃ a, Φ a) ⊣⊢ ∃ a, ▲ Φ a.
-Proof. by rewrite /bi_sink sep_exist_l. Qed.
+Lemma absorbingly_exist {A} (Φ : A → PROP) : ▲ (∃ a, Φ a) ⊣⊢ ∃ a, ▲ Φ a.
+Proof. by rewrite /bi_absorbingly sep_exist_l. Qed.
 
-Lemma sink_internal_eq {A : ofeT} (x y : A) : ▲ (x ≡ y) ⊣⊢ x ≡ y.
+Lemma absorbingly_internal_eq {A : ofeT} (x y : A) : ▲ (x ≡ y) ⊣⊢ x ≡ y.
 Proof.
-  apply (anti_symm _), sink_intro.
+  apply (anti_symm _), absorbingly_intro.
   apply wand_elim_r', (internal_eq_rewrite' x y (λ y, True -∗ x ≡ y)%I); auto.
   apply wand_intro_l, internal_eq_refl.
 Qed.
 
-Lemma sink_sep P Q : ▲ (P ∗ Q) ⊣⊢ ▲ P ∗ ▲ Q.
-Proof. by rewrite -{1}sink_idemp /bi_sink !assoc -!(comm _ P) !assoc. Qed.
-Lemma sink_True_emp : ▲ True ⊣⊢ ▲ emp.
-Proof. by rewrite sink_pure /bi_sink right_id. Qed.
-Lemma sink_wand P Q : ▲ (P -∗ Q) ⊢ ▲ P -∗ ▲ Q.
-Proof. apply wand_intro_l. by rewrite -sink_sep wand_elim_r. Qed.
+Lemma absorbingly_sep P Q : ▲ (P ∗ Q) ⊣⊢ ▲ P ∗ ▲ Q.
+Proof. by rewrite -{1}absorbingly_idemp /bi_absorbingly !assoc -!(comm _ P) !assoc. Qed.
+Lemma absorbingly_True_emp : ▲ True ⊣⊢ ▲ emp.
+Proof. by rewrite absorbingly_pure /bi_absorbingly right_id. Qed.
+Lemma absorbingly_wand P Q : ▲ (P -∗ Q) ⊢ ▲ P -∗ ▲ Q.
+Proof. apply wand_intro_l. by rewrite -absorbingly_sep wand_elim_r. Qed.
 
-Lemma sink_sep_l P Q : ▲ P ∗ Q ⊣⊢ ▲ (P ∗ Q).
-Proof. by rewrite /bi_sink assoc. Qed.
-Lemma sink_sep_r P Q : P ∗ ▲ Q ⊣⊢ ▲ (P ∗ Q).
-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 absorbingly_sep_l P Q : ▲ P ∗ Q ⊣⊢ ▲ (P ∗ Q).
+Proof. by rewrite /bi_absorbingly assoc. Qed.
+Lemma absorbingly_sep_r P Q : P ∗ ▲ Q ⊣⊢ ▲ (P ∗ Q).
+Proof. by rewrite /bi_absorbingly !assoc (comm _ P). Qed.
+Lemma absorbingly_sep_lr P Q : ▲ P ∗ Q ⊣⊢ P ∗ ▲ Q.
+Proof. by rewrite absorbingly_sep_l absorbingly_sep_r. Qed.
 
-Lemma bare_sink `{!PositiveBI PROP} P : bi_bare (▲ P) ⊣⊢ bi_bare P.
+Lemma affinely_absorbingly `{!PositiveBI PROP} P :
+  bi_affinely (▲ P) ⊣⊢ bi_affinely P.
 Proof.
-  apply (anti_symm _), bare_mono, sink_intro.
-  by rewrite /bi_sink bare_sep bare_True_emp bare_emp left_id.
+  apply (anti_symm _), affinely_mono, absorbingly_intro.
+  by rewrite /bi_absorbingly affinely_sep affinely_True_emp affinely_emp left_id.
 Qed.
 
 (* Affine propositions *)
@@ -817,53 +821,53 @@ 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 (bi_bare P).
-Proof. rewrite /bi_bare. apply _. Qed.
+Global Instance affinely_affine P : Affine (bi_affinely P).
+Proof. rewrite /bi_affinely. apply _. Qed.
 
 (* Absorbing propositions *)
 Global Instance Absorbing_proper : Proper ((⊣⊢) ==> iff) (@Absorbing PROP).
 Proof. solve_proper. Qed.
 
 Global Instance pure_absorbing φ : Absorbing (⌜φ⌝%I : PROP).
-Proof. by rewrite /Absorbing sink_pure. Qed.
+Proof. by rewrite /Absorbing absorbingly_pure. Qed.
 Global Instance and_absorbing P Q : Absorbing P → Absorbing Q → Absorbing (P ∧ Q).
-Proof. intros. by rewrite /Absorbing sink_and !absorbing. Qed.
+Proof. intros. by rewrite /Absorbing absorbingly_and !absorbing. Qed.
 Global Instance or_absorbing P Q : Absorbing P → Absorbing Q → Absorbing (P ∨ Q).
-Proof. intros. by rewrite /Absorbing sink_or !absorbing. Qed.
+Proof. intros. by rewrite /Absorbing absorbingly_or !absorbing. Qed.
 Global Instance forall_absorbing {A} (Φ : A → PROP) :
   (∀ x, Absorbing (Φ x)) → Absorbing (∀ x, Φ x).
-Proof. rewrite /Absorbing=> ?. rewrite sink_forall. auto using forall_mono. Qed.
+Proof. rewrite /Absorbing=> ?. rewrite absorbingly_forall. auto using forall_mono. Qed.
 Global Instance exist_absorbing {A} (Φ : A → PROP) :
   (∀ x, Absorbing (Φ x)) → Absorbing (∃ x, Φ x).
-Proof. rewrite /Absorbing=> ?. rewrite sink_exist. auto using exist_mono. Qed.
+Proof. rewrite /Absorbing=> ?. rewrite absorbingly_exist. auto using exist_mono. Qed.
 
 Global Instance internal_eq_absorbing {A : ofeT} (x y : A) :
   Absorbing (x ≡ y : PROP)%I.
-Proof. by rewrite /Absorbing sink_internal_eq. Qed.
+Proof. by rewrite /Absorbing absorbingly_internal_eq. Qed.
 
 Global Instance sep_absorbing_l P Q : Absorbing P → Absorbing (P ∗ Q).
-Proof. intros. by rewrite /Absorbing -sink_sep_l absorbing. Qed.
+Proof. intros. by rewrite /Absorbing -absorbingly_sep_l absorbing. Qed.
 Global Instance sep_absorbing_r P Q : Absorbing Q → Absorbing (P ∗ Q).
-Proof. intros. by rewrite /Absorbing -sink_sep_r absorbing. Qed.
+Proof. intros. by rewrite /Absorbing -absorbingly_sep_r absorbing. Qed.
 
 Global Instance wand_absorbing P Q : Absorbing Q → Absorbing (P -∗ Q).
-Proof. intros. by rewrite /Absorbing sink_wand !absorbing -sink_intro. Qed.
+Proof. intros. by rewrite /Absorbing absorbingly_wand !absorbing -absorbingly_intro. Qed.
 
-Global Instance sink_absorbing P : Absorbing (â–² P).
-Proof. rewrite /bi_sink. apply _. Qed.
+Global Instance absorbingly_absorbing P : Absorbing (â–² P).
+Proof. rewrite /bi_absorbingly. apply _. Qed.
 
 (* Properties of affine and absorbing propositions *)
-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.
+Lemma affine_affinely P `{!Affine P} : bi_affinely P ⊣⊢ P.
+Proof. rewrite /bi_affinely. apply (anti_symm _); auto. Qed.
+Lemma absorbing_absorbingly P `{!Absorbing P} : ▲ P ⊣⊢ P.
+Proof. by apply (anti_symm _), absorbingly_intro. Qed.
 
 Lemma True_affine_all_affine P : Affine (True%I : PROP) → Affine P.
 Proof. rewrite /Affine=> <-; auto. Qed.
 Lemma emp_absorbing_all_absorbing P : Absorbing (emp%I : PROP) → Absorbing P.
 Proof.
   intros. rewrite /Absorbing -{2}(left_id emp%I _ P).
-  by rewrite -(absorbing emp) sink_sep_l left_id.
+  by rewrite -(absorbing emp) absorbingly_sep_l left_id.
 Qed.
 
 Lemma sep_elim_l P Q `{H : TCOr (Affine Q) (Absorbing P)} : P ∗ Q ⊢ P.
@@ -884,8 +888,8 @@ Proof.
 Qed.
 
 
-Lemma bare_intro P Q `{!Affine P} : (P ⊢ Q) → P ⊢ bi_bare Q.
-Proof. intros <-. by rewrite affine_bare. Qed.
+Lemma affinely_intro P Q `{!Affine P} : (P ⊢ Q) → P ⊢ bi_affinely Q.
+Proof. intros <-. by rewrite affine_affinely. Qed.
 
 Lemma emp_and P `{!Affine P} : emp ∧ P ⊣⊢ P.
 Proof. apply (anti_symm _); auto. Qed.
@@ -905,9 +909,9 @@ Section affine_bi.
   Context `{AffineBI PROP}.
 
   Global Instance affine_bi_absorbing P : Absorbing P | 0.
-  Proof. by rewrite /Absorbing /bi_sink (affine True%I) left_id. Qed.
+  Proof. by rewrite /Absorbing /bi_absorbingly (affine True%I) left_id. Qed.
   Global Instance affine_bi_positive : PositiveBI PROP.
-  Proof. intros P Q. by rewrite !affine_bare. Qed.
+  Proof. intros P Q. by rewrite !affine_affinely. Qed.
 
   Lemma True_emp : True ⊣⊢ emp.
   Proof. apply (anti_symm _); auto using affine. Qed.
@@ -942,12 +946,13 @@ Global Instance persistently_flip_mono' :
   Proper (flip (⊢) ==> flip (⊢)) (@bi_persistently PROP).
 Proof. intros P Q; apply persistently_mono. Qed.
 
-Lemma sink_persistently P : ▲ bi_persistently P ⊣⊢ bi_persistently P.
+Lemma absorbingly_persistently P : ▲ bi_persistently P ⊣⊢ bi_persistently P.
 Proof.
-  apply (anti_symm _), sink_intro. by rewrite /bi_sink comm persistently_absorbing.
+  apply (anti_symm _), absorbingly_intro.
+  by rewrite /bi_absorbingly comm persistently_absorbing.
 Qed.
 Global Instance persistently_absorbing P : Absorbing (bi_persistently P).
-Proof. by rewrite /Absorbing sink_persistently. Qed.
+Proof. by rewrite /Absorbing absorbingly_persistently. Qed.
 
 Lemma persistently_and_sep_assoc P Q R :
   bi_persistently P ∧ (Q ∗ R) ⊣⊢ (bi_persistently P ∧ Q) ∗ R.
@@ -963,17 +968,17 @@ Proof.
 Qed.
 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 : bi_persistently P ⊢ ▲ P.
+Lemma persistently_elim_absorbingly P : bi_persistently P ⊢ ▲ P.
 Proof.
   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} : bi_persistently P ⊢ P.
-Proof. by rewrite persistently_elim_sink absorbing_sink. Qed.
+Proof. by rewrite persistently_elim_absorbingly absorbing_absorbingly. Qed.
 
 Lemma persistently_idemp_1 P :
   bi_persistently (bi_persistently P) ⊢ bi_persistently P.
-Proof. by rewrite persistently_elim_sink sink_persistently. Qed.
+Proof. by rewrite persistently_elim_absorbingly absorbingly_persistently. Qed.
 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.
@@ -1047,9 +1052,9 @@ Proof.
   by rewrite persistently_and_sep_assoc (comm bi_and) persistently_and_emp_elim.
 Qed.
 
-Lemma persistently_bare P : bi_persistently (bi_bare P) ⊣⊢ bi_persistently P.
+Lemma persistently_affinely P : bi_persistently (bi_affinely P) ⊣⊢ bi_persistently P.
 Proof.
-  by rewrite /bi_bare persistently_and -persistently_True_emp
+  by rewrite /bi_affinely persistently_and -persistently_True_emp
              persistently_pure left_id.
 Qed.
 
@@ -1067,7 +1072,7 @@ 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
+  by rewrite -persistently_affinely affinely_sep sep_and !affinely_elim persistently_and
              and_sep_persistently.
 Qed.
 
@@ -1090,7 +1095,7 @@ Proof.
   by rewrite (comm bi_and) persistently_and_emp_elim wand_elim_l.
 Qed.
 
-Section persistently_bare_bi.
+Section persistently_affinely_bi.
   Context `{AffineBI PROP}.
 
   Lemma persistently_emp : bi_persistently emp ⊣⊢ emp.
@@ -1134,86 +1139,96 @@ Section persistently_bare_bi.
     - 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.
+End persistently_affinely_bi.
 
 
-(* The combined bare persistently modality *)
-Lemma bare_persistently_elim P : □ P ⊢ P.
+(* The combined affinely persistently modality *)
+Lemma affinely_persistently_elim P : □ P ⊢ P.
 Proof. apply persistently_and_emp_elim. Qed.
-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.
-Proof. by rewrite -persistently_True_emp persistently_pure bare_True_emp bare_emp. Qed.
-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.
-Proof. by rewrite persistently_or bare_or. Qed.
-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).
-Proof. by rewrite bare_sep_2 persistently_sep_2. Qed.
-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.
-Proof. by rewrite persistently_bare persistently_idemp. Qed.
-
-Lemma persistently_and_bare_sep_l P Q : bi_persistently P ∧ Q ⊣⊢ □ P ∗ Q.
+Lemma affinely_persistently_intro' P Q : (□ P ⊢ Q) → □ P ⊢ □ Q.
+Proof. intros <-. by rewrite persistently_affinely persistently_idemp. Qed.
+
+Lemma affinely_persistently_emp : □ emp ⊣⊢ emp.
+Proof.
+  by rewrite -persistently_True_emp persistently_pure affinely_True_emp
+             affinely_emp.
+Qed.
+Lemma affinely_persistently_and P Q : □ (P ∧ Q) ⊣⊢ □ P ∧ □ Q.
+Proof. by rewrite persistently_and affinely_and. Qed.
+Lemma affinely_persistently_or P Q : □ (P ∨ Q) ⊣⊢ □ P ∨ □ Q.
+Proof. by rewrite persistently_or affinely_or. Qed.
+Lemma affinely_persistently_exist {A} (Φ : A → PROP) : □ (∃ x, Φ x) ⊣⊢ ∃ x, □ Φ x.
+Proof. by rewrite persistently_exist affinely_exist. Qed.
+Lemma affinely_persistently_sep_2 P Q : □ P ∗ □ Q ⊢ □ (P ∗ Q).
+Proof. by rewrite affinely_sep_2 persistently_sep_2. Qed.
+Lemma affinely_persistently_sep `{PositiveBI PROP} P Q : □ (P ∗ Q) ⊣⊢ □ P ∗ □ Q.
+Proof. by rewrite -affinely_sep -persistently_sep. Qed.
+
+Lemma affinely_persistently_idemp P : □ □ P ⊣⊢ □ P.
+Proof. by rewrite persistently_affinely persistently_idemp. Qed.
+
+Lemma persistently_and_affinely_sep_l P Q : bi_persistently P ∧ Q ⊣⊢ □ P ∗ Q.
 Proof.
   apply (anti_symm _).
-  - by rewrite /bi_bare -(comm bi_and (bi_persistently P)%I)
+  - by rewrite /bi_affinely -(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.
+  - apply and_intro. by rewrite affinely_elim sep_elim_l. by rewrite sep_elim_r.
+Qed.
+Lemma persistently_and_affinely_sep_r P Q : P ∧ bi_persistently Q ⊣⊢ P ∗ □ Q.
+Proof. by rewrite !(comm _ P) persistently_and_affinely_sep_l. Qed.
+Lemma and_sep_affinely_persistently P Q : □ P ∧ □ Q ⊣⊢ □ P ∗ □ Q.
+Proof.
+  by rewrite -persistently_and_affinely_sep_l -affinely_and affinely_and_r.
 Qed.
-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.
-Proof. by rewrite -persistently_and_bare_sep_l -bare_and bare_and_r. Qed.
 
-Lemma bare_persistently_sep_dup P : □ P ⊣⊢ □ P ∗ □ P.
-Proof. by rewrite -persistently_and_bare_sep_l bare_and_r bare_and idemp. Qed.
+Lemma affinely_persistently_sep_dup P : □ P ⊣⊢ □ P ∗ □ P.
+Proof.
+  by rewrite -persistently_and_affinely_sep_l affinely_and_r affinely_and idemp.
+Qed.
 
-(* Conditional bare modality *)
-Global Instance bare_if_ne p : NonExpansive (@bi_bare_if PROP p).
+(* Conditional affinely modality *)
+Global Instance affinely_if_ne p : NonExpansive (@bi_affinely_if PROP p).
 Proof. solve_proper. Qed.
-Global Instance bare_if_proper p : Proper ((⊣⊢) ==> (⊣⊢)) (@bi_bare_if PROP p).
+Global Instance affinely_if_proper p : Proper ((⊣⊢) ==> (⊣⊢)) (@bi_affinely_if PROP p).
 Proof. solve_proper. Qed.
-Global Instance bare_if_mono' p : Proper ((⊢) ==> (⊢)) (@bi_bare_if PROP p).
+Global Instance affinely_if_mono' p : Proper ((⊢) ==> (⊢)) (@bi_affinely_if PROP p).
 Proof. solve_proper. Qed.
-Global Instance bare_if_flip_mono' p :
-  Proper (flip (⊢) ==> flip (⊢)) (@bi_bare_if PROP p).
+Global Instance affinely_if_flip_mono' p :
+  Proper (flip (⊢) ==> flip (⊢)) (@bi_affinely_if PROP p).
 Proof. solve_proper. Qed.
 
-Lemma bare_if_mono p P Q : (P ⊢ Q) → bi_bare_if p P ⊢ bi_bare_if p Q.
+Lemma affinely_if_mono p P Q : (P ⊢ Q) → bi_affinely_if p P ⊢ bi_affinely_if p Q.
 Proof. by intros ->. Qed.
 
-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 : bi_bare P ⊢ bi_bare_if p P.
-Proof. destruct p; simpl; auto using bare_elim. Qed.
-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 : bi_bare_if p emp ⊣⊢ emp.
-Proof. destruct p; simpl; auto using bare_emp. Qed.
-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 : 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) :
-  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 :
-  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 :
-  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 : bi_bare_if p (bi_bare_if p P) ⊣⊢ bi_bare_if p P.
-Proof. destruct p; simpl; auto using bare_idemp. Qed.
+Lemma affinely_if_elim p P : bi_affinely_if p P ⊢ P.
+Proof. destruct p; simpl; auto using affinely_elim. Qed.
+Lemma affinely_affinely_if p P : bi_affinely P ⊢ bi_affinely_if p P.
+Proof. destruct p; simpl; auto using affinely_elim. Qed.
+Lemma affinely_if_intro' p P Q :
+  (bi_affinely_if p P ⊢ Q) → bi_affinely_if p P ⊢ bi_affinely_if p Q.
+Proof. destruct p; simpl; auto using affinely_intro'. Qed.
+
+Lemma affinely_if_emp p : bi_affinely_if p emp ⊣⊢ emp.
+Proof. destruct p; simpl; auto using affinely_emp. Qed.
+Lemma affinely_if_and p P Q :
+  bi_affinely_if p (P ∧ Q) ⊣⊢ bi_affinely_if p P ∧ bi_affinely_if p Q.
+Proof. destruct p; simpl; auto using affinely_and. Qed.
+Lemma affinely_if_or p P Q :
+  bi_affinely_if p (P ∨ Q) ⊣⊢ bi_affinely_if p P ∨ bi_affinely_if p Q.
+Proof. destruct p; simpl; auto using affinely_or. Qed.
+Lemma affinely_if_exist {A} p (Ψ : A → PROP) :
+  bi_affinely_if p (∃ a, Ψ a) ⊣⊢ ∃ a, bi_affinely_if p (Ψ a).
+Proof. destruct p; simpl; auto using affinely_exist. Qed.
+Lemma affinely_if_sep_2 p P Q :
+  bi_affinely_if p P ∗ bi_affinely_if p Q ⊢ bi_affinely_if p (P ∗ Q).
+Proof. destruct p; simpl; auto using affinely_sep_2. Qed.
+Lemma affinely_if_sep `{PositiveBI PROP} p P Q :
+  bi_affinely_if p (P ∗ Q) ⊣⊢ bi_affinely_if p P ∗ bi_affinely_if p Q.
+Proof. destruct p; simpl; auto using affinely_sep. Qed.
+
+Lemma affinely_if_idemp p P :
+  bi_affinely_if p (bi_affinely_if p P) ⊣⊢ bi_affinely_if p P.
+Proof. destruct p; simpl; auto using affinely_idemp. Qed.
 
 (* Conditional persistently *)
 Global Instance persistently_if_ne p : NonExpansive (@bi_persistently_if PROP p).
@@ -1254,34 +1269,34 @@ 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.
+(* Conditional affinely persistently *)
+Lemma affinely_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.
-Proof. destruct p; simpl; auto using bare_persistently_elim. Qed.
-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.
-Proof. destruct p; simpl; auto using bare_persistently_intro'. Qed.
-
-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.
-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.
-Proof. destruct p; simpl; auto using bare_persistently_or. Qed.
-Lemma bare_persistently_if_exist {A} p (Ψ : A → PROP) :
+Lemma affinely_persistently_if_elim p P : □?p P ⊢ P.
+Proof. destruct p; simpl; auto using affinely_persistently_elim. Qed.
+Lemma affinely_persistently_affinely_persistently_if p P : □ P ⊢ □?p P.
+Proof. destruct p; simpl; auto using affinely_persistently_elim. Qed.
+Lemma affinely_persistently_if_intro' p P Q : (□?p P ⊢ Q) → □?p P ⊢ □?p Q.
+Proof. destruct p; simpl; auto using affinely_persistently_intro'. Qed.
+
+Lemma affinely_persistently_if_emp p : □?p emp ⊣⊢ emp.
+Proof. destruct p; simpl; auto using affinely_persistently_emp. Qed.
+Lemma affinely_persistently_if_and p P Q : □?p (P ∧ Q) ⊣⊢ □?p P ∧ □?p Q.
+Proof. destruct p; simpl; auto using affinely_persistently_and. Qed.
+Lemma affinely_persistently_if_or p P Q : □?p (P ∨ Q) ⊣⊢ □?p P ∨ □?p Q.
+Proof. destruct p; simpl; auto using affinely_persistently_or. Qed.
+Lemma affinely_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).
-Proof. destruct p; simpl; auto using bare_persistently_sep_2. Qed.
-Lemma bare_persistently_if_sep `{PositiveBI PROP} p P Q :
+Proof. destruct p; simpl; auto using affinely_persistently_exist. Qed.
+Lemma affinely_persistently_if_sep_2 p P Q : □?p P ∗ □?p Q ⊢ □?p (P ∗ Q).
+Proof. destruct p; simpl; auto using affinely_persistently_sep_2. Qed.
+Lemma affinely_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.
+Proof. destruct p; simpl; auto using affinely_persistently_sep. Qed.
 
-Lemma bare_persistently_if_idemp p P : □?p □?p P ⊣⊢ □?p P.
-Proof. destruct p; simpl; auto using bare_persistently_idemp. Qed.
+Lemma affinely_persistently_if_idemp p P : □?p □?p P ⊣⊢ □?p P.
+Proof. destruct p; simpl; auto using affinely_persistently_idemp. Qed.
 
 (* Persistence *)
 Global Instance Persistent_proper : Proper ((≡) ==> iff) (@Persistent PROP).
@@ -1326,10 +1341,10 @@ Proof. intros. by rewrite /Persistent -persistently_sep_2 -!persistent. Qed.
 
 Global Instance persistently_persistent P : Persistent (bi_persistently P).
 Proof. by rewrite /Persistent persistently_idemp. Qed.
-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.
+Global Instance affinely_persistent P : Persistent P → Persistent (bi_affinely P).
+Proof. rewrite /bi_affinely. apply _. Qed.
+Global Instance absorbingly_persistent P : Persistent P → Persistent (▲ P).
+Proof. rewrite /bi_absorbingly. apply _. Qed.
 
 Global Instance from_option_persistent {A} P (Ψ : A → PROP) (mx : option A) :
   (∀ x, Persistent (Ψ x)) → Persistent P → Persistent (from_option Ψ P mx).
@@ -1346,27 +1361,29 @@ Qed.
 
 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 ⊢ bi_bare P ∗ Q.
+Lemma persistent_and_affinely_sep_l_1 P Q `{!Persistent P} :
+  P ∧ Q ⊢ bi_affinely P ∗ Q.
 Proof.
-  rewrite {1}(persistent_persistently_2 P) persistently_and_bare_sep_l.
-  by rewrite -bare_idemp bare_persistently_elim.
+  rewrite {1}(persistent_persistently_2 P) persistently_and_affinely_sep_l.
+  by rewrite -affinely_idemp affinely_persistently_elim.
 Qed.
-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_affinely_sep_r_1 P Q `{!Persistent Q} :
+  P ∧ Q ⊢ P ∗ bi_affinely Q.
+Proof. by rewrite !(comm _ P) persistent_and_affinely_sep_l_1. Qed.
 
-Lemma persistent_and_bare_sep_l P Q `{!Persistent P, !Absorbing P} :
-  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 ∗ bi_bare Q.
-Proof. by rewrite -(persistent_persistently Q) persistently_and_bare_sep_r. Qed.
+Lemma persistent_and_affinely_sep_l P Q `{!Persistent P, !Absorbing P} :
+  P ∧ Q ⊣⊢ bi_affinely P ∗ Q.
+Proof. by rewrite -(persistent_persistently P) persistently_and_affinely_sep_l. Qed.
+Lemma persistent_and_affinely_sep_r P Q `{!Persistent Q, !Absorbing Q} :
+  P ∧ Q ⊣⊢ P ∗ bi_affinely Q.
+Proof. by rewrite -(persistent_persistently Q) persistently_and_affinely_sep_r. Qed.
 
 Lemma persistent_and_sep_1 P Q `{HPQ : !TCOr (Persistent P) (Persistent Q)} :
   P ∧ Q ⊢ P ∗ Q.
 Proof.
   destruct HPQ.
-  - by rewrite persistent_and_bare_sep_l_1 bare_elim.
-  - by rewrite persistent_and_bare_sep_r_1 bare_elim.
+  - by rewrite persistent_and_affinely_sep_l_1 affinely_elim.
+  - by rewrite persistent_and_affinely_sep_r_1 affinely_elim.
 Qed.
 
 Lemma persistent_sep_dup P `{!Persistent P, !Absorbing P} : P ⊣⊢ P ∗ P.
@@ -1377,10 +1394,10 @@ 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 ⊢ ▲ bi_bare P.
+Lemma persistent_absorbingly_affinely P `{!Persistent P} : P ⊢ ▲ bi_affinely P.
 Proof.
-  by rewrite {1}(persistent_persistently_2 P) -persistently_bare
-             persistently_elim_sink.
+  by rewrite {1}(persistent_persistently_2 P) -persistently_affinely
+             persistently_elim_absorbingly.
 Qed.
 
 Lemma persistent_and_sep_assoc P `{!Persistent P, !Absorbing P} Q R :
@@ -1542,14 +1559,14 @@ Lemma later_iff P Q : ▷ (P ↔ Q) ⊢ ▷ P ↔ ▷ Q.
 Proof. by rewrite /bi_iff later_and !later_impl. Qed.
 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 : 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.
-Proof. by rewrite -later_persistently later_bare_2. Qed.
-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.
+Lemma later_affinely_2 P : bi_affinely (▷ P) ⊢ ▷ bi_affinely P.
+Proof. rewrite /bi_affinely later_and. auto using later_intro. Qed.
+Lemma later_affinely_persistently_2 P : □ ▷ P ⊢ ▷ □ P.
+Proof. by rewrite -later_persistently later_affinely_2. Qed.
+Lemma later_affinely_persistently_if_2 p P : □?p ▷ P ⊢ ▷ □?p P.
+Proof. destruct p; simpl; auto using later_affinely_persistently_2. Qed.
+Lemma later_absorbingly P : ▷ ▲ P ⊣⊢ ▲ ▷ P.
+Proof. by rewrite /bi_absorbingly later_sep later_True. Qed.
 
 Global Instance later_persistent P : Persistent P → Persistent (▷ P).
 Proof.
@@ -1557,7 +1574,7 @@ Proof.
                      later_persistently.
 Qed.
 Global Instance later_absorbing P : Absorbing P → Absorbing (▷ P).
-Proof. intros ?. by rewrite /Absorbing -later_sink absorbing. Qed.
+Proof. intros ?. by rewrite /Absorbing -later_absorbingly absorbing. Qed.
 
 (* Iterated later modality *)
 Global Instance laterN_ne m : NonExpansive (@bi_laterN PROP m).
@@ -1613,14 +1630,14 @@ Proof. by rewrite /bi_iff laterN_and !laterN_impl. Qed.
 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 : 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.
-Proof. by rewrite -laterN_persistently laterN_bare_2. Qed.
-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.
+Lemma laterN_affinely_2 n P : bi_affinely (▷^n P) ⊢ ▷^n bi_affinely P.
+Proof. rewrite /bi_affinely laterN_and. auto using laterN_intro. Qed.
+Lemma laterN_affinely_persistently_2 n P : □ ▷^n P ⊢ ▷^n □ P.
+Proof. by rewrite -laterN_persistently laterN_affinely_2. Qed.
+Lemma laterN_affinely_persistently_if_2 n p P : □?p ▷^n P ⊢ ▷^n □?p P.
+Proof. destruct p; simpl; auto using laterN_affinely_persistently_2. Qed.
+Lemma laterN_absorbingly n P : ▷^n ▲ P ⊣⊢ ▲ ▷^n P.
+Proof. by rewrite /bi_absorbingly laterN_sep laterN_True. Qed.
 
 Global Instance laterN_persistent n P : Persistent P → Persistent (▷^n P).
 Proof. induction n; apply _. Qed.
@@ -1678,23 +1695,24 @@ Lemma except_0_persistently P : ◇ bi_persistently P ⊣⊢ bi_persistently (
 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.
-Proof. by rewrite -except_0_persistently except_0_bare_2. Qed.
-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.
+Lemma except_0_affinely_2 P : bi_affinely (◇ P) ⊢ ◇ bi_affinely P.
+Proof. rewrite /bi_affinely except_0_and. auto using except_0_intro. Qed.
+Lemma except_0_affinely_persistently_2 P : □ ◇ P ⊢ ◇ □ P.
+Proof. by rewrite -except_0_persistently except_0_affinely_2. Qed.
+Lemma except_0_affinely_persistently_if_2 p P : □?p ◇ P ⊢ ◇ □?p P.
+Proof. destruct p; simpl; auto using except_0_affinely_persistently_2. Qed.
+Lemma except_0_absorbingly P : ◇ ▲ P ⊣⊢ ▲ ◇ P.
+Proof. by rewrite /bi_absorbingly except_0_sep except_0_True. Qed.
 
 Lemma except_0_frame_l P Q : P ∗ ◇ Q ⊢ ◇ (P ∗ Q).
 Proof. by rewrite {1}(except_0_intro P) except_0_sep. Qed.
 Lemma except_0_frame_r P Q : ◇ P ∗ Q ⊢ ◇ (P ∗ Q).
 Proof. by rewrite {1}(except_0_intro Q) except_0_sep. Qed.
 
-Lemma later_bare_1 `{!Timeless (emp%I : PROP)} P : ▷ bi_bare P ⊢ ◇ bi_bare (▷ P).
+Lemma later_affinely_1 `{!Timeless (emp%I : PROP)} P :
+  ▷ bi_affinely P ⊢ ◇ bi_affinely (▷ P).
 Proof.
-  rewrite /bi_bare later_and (timeless emp%I) except_0_and.
+  rewrite /bi_affinely later_and (timeless emp%I) except_0_and.
   by apply and_mono, except_0_intro.
 Qed.
 
@@ -1758,11 +1776,11 @@ Proof.
   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 (bi_bare P).
-Proof. rewrite /bi_bare; apply _. Qed.
-Global Instance sink_timeless P : Timeless P → Timeless (▲ P).
-Proof. rewrite /bi_sink; apply _. Qed.
+Global Instance affinely_timeless P :
+  Timeless (emp%I : PROP) → Timeless P → Timeless (bi_affinely P).
+Proof. rewrite /bi_affinely; apply _. Qed.
+Global Instance absorbingly_timeless P : Timeless P → Timeless (▲ P).
+Proof. rewrite /bi_absorbingly; apply _. Qed.
 
 Global Instance eq_timeless {A : ofeT} (a b : A) :
   Discrete a → Timeless (a ≡ b : PROP)%I.
diff --git a/theories/bi/fractional.v b/theories/bi/fractional.v
index 38dc36fd00c3b2b416e49e0729f55485bfb9b279..370f735b6324fe4c3b354a18d813bf9dbeb11ccd 100644
--- a/theories/bi/fractional.v
+++ b/theories/bi/fractional.v
@@ -173,6 +173,6 @@ Section fractional.
     - rewrite fractional /Frame /MakeSep=><-<-. by rewrite assoc.
     - rewrite fractional /Frame /MakeSep=><-<-=>_.
       by rewrite (comm _ Q (Φ q0)) !assoc (comm _ (Φ _)).
-    - move=>-[-> _]->. by rewrite bi.bare_persistently_if_elim -fractional Qp_div_2.
+    - move=>-[-> _]->. by rewrite bi.affinely_persistently_if_elim -fractional Qp_div_2.
   Qed.
 End fractional.
diff --git a/theories/program_logic/hoare.v b/theories/program_logic/hoare.v
index 7ff1a8c9971cc43126864596de37e662d0b1fbef..e00826d27961fa179ecc330e4942a7ca78f88ef9 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. intros. by apply bare_mono, persistently_mono, wand_mono, wp_mono. Qed.
+Proof. intros. by apply affinely_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 96a456cb61a4ed7758dd5f07f0e2ae6612e8f501..70efe4a8fc8de075de9d439023cb9f23bbc0aa6a 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -11,59 +11,59 @@ Implicit Types P Q R : PROP.
 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 (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 :
+Global Instance into_internal_eq_affinely {A : ofeT} (x y : A) P :
+  IntoInternalEq P x y → IntoInternalEq (bi_affinely P) x y.
+Proof. rewrite /IntoInternalEq=> ->. by rewrite affinely_elim. Qed.
+Global Instance into_internal_eq_absorbingly {A : ofeT} (x y : A) P :
   IntoInternalEq P x y → IntoInternalEq (▲ P) x y.
-Proof. rewrite /IntoInternalEq=> ->. by rewrite sink_internal_eq. Qed.
+Proof. rewrite /IntoInternalEq=> ->. by rewrite absorbingly_internal_eq. Qed.
 Global Instance into_internal_eq_persistently {A : ofeT} (x y : A) P :
   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 (bi_bare P) P | 100.
-Proof. by rewrite /FromBare. Qed.
+(* FromAffinely *)
+Global Instance from_affinely_affine P : Affine P → FromAffinely P P.
+Proof. intros. by rewrite /FromAffinely affinely_elim. Qed.
+Global Instance from_affinely_default P : FromAffinely (bi_affinely P) P | 100.
+Proof. by rewrite /FromAffinely. Qed.
 
-(* IntoSink *)
-Global Instance into_sink_True : @IntoSink PROP True emp | 0.
-Proof. by rewrite /IntoSink -sink_True_emp sink_pure. Qed.
-Global Instance into_sink_absorbing P : Absorbing P → IntoSink P P | 1.
-Proof. intros. by rewrite /IntoSink absorbing_sink. Qed.
-Global Instance into_sink_default P : IntoSink (â–² P) P | 100.
-Proof. by rewrite /IntoSink. Qed.
+(* IntoAbsorbingly *)
+Global Instance into_absorbingly_True : @IntoAbsorbingly PROP True emp | 0.
+Proof. by rewrite /IntoAbsorbingly -absorbingly_True_emp absorbingly_pure. Qed.
+Global Instance into_absorbingly_absorbing P : Absorbing P → IntoAbsorbingly P P | 1.
+Proof. intros. by rewrite /IntoAbsorbingly absorbing_absorbingly. Qed.
+Global Instance into_absorbingly_default P : IntoAbsorbingly (â–² P) P | 100.
+Proof. by rewrite /IntoAbsorbingly. Qed.
 
 (* FromAssumption *)
 Global Instance from_assumption_exact p P : FromAssumption p P P | 0.
-Proof. by rewrite /FromAssumption /= bare_persistently_if_elim. Qed.
+Proof. by rewrite /FromAssumption /= affinely_persistently_if_elim. Qed.
 
 Global Instance from_assumption_persistently_r P Q :
   FromAssumption true P Q → FromAssumption true P (bi_persistently Q).
 Proof.
   rewrite /FromAssumption /= =><-.
-  by rewrite -{1}bare_persistently_idemp bare_elim.
+  by rewrite -{1}affinely_persistently_idemp affinely_elim.
 Qed.
-Global Instance from_assumption_bare_r 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 :
+Global Instance from_assumption_affinely_r P Q :
+  FromAssumption true P Q → FromAssumption true P (bi_affinely Q).
+Proof. rewrite /FromAssumption /= =><-. by rewrite affinely_idemp. Qed.
+Global Instance from_assumption_absorbingly_r p P Q :
   FromAssumption p P Q → FromAssumption p P (▲ Q).
-Proof. rewrite /FromAssumption /= =><-. apply sink_intro. Qed.
+Proof. rewrite /FromAssumption /= =><-. apply absorbingly_intro. Qed.
 
-Global Instance from_assumption_bare_persistently_l p P Q :
+Global Instance from_assumption_affinely_persistently_l p P Q :
   FromAssumption true P Q → FromAssumption p (□ P) Q.
-Proof. rewrite /FromAssumption /= =><-. by rewrite bare_persistently_if_elim. Qed.
+Proof. rewrite /FromAssumption /= =><-. by rewrite affinely_persistently_if_elim. Qed.
 Global Instance from_assumption_persistently_l_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 (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 (bi_bare P) Q.
-Proof. rewrite /FromAssumption /= =><-. by rewrite bare_elim. Qed.
+Proof. rewrite /FromAssumption /= =><-. by rewrite affine_affinely. Qed.
+Global Instance from_assumption_affinely_l_true p P Q :
+  FromAssumption p P Q → FromAssumption p (bi_affinely P) Q.
+Proof. rewrite /FromAssumption /= =><-. by rewrite affinely_elim. Qed.
 
 Global Instance from_assumption_forall {A} p (Φ : A → PROP) Q x :
   FromAssumption p (Φ x) Q → FromAssumption p (∀ x, Φ x) Q.
@@ -101,11 +101,13 @@ 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 (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 (bi_persistently P) φ.
+Global Instance into_pure_affinely P φ :
+  IntoPure P φ → IntoPure (bi_affinely P) φ.
+Proof. rewrite /IntoPure=> ->. apply affinely_elim. Qed.
+Global Instance into_pure_absorbingly P φ : IntoPure P φ → IntoPure (▲ P) φ.
+Proof. rewrite /IntoPure=> ->. by rewrite absorbingly_pure. Qed.
+Global Instance into_pure_persistently P φ :
+  IntoPure P φ → IntoPure (bi_persistently P) φ.
 Proof. rewrite /IntoPure=> ->. apply: persistently_elim. Qed.
 
 (* FromPure *)
@@ -145,11 +147,11 @@ Qed.
 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.
+Global Instance from_pure_affinely P φ `{!Affine P} :
+  FromPure P φ → FromPure (bi_affinely P) φ.
+Proof. by rewrite /FromPure affine_affinely. Qed.
+Global Instance from_pure_absorbingly P φ : FromPure P φ → FromPure (▲ P) φ.
+Proof. rewrite /FromPure=> <-. by rewrite absorbingly_pure. Qed.
 
 (* IntoPersistent *)
 Global Instance into_persistent_persistently p P Q :
@@ -158,9 +160,9 @@ 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 (bi_bare P) Q | 0.
-Proof. rewrite /IntoPersistent /= => <-. by rewrite bare_elim. Qed.
+Global Instance into_persistent_affinely p P Q :
+  IntoPersistent p P Q → IntoPersistent p (bi_affinely P) Q | 0.
+Proof. rewrite /IntoPersistent /= => <-. by rewrite affinely_elim. Qed.
 Global Instance into_persistent_here P : IntoPersistent true P P | 1.
 Proof. by rewrite /IntoPersistent. Qed.
 Global Instance into_persistent_persistent P :
@@ -173,17 +175,19 @@ Proof. by rewrite /FromPersistent. Qed.
 Global Instance from_persistent_persistently a P Q :
   FromPersistent a false P Q → FromPersistent false true (bi_persistently P) Q | 0.
 Proof.
-  rewrite /FromPersistent /= => <-. by destruct a; rewrite /= ?persistently_bare.
+  rewrite /FromPersistent /= => <-. by destruct a; rewrite /= ?persistently_affinely.
+Qed.
+Global Instance from_persistent_affinely a p P Q :
+  FromPersistent a p P Q → FromPersistent true p (bi_affinely P) Q | 0.
+Proof.
+  rewrite /FromPersistent /= => <-. destruct a; by rewrite /= ?affinely_idemp.
 Qed.
-Global Instance from_persistent_bare a p P Q :
-  FromPersistent a p P Q → FromPersistent true p (bi_bare P) Q | 0.
-Proof. rewrite /FromPersistent /= => <-. destruct a; by rewrite /= ?bare_idemp. Qed.
 
 (* IntoWand *)
 Global Instance into_wand_wand p q P Q P' :
   FromAssumption q P P' → IntoWand p q (P' -∗ Q) P Q.
 Proof.
-  rewrite /FromAssumption /IntoWand=> HP. by rewrite HP bare_persistently_if_elim.
+  rewrite /FromAssumption /IntoWand=> HP. by rewrite HP affinely_persistently_if_elim.
 Qed.
 
 Global Instance into_wand_impl_false_false `{!AffineBI PROP} P Q P' :
@@ -198,8 +202,8 @@ Global Instance into_wand_impl_false_true P Q P' :
   IntoWand false true (P' → Q) P Q.
 Proof.
   rewrite /IntoWand /FromAssumption /= => ? HP. apply wand_intro_l.
-  rewrite -(bare_persistently_idemp P) HP.
-  by rewrite -persistently_and_bare_sep_l persistently_elim impl_elim_r.
+  rewrite -(affinely_persistently_idemp P) HP.
+  by rewrite -persistently_and_affinely_sep_l persistently_elim impl_elim_r.
 Qed.
 
 Global Instance into_wand_impl_true_false P Q P' :
@@ -207,16 +211,16 @@ Global Instance into_wand_impl_true_false P Q P' :
   IntoWand true false (P' → Q) P Q.
 Proof.
   rewrite /FromAssumption /IntoWand /= => ? HP. apply wand_intro_r.
-  rewrite -persistently_and_bare_sep_l HP -{2}(affine_bare P') -bare_and_lr.
-  by rewrite bare_persistently_elim impl_elim_l.
+  rewrite -persistently_and_affinely_sep_l HP -{2}(affine_affinely P') -affinely_and_lr.
+  by rewrite affinely_persistently_elim impl_elim_l.
 Qed.
 
 Global Instance into_wand_impl_true_true P Q P' :
   FromAssumption true P P' → IntoWand true true (P' → Q) P Q.
 Proof.
   rewrite /FromAssumption /IntoWand /= => <-. apply wand_intro_l.
-  rewrite -{1}(bare_persistently_idemp P) -and_sep_bare_persistently.
-  by rewrite -bare_persistently_and impl_elim_r bare_persistently_elim.
+  rewrite -{1}(affinely_persistently_idemp P) -and_sep_affinely_persistently.
+  by rewrite -affinely_persistently_and impl_elim_r affinely_persistently_elim.
 Qed.
 
 Global Instance into_wand_and_l p q R1 R2 P' Q' :
@@ -237,27 +241,27 @@ Global Instance into_wand_persistently_false `{!AffineBI PROP} 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 :
+Global Instance into_wand_affinely_persistently 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.
+Proof. by rewrite /IntoWand affinely_persistently_elim. Qed.
 
 (* FromAnd *)
 Global Instance from_and_and P1 P2 : FromAnd (P1 ∧ P2) P1 P2 | 100.
 Proof. by rewrite /FromAnd. Qed.
 Global Instance from_and_sep_persistent_l P1 P1' P2 :
-  FromBare P1 P1' → Persistent P1' → FromAnd (P1 ∗ P2) P1' P2 | 9.
+  FromAffinely P1 P1' → Persistent P1' → FromAnd (P1 ∗ P2) P1' P2 | 9.
 Proof.
-  rewrite /FromBare /FromAnd=> <- ?. by rewrite persistent_and_bare_sep_l_1.
+  rewrite /FromAffinely /FromAnd=> <- ?. by rewrite persistent_and_affinely_sep_l_1.
 Qed.
 Global Instance from_and_sep_persistent_r P1 P2 P2' :
-  FromBare P2 P2' → Persistent P2' → FromAnd (P1 ∗ P2) P1 P2' | 10.
+  FromAffinely P2 P2' → Persistent P2' → FromAnd (P1 ∗ P2) P1 P2' | 10.
 Proof.
-  rewrite /FromBare /FromAnd=> <- ?. by rewrite persistent_and_bare_sep_r_1.
+  rewrite /FromAffinely /FromAnd=> <- ?. by rewrite persistent_and_affinely_sep_r_1.
 Qed.
 Global Instance from_and_sep_persistent P1 P2 :
   Persistent P1 → Persistent P2 → FromAnd (P1 ∗ P2) P1 P2 | 11.
 Proof.
-  rewrite /FromBare /FromAnd. intros ??. by rewrite -persistent_and_sep_1.
+  rewrite /FromAffinely /FromAnd. intros ??. by rewrite -persistent_and_sep_1.
 Qed.
 
 Global Instance from_and_pure φ ψ : @FromAnd PROP ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
@@ -293,12 +297,12 @@ Proof. intros. by rewrite /FromSep sep_and. Qed.
 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 (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 :
+Global Instance from_sep_affinely P Q1 Q2 :
+  FromSep P Q1 Q2 → FromSep (bi_affinely P) (bi_affinely Q1) (bi_affinely Q2).
+Proof. rewrite /FromSep=> <-. by rewrite affinely_sep_2. Qed.
+Global Instance from_sep_absorbingly P Q1 Q2 :
   FromSep P Q1 Q2 → FromSep (▲ P) (▲ Q1) (▲ Q2).
-Proof. rewrite /FromSep=> <-. by rewrite sink_sep. Qed.
+Proof. rewrite /FromSep=> <-. by rewrite absorbingly_sep. Qed.
 Global Instance from_sep_persistently P Q1 Q2 :
   FromSep P Q1 Q2 →
   FromSep (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
@@ -314,18 +318,18 @@ Proof. by rewrite /FromSep big_opL_app. Qed.
 
 (* IntoAnd *)
 Global Instance into_and_and p P Q : IntoAnd p (P ∧ Q) P Q | 10.
-Proof. by rewrite /IntoAnd bare_persistently_if_and. Qed.
+Proof. by rewrite /IntoAnd affinely_persistently_if_and. Qed.
 Global Instance into_and_and_affine_l P Q Q' :
-  Affine P → FromBare Q' Q → IntoAnd false (P ∧ Q) P Q'.
+  Affine P → FromAffinely Q' Q → IntoAnd false (P ∧ Q) P Q'.
 Proof.
   intros. rewrite /IntoAnd /=.
-  by rewrite -(affine_bare P) bare_and_l bare_and (from_bare Q').
+  by rewrite -(affine_affinely P) affinely_and_l affinely_and (from_affinely Q').
 Qed.
 Global Instance into_and_and_affine_r P P' Q :
-  Affine Q → FromBare P' P → IntoAnd false (P ∧ Q) P' Q.
+  Affine Q → FromAffinely P' P → IntoAnd false (P ∧ Q) P' Q.
 Proof.
   intros. rewrite /IntoAnd /=.
-  by rewrite -(affine_bare Q) bare_and_r bare_and (from_bare P').
+  by rewrite -(affine_affinely Q) affinely_and_r affinely_and (from_affinely P').
 Qed.
 
 Global Instance into_and_sep `{PositiveBI PROP} P Q : IntoAnd true (P ∗ Q) P Q.
@@ -334,14 +338,14 @@ Proof.
 Qed.
 
 Global Instance into_and_pure p φ ψ : @IntoAnd PROP p ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
-Proof. by rewrite /IntoAnd pure_and bare_persistently_if_and. Qed.
+Proof. by rewrite /IntoAnd pure_and affinely_persistently_if_and. Qed.
 
-Global Instance into_and_bare p P Q1 Q2 :
-  IntoAnd p P Q1 Q2 → IntoAnd p (bi_bare P) (bi_bare Q1) (bi_bare Q2).
+Global Instance into_and_affinely p P Q1 Q2 :
+  IntoAnd p P Q1 Q2 → IntoAnd p (bi_affinely P) (bi_affinely Q1) (bi_affinely Q2).
 Proof.
   rewrite /IntoAnd. destruct p; simpl.
-  - by rewrite -bare_and !persistently_bare.
-  - intros ->. by rewrite bare_and.
+  - by rewrite -affinely_and !persistently_affinely.
+  - intros ->. by rewrite affinely_and.
 Qed.
 Global Instance into_and_persistently p P Q1 Q2 :
   IntoAnd p P Q1 Q2 →
@@ -357,8 +361,8 @@ Global Instance into_sep_sep P Q : IntoSep (P ∗ Q) P Q.
 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 (bi_bare P)%I Q Q.
+  | and_into_sep_affine P Q Q' : Affine P → FromAffinely Q' Q → AndIntoSep P P Q Q'
+  | and_into_sep P Q : AndIntoSep P (bi_affinely P)%I Q Q.
 Existing Class AndIntoSep.
 Global Existing Instance and_into_sep_affine | 0.
 Global Existing Instance and_into_sep | 2.
@@ -367,28 +371,28 @@ Global Instance into_sep_and_persistent_l P P' Q Q' :
   Persistent P → AndIntoSep P P' Q Q' → IntoSep (P ∧ Q) P' Q'.
 Proof.
   destruct 2 as [P Q Q'|P Q]; rewrite /IntoSep.
-  - rewrite -(from_bare Q') -(affine_bare P) bare_and_lr.
-    by rewrite persistent_and_bare_sep_l_1.
-  - by rewrite persistent_and_bare_sep_l_1.
+  - rewrite -(from_affinely Q') -(affine_affinely P) affinely_and_lr.
+    by rewrite persistent_and_affinely_sep_l_1.
+  - by rewrite persistent_and_affinely_sep_l_1.
 Qed.
 Global Instance into_sep_and_persistent_r P P' Q Q' :
   Persistent Q → AndIntoSep Q Q' P P' → IntoSep (P ∧ Q) P' Q'.
 Proof.
   destruct 2 as [Q P P'|Q P]; rewrite /IntoSep.
-  - rewrite -(from_bare P') -(affine_bare Q) -bare_and_lr.
-    by rewrite persistent_and_bare_sep_r_1.
-  - by rewrite persistent_and_bare_sep_r_1.
+  - rewrite -(from_affinely P') -(affine_affinely Q) -affinely_and_lr.
+    by rewrite persistent_and_affinely_sep_r_1.
+  - by rewrite persistent_and_affinely_sep_r_1.
 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 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 (bi_bare P) Q1 Q2 | 20.
-Proof. rewrite /IntoSep /= => ->. by rewrite bare_elim. Qed.
+(* FIXME: This instance is kind of strange, it just gets rid of the bi_affinely. Also, it
+overlaps with `into_sep_affinely_later`, and hence has lower precedence. *)
+Global Instance into_sep_affinely P Q1 Q2 :
+  IntoSep P Q1 Q2 → IntoSep (bi_affinely P) Q1 Q2 | 20.
+Proof. rewrite /IntoSep /= => ->. by rewrite affinely_elim. Qed.
 
 Global Instance into_sep_persistently `{PositiveBI PROP} P Q1 Q2 :
   IntoSep P Q1 Q2 →
@@ -414,12 +418,12 @@ Global Instance from_or_or P1 P2 : FromOr (P1 ∨ P2) P1 P2.
 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 (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 :
+Global Instance from_or_affinely P Q1 Q2 :
+  FromOr P Q1 Q2 → FromOr (bi_affinely P) (bi_affinely Q1) (bi_affinely Q2).
+Proof. rewrite /FromOr=> <-. by rewrite affinely_or. Qed.
+Global Instance from_or_absorbingly P Q1 Q2 :
   FromOr P Q1 Q2 → FromOr (▲ P) (▲ Q1) (▲ Q2).
-Proof. rewrite /FromOr=> <-. by rewrite sink_or. Qed.
+Proof. rewrite /FromOr=> <-. by rewrite absorbingly_or. Qed.
 Global Instance from_or_persistently P Q1 Q2 :
   FromOr P Q1 Q2 →
   FromOr (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
@@ -430,12 +434,12 @@ Global Instance into_or_or P Q : IntoOr (P ∨ Q) P Q.
 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 (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 :
+Global Instance into_or_affinely P Q1 Q2 :
+  IntoOr P Q1 Q2 → IntoOr (bi_affinely P) (bi_affinely Q1) (bi_affinely Q2).
+Proof. rewrite /IntoOr=>->. by rewrite affinely_or. Qed.
+Global Instance into_or_absorbingly P Q1 Q2 :
   IntoOr P Q1 Q2 → IntoOr (▲ P) (▲ Q1) (▲ Q2).
-Proof. rewrite /IntoOr=>->. by rewrite sink_or. Qed.
+Proof. rewrite /IntoOr=>->. by rewrite absorbingly_or. Qed.
 Global Instance into_or_persistently P Q1 Q2 :
   IntoOr P Q1 Q2 →
   IntoOr (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
@@ -447,12 +451,12 @@ Proof. by rewrite /FromExist. Qed.
 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 (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) :
+Global Instance from_exist_affinely {A} P (Φ : A → PROP) :
+  FromExist P Φ → FromExist (bi_affinely P) (λ a, bi_affinely (Φ a))%I.
+Proof. rewrite /FromExist=> <-. by rewrite affinely_exist. Qed.
+Global Instance from_exist_absorbingly {A} P (Φ : A → PROP) :
   FromExist P Φ → FromExist (▲ P) (λ a, ▲ (Φ a))%I.
-Proof. rewrite /FromExist=> <-. by rewrite sink_exist. Qed.
+Proof. rewrite /FromExist=> <-. by rewrite absorbingly_exist. Qed.
 Global Instance from_exist_persistently {A} P (Φ : A → PROP) :
   FromExist P Φ → FromExist (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
 Proof. rewrite /FromExist=> <-. by rewrite persistently_exist. Qed.
@@ -463,9 +467,9 @@ Proof. by rewrite /IntoExist. Qed.
 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 (bi_bare P) (λ a, bi_bare (Φ a))%I.
-Proof. rewrite /IntoExist=> HP. by rewrite HP bare_exist. Qed.
+Global Instance into_exist_affinely {A} P (Φ : A → PROP) :
+  IntoExist P Φ → IntoExist (bi_affinely P) (λ a, bi_affinely (Φ a))%I.
+Proof. rewrite /IntoExist=> HP. by rewrite HP affinely_exist. Qed.
 Global Instance into_exist_and_pure P Q φ :
   IntoPureT P φ → IntoExist (P ∧ Q) (λ _ : φ, Q).
 Proof.
@@ -479,9 +483,9 @@ Proof.
   eapply (pure_elim φ'); [by rewrite (into_pure P); apply sep_elim_l, _|]=>?.
   rewrite -exist_intro //. apply sep_elim_r, _.
 Qed.
-Global Instance into_exist_sink {A} P (Φ : A → PROP) :
+Global Instance into_exist_absorbingly {A} P (Φ : A → PROP) :
   IntoExist P Φ → IntoExist (▲ P) (λ a, ▲ (Φ a))%I.
-Proof. rewrite /IntoExist=> HP. by rewrite HP sink_exist. Qed.
+Proof. rewrite /IntoExist=> HP. by rewrite HP absorbingly_exist. Qed.
 Global Instance into_exist_persistently {A} P (Φ : A → PROP) :
   IntoExist P Φ → IntoExist (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
 Proof. rewrite /IntoExist=> HP. by rewrite HP persistently_exist. Qed.
@@ -489,9 +493,9 @@ 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 (bi_bare P) (λ a, bi_bare (Φ a))%I.
-Proof. rewrite /IntoForall=> HP. by rewrite HP bare_forall. Qed.
+Global Instance into_forall_affinely {A} P (Φ : A → PROP) :
+  IntoForall P Φ → IntoForall (bi_affinely P) (λ a, bi_affinely (Φ a))%I.
+Proof. rewrite /IntoForall=> HP. by rewrite HP affinely_forall. Qed.
 Global Instance into_forall_persistently {A} P (Φ : A → PROP) :
   IntoForall P Φ → IntoForall (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
 Proof. rewrite /IntoForall=> HP. by rewrite HP persistently_forall. Qed.
@@ -513,14 +517,16 @@ Global Instance from_forall_wand_pure P Q φ :
   FromForall (P -∗ Q)%I (λ _ : φ, Q)%I.
 Proof.
   intros [|] (φ'&->&?); rewrite /FromForall; apply wand_intro_r.
-  - rewrite -(affine_bare P) (into_pure P) -persistent_and_bare_sep_r.
+  - rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_r.
     apply pure_elim_r=>?. by rewrite forall_elim.
   - 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_affinely `{AffineBI PROP} {A} P (Φ : A → PROP) :
+  FromForall P Φ → FromForall (bi_affinely P)%I (λ a, bi_affinely (Φ a))%I.
+Proof.
+  rewrite /FromForall=> <-. rewrite affine_affinely. by setoid_rewrite affinely_elim.
+Qed.
 Global Instance from_forall_persistently {A} P (Φ : A → PROP) :
   FromForall P Φ → FromForall (bi_persistently P)%I (λ a, bi_persistently (Φ a))%I.
 Proof. rewrite /FromForall=> <-. by rewrite persistently_forall. Qed.
@@ -537,25 +543,29 @@ Global Instance forall_modal_wand {A} P P' (Φ Ψ : A → PROP) :
 Proof.
   rewrite /ElimModal=> H. apply forall_intro=> a. by rewrite (forall_elim a).
 Qed.
-Global Instance elim_modal_sink P Q : Absorbing Q → ElimModal (▲ P) P Q Q.
+Global Instance elim_modal_absorbingly P Q : Absorbing Q → ElimModal (▲ P) P Q Q.
 Proof.
-  rewrite /ElimModal=> H. by rewrite sink_sep_l wand_elim_r absorbing_sink.
+  rewrite /ElimModal=> H. by rewrite absorbingly_sep_l wand_elim_r absorbing_absorbingly.
 Qed.
 
 (* Frame *)
 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.
+Proof. intros. by rewrite /Frame affinely_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 (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 (bi_bare R) R emp | 1.
-Proof. intros. by rewrite /Frame bare_persistently_if_elim bare_elim sep_elim_l. Qed.
+Proof. intros. by rewrite /Frame affinely_persistently_if_elim sep_elim_l. Qed.
+Global Instance frame_affinely_here_absorbing p R :
+  Absorbing R → Frame p (bi_affinely R) R True | 0.
+Proof.
+  intros. by rewrite /Frame affinely_persistently_if_elim affinely_elim sep_elim_l.
+Qed.
+Global Instance frame_affinely_here p R : Frame p (bi_affinely R) R emp | 1.
+Proof.
+  intros. by rewrite /Frame affinely_persistently_if_elim affinely_elim sep_elim_l.
+Qed.
 
 Global Instance frame_here_pure p φ Q : FromPure Q φ → Frame p ⌜φ⌝ Q True.
 Proof.
-  rewrite /FromPure /Frame=> <-. by rewrite bare_persistently_if_elim sep_elim_l.
+  rewrite /FromPure /Frame=> <-. by rewrite affinely_persistently_if_elim sep_elim_l.
 Qed.
 
 Class MakeSep (P Q PQ : PROP) := make_sep : P ∗ Q ⊣⊢ PQ.
@@ -566,11 +576,11 @@ Global Instance make_sep_emp_r P : MakeSep P emp P.
 Proof. by rewrite /MakeSep right_id. Qed.
 Global Instance make_sep_true_l P : Absorbing P → MakeSep True P P.
 Proof. intros. by rewrite /MakeSep True_sep. Qed.
-Global Instance make_and_emp_l_sink P : MakeSep True P (â–² P) | 10.
+Global Instance make_and_emp_l_absorbingly P : MakeSep True P (â–² P) | 10.
 Proof. intros. by rewrite /MakeSep. Qed.
 Global Instance make_sep_true_r P : Absorbing P → MakeSep P True P.
 Proof. intros. by rewrite /MakeSep sep_True. Qed.
-Global Instance make_and_emp_r_sink P : MakeSep P True (â–² P) | 10.
+Global Instance make_and_emp_r_absorbingly P : MakeSep P True (â–² P) | 10.
 Proof. intros. by rewrite /MakeSep comm. Qed.
 Global Instance make_sep_default P Q : MakeSep P Q (P ∗ Q) | 100.
 Proof. by rewrite /MakeSep. Qed.
@@ -580,7 +590,7 @@ Global Instance frame_sep_persistent_l R P1 P2 Q1 Q2 Q' :
   Frame true R (P1 ∗ P2) Q' | 9.
 Proof.
   rewrite /Frame /MaybeFrame /MakeSep /= => <- <- <-.
-  rewrite {1}(bare_persistently_sep_dup R). solve_sep_entails.
+  rewrite {1}(affinely_persistently_sep_dup R). solve_sep_entails.
 Qed.
 Global Instance frame_sep_l R P1 P2 Q Q' :
   Frame false R P1 Q → MakeSep Q P2 Q' → Frame false R (P1 ∗ P2) Q' | 9.
@@ -609,11 +619,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 (bi_bare P) | 10.
+Global Instance make_and_emp_l_affinely P : MakeAnd emp P (bi_affinely 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 (bi_bare P) | 10.
+Global Instance make_and_emp_r_affinely P : MakeAnd P emp (bi_affinely 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.
@@ -629,7 +639,7 @@ Global Instance frame_and_persistent_r R P1 P2 Q2 Q :
   Frame true R P2 Q2 →
   MakeAnd P1 Q2 Q → Frame true R (P1 ∧ P2) Q | 10.
 Proof.
-  rewrite /Frame /MakeAnd => <- <- /=. rewrite -!persistently_and_bare_sep_l.
+  rewrite /Frame /MakeAnd => <- <- /=. rewrite -!persistently_and_affinely_sep_l.
   auto using and_intro, and_elim_l', and_elim_r'.
 Qed.
 Global Instance frame_and_r R P1 P2 Q2 Q :
@@ -678,35 +688,35 @@ Proof.
   by rewrite assoc (comm _ P1) -assoc wand_elim_r.
 Qed.
 
-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 (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 (bi_bare P) Q'.
+Class MakeAffinely (P Q : PROP) := make_affinely : bi_affinely P ⊣⊢ Q.
+Arguments MakeAffinely _%I _%I.
+Global Instance make_affinely_True : MakeAffinely True emp | 0.
+Proof. by rewrite /MakeAffinely affinely_True_emp affinely_emp. Qed.
+Global Instance make_affinely_affine P : Affine P → MakeAffinely P P | 1.
+Proof. intros. by rewrite /MakeAffinely affine_affinely. Qed.
+Global Instance make_affinely_default P : MakeAffinely P (bi_affinely P) | 100.
+Proof. by rewrite /MakeAffinely. Qed.
+
+Global Instance frame_affinely R P Q Q' :
+  Frame true R P Q → MakeAffinely Q Q' → Frame true R (bi_affinely P) Q'.
 Proof.
-  rewrite /Frame /MakeBare=> <- <- /=.
-  by rewrite -{1}bare_idemp bare_sep_2.
+  rewrite /Frame /MakeAffinely=> <- <- /=.
+  by rewrite -{1}affinely_idemp affinely_sep_2.
 Qed.
 
-Class MakeSink (P Q : PROP) := make_sink : ▲ P ⊣⊢ Q.
-Arguments MakeSink _%I _%I.
-Global Instance make_sink_emp : MakeSink emp True | 0.
-Proof. by rewrite /MakeSink -sink_True_emp sink_pure. Qed.
-(* Note: there is no point in having an instance `Absorbing P → MakeSink P P`
+Class MakeAbsorbingly (P Q : PROP) := make_absorbingly : ▲ P ⊣⊢ Q.
+Arguments MakeAbsorbingly _%I _%I.
+Global Instance make_absorbingly_emp : MakeAbsorbingly emp True | 0.
+Proof. by rewrite /MakeAbsorbingly -absorbingly_True_emp absorbingly_pure. Qed.
+(* Note: there is no point in having an instance `Absorbing P → MakeAbsorbingly P P`
 because framing will never turn a proposition that is not absorbing into
 something that is absorbing. *)
-Global Instance make_sink_default P : MakeSink P (â–² P) | 100.
-Proof. by rewrite /MakeSink. Qed.
+Global Instance make_absorbingly_default P : MakeAbsorbingly P (â–² P) | 100.
+Proof. by rewrite /MakeAbsorbingly. Qed.
 
-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.
+Global Instance frame_absorbingly p R P Q Q' :
+  Frame p R P Q → MakeAbsorbingly Q Q' → Frame p R (▲ P) Q'.
+Proof. rewrite /Frame /MakeAbsorbingly=> <- <- /=. by rewrite absorbingly_sep_r. Qed.
 
 Class MakePersistently (P Q : PROP) := make_persistently : bi_persistently P ⊣⊢ Q.
 Arguments MakePersistently _%I _%I.
@@ -714,14 +724,15 @@ 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 (bi_persistently 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 (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
+  rewrite /Frame /MakePersistently=> <- <- /=. rewrite -persistently_and_affinely_sep_l.
+  by rewrite -persistently_sep_2 -persistently_and_sep_l_1 persistently_affinely
               persistently_idemp.
 Qed.
 
@@ -733,8 +744,8 @@ Global Instance frame_forall {A} p R (Φ Ψ : A → PROP) :
 Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.
 
 (* FromModal *)
-Global Instance from_modal_sink P : FromModal (â–² P) P.
-Proof. apply sink_intro. Qed.
+Global Instance from_modal_absorbingly P : FromModal (â–² P) P.
+Proof. apply absorbingly_intro. Qed.
 End bi_instances.
 
 
@@ -765,27 +776,27 @@ Proof. rewrite /FromPure=> ->. apply except_0_intro. Qed.
 Global Instance into_wand_later p q R P Q :
   IntoWand p q R P Q → IntoWand p q (▷ R) (▷ P) (▷ Q).
 Proof.
-  rewrite /IntoWand /= => HR. by rewrite !later_bare_persistently_if_2 -later_wand HR.
+  rewrite /IntoWand /= => HR. by rewrite !later_affinely_persistently_if_2 -later_wand HR.
 Qed.
 
 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_affinely_persistently_if_2 (later_intro (â–¡?p R)%I) -later_wand HR.
 Qed.
 
 Global Instance into_wand_laterN n p q R P Q :
   IntoWand p q R P Q → IntoWand p q (▷^n R) (▷^n P) (▷^n Q).
 Proof.
-  rewrite /IntoWand /= => HR. by rewrite !laterN_bare_persistently_if_2 -laterN_wand HR.
+  rewrite /IntoWand /= => HR. by rewrite !laterN_affinely_persistently_if_2 -laterN_wand HR.
 Qed.
 
 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_affinely_persistently_if_2 (laterN_intro _ (â–¡?p R)%I) -laterN_wand HR.
 Qed.
 
 (* FromAnd *)
@@ -814,20 +825,20 @@ Proof. rewrite /FromSep=><-. by rewrite except_0_sep. Qed.
 Global Instance into_and_later p P Q1 Q2 :
   IntoAnd p P Q1 Q2 → IntoAnd p (▷ P) (▷ Q1) (▷ Q2).
 Proof.
-  rewrite /IntoAnd=> HP. apply bare_persistently_if_intro'.
-  by rewrite later_bare_persistently_if_2 HP bare_persistently_if_elim later_and.
+  rewrite /IntoAnd=> HP. apply affinely_persistently_if_intro'.
+  by rewrite later_affinely_persistently_if_2 HP affinely_persistently_if_elim later_and.
 Qed.
 Global Instance into_and_laterN n p P Q1 Q2 :
   IntoAnd p P Q1 Q2 → IntoAnd p (▷^n P) (▷^n Q1) (▷^n Q2).
 Proof.
-  rewrite /IntoAnd=> HP. apply bare_persistently_if_intro'.
-  by rewrite laterN_bare_persistently_if_2 HP bare_persistently_if_elim laterN_and.
+  rewrite /IntoAnd=> HP. apply affinely_persistently_if_intro'.
+  by rewrite laterN_affinely_persistently_if_2 HP affinely_persistently_if_elim laterN_and.
 Qed.
 Global Instance into_and_except_0 p P Q1 Q2 :
   IntoAnd p P Q1 Q2 → IntoAnd p (◇ P) (◇ Q1) (◇ Q2).
 Proof.
-  rewrite /IntoAnd=> HP. apply bare_persistently_if_intro'.
-  by rewrite except_0_bare_persistently_if_2 HP bare_persistently_if_elim except_0_and.
+  rewrite /IntoAnd=> HP. apply affinely_persistently_if_intro'.
+  by rewrite except_0_affinely_persistently_if_2 HP affinely_persistently_if_elim except_0_and.
 Qed.
 
 (* IntoSep *)
@@ -842,14 +853,14 @@ Global Instance into_sep_except_0 P Q1 Q2 :
 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 :
+Global Instance into_sep_affinely_later `{!Timeless (emp%I : PROP)} P Q1 Q2 :
   Affine Q1 → Affine Q2 → IntoSep P Q1 Q2 →
-  IntoSep (bi_bare (â–· P)) (bi_bare (â–· Q1)) (bi_bare (â–· Q2)).
+  IntoSep (bi_affinely (â–· P)) (bi_affinely (â–· Q1)) (bi_affinely (â–· 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 (bi_bare (â–· False))%I) persistent_and_sep_1.
+  rewrite -{1}(affine_affinely Q1) -{1}(affine_affinely Q2) later_sep !later_affinely_1.
+  rewrite -except_0_sep /bi_except_0 affinely_or. apply or_elim, affinely_elim.
+  rewrite -(idemp bi_and (bi_affinely (â–· False))%I) persistent_and_sep_1.
   by rewrite -(False_elim Q1) -(False_elim Q2).
 Qed.
 
@@ -931,11 +942,11 @@ 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 (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_affinely P Q :
+  IntoExcept0 P Q → IntoExcept0 (bi_affinely P) (bi_affinely Q).
+Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_affinely_2. Qed.
+Global Instance into_timeless_absorbingly P Q : IntoExcept0 P Q → IntoExcept0 (▲ P) (▲ Q).
+Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_absorbingly. Qed.
 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.
@@ -961,7 +972,7 @@ Global Instance frame_later p R R' P Q Q' :
   IntoLaterN 1 R' R → Frame p R P Q → MakeLater Q Q' → Frame p R' (▷ P) Q'.
 Proof.
   rewrite /Frame /MakeLater /IntoLaterN=>-> <- <- /=.
-  by rewrite later_bare_persistently_if_2 later_sep.
+  by rewrite later_affinely_persistently_if_2 later_sep.
 Qed.
 
 Class MakeLaterN (n : nat) (P lP : PROP) := make_laterN : ▷^n P ⊣⊢ lP.
@@ -976,7 +987,7 @@ Global Instance frame_laterN p n R R' P Q Q' :
   IntoLaterN n R' R → Frame p R P Q → MakeLaterN n Q Q' → Frame p R' (▷^n P) Q'.
 Proof.
   rewrite /Frame /MakeLaterN /IntoLaterN=>-> <- <-.
-  by rewrite laterN_bare_persistently_if_2 laterN_sep.
+  by rewrite laterN_affinely_persistently_if_2 laterN_sep.
 Qed.
 
 Class MakeExcept0 (P Q : PROP) := make_except_0 : ◇ P ⊣⊢ Q.
@@ -1033,12 +1044,12 @@ Global Instance into_laterN_exist {A} n (Φ Ψ : A → PROP) :
   IntoLaterN' n (∃ x, Φ x) (∃ x, Ψ x).
 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 (bi_bare P) (bi_bare Q).
-Proof. rewrite /IntoLaterN=> ->. by rewrite laterN_bare_2. Qed.
-Global Instance into_later_sink n P Q :
+Global Instance into_later_affinely n P Q :
+  IntoLaterN n P Q → IntoLaterN n (bi_affinely P) (bi_affinely Q).
+Proof. rewrite /IntoLaterN=> ->. by rewrite laterN_affinely_2. Qed.
+Global Instance into_later_absorbingly n P Q :
   IntoLaterN n P Q → IntoLaterN n (▲ P) (▲ Q).
-Proof. rewrite /IntoLaterN=> ->. by rewrite laterN_sink. Qed.
+Proof. rewrite /IntoLaterN=> ->. by rewrite laterN_absorbingly. Qed.
 Global Instance into_later_persistently n P Q :
   IntoLaterN n P Q → IntoLaterN n (bi_persistently P) (bi_persistently Q).
 Proof. rewrite /IntoLaterN=> ->. by rewrite laterN_persistently. Qed.
@@ -1113,15 +1124,15 @@ 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_affinely n P Q `{AffineBI PROP} :
+  FromLaterN n P Q → FromLaterN n (bi_affinely P) (bi_affinely Q).
+Proof. rewrite /FromLaterN=><-. by rewrite affinely_elim affine_affinely. Qed.
 Global Instance from_later_persistently 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 :
+Global Instance from_later_absorbingly n P Q :
   FromLaterN n P Q → FromLaterN n (▲ P) (▲ Q).
-Proof. by rewrite /FromLaterN laterN_sink=> ->. Qed.
+Proof. by rewrite /FromLaterN laterN_absorbingly=> ->. Qed.
 
 Global Instance from_later_forall {A} n (Φ Ψ : A → PROP) :
   (∀ x, FromLaterN n (Φ x) (Ψ x)) → FromLaterN n (∀ x, Φ x) (∀ x, Ψ x).
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 4090d497a38ac14b0d7481ddbdafc1c39c62c0c9..88d6b667c26dc6614958adaf1975cc3358f651be 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -56,23 +56,23 @@ Arguments into_persistent {_} _ _%I _%I {_}.
 Hint Mode IntoPersistent + + ! - : typeclass_instances.
 
 Class FromPersistent {PROP : bi} (a p : bool) (P Q : PROP) :=
-  from_persistent : bi_bare_if a (bi_persistently_if p Q) ⊢ P.
+  from_persistent : bi_affinely_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 : bi_bare Q ⊢ P.
-Arguments FromBare {_} _%I _%type_scope : simpl never.
-Arguments from_bare {_} _%I _%type_scope {_}.
-Hint Mode FromBare + ! - : typeclass_instances.
-Hint Mode FromBare + - ! : typeclass_instances.
-
-Class IntoSink {PROP : bi} (P Q : PROP) := into_sink : P ⊢ ▲ Q.
-Arguments IntoSink {_} _%I _%I.
-Arguments into_sink {_} _%I _%I {_}.
-Hint Mode IntoSink + ! -  : typeclass_instances.
-Hint Mode IntoSink + - ! : typeclass_instances.
+Class FromAffinely {PROP : bi} (P Q : PROP) :=
+  from_affinely : bi_affinely Q ⊢ P.
+Arguments FromAffinely {_} _%I _%type_scope : simpl never.
+Arguments from_affinely {_} _%I _%type_scope {_}.
+Hint Mode FromAffinely + ! - : typeclass_instances.
+Hint Mode FromAffinely + - ! : typeclass_instances.
+
+Class IntoAbsorbingly {PROP : bi} (P Q : PROP) := into_absorbingly : P ⊢ ▲ Q.
+Arguments IntoAbsorbingly {_} _%I _%I.
+Arguments into_absorbingly {_} _%I _%I {_}.
+Hint Mode IntoAbsorbingly + ! -  : typeclass_instances.
+Hint Mode IntoAbsorbingly + - ! : typeclass_instances.
 
 Class IntoInternalEq {PROP : bi} {A : ofeT} (P : PROP) (x y : A) :=
   into_internal_eq : P ⊢ x ≡ y.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 0dbfee39609c40284e2bacbaeebf835437ebed00..850e3ce5bfc13778c313860a5c71432e5fab0cf6 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -145,8 +145,8 @@ Proof.
   destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
   - rewrite pure_True ?left_id; last (destruct Hwf; constructor;
       naive_solver eauto using env_delete_wf, env_delete_fresh).
-    rewrite (env_lookup_perm Γp) //= bare_persistently_and.
-    by rewrite and_sep_bare_persistently -assoc.
+    rewrite (env_lookup_perm Γp) //= affinely_persistently_and.
+    by rewrite and_sep_affinely_persistently -assoc.
   - destruct (Γs !! i) eqn:?; simplify_eq/=.
     rewrite pure_True ?left_id; last (destruct Hwf; constructor;
       naive_solver eauto using env_delete_wf, env_delete_fresh).
@@ -155,9 +155,9 @@ Qed.
 Lemma envs_lookup_persistent_sound Δ i P :
   envs_lookup i Δ = Some (true,P) → Δ ⊢ □ P ∗ Δ.
 Proof.
-  intros. rewrite -persistently_and_bare_sep_l. apply and_intro; last done.
+  intros. rewrite -persistently_and_affinely_sep_l. apply and_intro; last done.
   rewrite envs_lookup_sound //; simpl.
-  by rewrite -persistently_and_bare_sep_l and_elim_l.
+  by rewrite -persistently_and_affinely_sep_l and_elim_l.
 Qed.
 
 Lemma envs_lookup_split Δ i p P :
@@ -165,8 +165,8 @@ Lemma envs_lookup_split Δ i 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.
+  - rewrite pure_True // left_id (env_lookup_perm Γp) //=
+            affinely_persistently_and and_sep_affinely_persistently.
     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.
@@ -182,17 +182,17 @@ Lemma envs_lookup_delete_list_sound Δ Δ' js rp 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. }
+  { by rewrite affinely_persistently_emp left_id. }
   destruct (envs_lookup_delete j Δ) as [[[q1 P] Δ']|] eqn:Hj; simplify_eq/=.
   apply envs_lookup_delete_Some in Hj as [Hj ->].
   destruct (envs_lookup_delete_list js rp _) as [[[q2 Ps'] ?]|] eqn:?; simplify_eq/=.
-  rewrite -bare_persistently_if_sep_2 -assoc. destruct q1; simpl.
+  rewrite -affinely_persistently_if_sep_2 -assoc. destruct q1; simpl.
   - destruct rp.
     + rewrite envs_lookup_sound //; simpl.
-      by rewrite IH // (bare_persistently_bare_persistently_if q2).
+      by rewrite IH // (affinely_persistently_affinely_persistently_if q2).
     + rewrite envs_lookup_persistent_sound //.
-      by rewrite IH // (bare_persistently_bare_persistently_if q2).
-  - rewrite envs_lookup_sound // IH //; simpl. by rewrite bare_persistently_if_elim.
+      by rewrite IH // (affinely_persistently_affinely_persistently_if q2).
+  - rewrite envs_lookup_sound // IH //; simpl. by rewrite affinely_persistently_if_elim.
 Qed.
 
 Lemma envs_lookup_snoc Δ i p P :
@@ -217,7 +217,7 @@ Proof.
   - apply and_intro; [apply pure_intro|].
     + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
       intros j; destruct (strings.string_beq_reflect j i); naive_solver.
-    + by rewrite bare_persistently_and and_sep_bare_persistently assoc.
+    + by rewrite affinely_persistently_and and_sep_affinely_persistently assoc.
   - apply and_intro; [apply pure_intro|].
     + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
       intros j; destruct (strings.string_beq_reflect j i); naive_solver.
@@ -236,7 +236,7 @@ Proof.
       intros j. apply (env_app_disjoint _ _ _ j) in Happ.
       naive_solver eauto using env_app_fresh.
     + rewrite (env_app_perm _ _ Γp') //.
-      rewrite big_opL_app bare_persistently_and and_sep_bare_persistently.
+      rewrite big_opL_app affinely_persistently_and and_sep_affinely_persistently.
       solve_sep_entails.
   - destruct (env_app Γ Γp) eqn:Happ,
       (env_app Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
@@ -264,7 +264,7 @@ Proof.
       intros j. apply (env_app_disjoint _ _ _ j) in Happ.
       destruct (decide (i = j)); try naive_solver eauto using env_replace_fresh.
     + rewrite (env_replace_perm _ _ Γp') //.
-      rewrite big_opL_app bare_persistently_and and_sep_bare_persistently.
+      rewrite big_opL_app affinely_persistently_and and_sep_affinely_persistently.
       solve_sep_entails.
   - destruct (env_app Γ Γp) eqn:Happ,
       (env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
@@ -335,12 +335,12 @@ Proof.
   apply pure_intro. destruct Hwf; constructor; simpl; auto using Enil_wf.
 Qed.
 
-Lemma env_spatial_is_nil_bare_persistently Δ :
+Lemma env_spatial_is_nil_affinely_persistently Δ :
   env_spatial_is_nil Δ = true → Δ ⊢ □ Δ.
 Proof.
   intros. unfold of_envs; destruct Δ as [? []]; simplify_eq/=.
-  rewrite !right_id {1}bare_and_r persistently_and.
-  by rewrite persistently_bare persistently_idemp persistently_pure.
+  rewrite !right_id {1}affinely_and_r persistently_and.
+  by rewrite persistently_affinely persistently_idemp persistently_pure.
 Qed.
 
 Lemma envs_lookup_envs_delete Δ i p P :
@@ -385,10 +385,10 @@ Lemma envs_split_sound Δ lr js Δ1 Δ2 :
 Proof.
   rewrite /envs_split=> ?. rewrite -(idemp bi_and Δ).
   rewrite {2}envs_clear_spatial_sound.
-  rewrite (env_spatial_is_nil_bare_persistently (envs_clear_spatial _)) //.
-  rewrite -persistently_and_bare_sep_l.
+  rewrite (env_spatial_is_nil_affinely_persistently (envs_clear_spatial _)) //.
+  rewrite -persistently_and_affinely_sep_l.
   rewrite (and_elim_l (bi_persistently _)%I)
-          persistently_and_bare_sep_r bare_persistently_elim.
+          persistently_and_affinely_sep_r affinely_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=> ->. }
@@ -431,7 +431,7 @@ Proof. by constructor. Qed.
 (** * Adequacy *)
 Lemma tac_adequate P : (Envs Enil Enil ⊢ P) → P.
 Proof.
-  intros <-. rewrite /of_envs /= persistently_True_emp bare_persistently_emp left_id.
+  intros <-. rewrite /of_envs /= persistently_True_emp affinely_persistently_emp left_id.
   apply and_intro=> //. apply pure_intro; repeat constructor.
 Qed.
 
@@ -464,7 +464,7 @@ Lemma tac_assumption Δ Δ' i p P Q :
 Proof.
   intros ?? H. rewrite envs_lookup_delete_sound //.
   destruct (env_spatial_is_nil Δ') eqn:?.
-  - by rewrite (env_spatial_is_nil_bare_persistently Δ') // sep_elim_l.
+  - by rewrite (env_spatial_is_nil_affinely_persistently Δ') // sep_elim_l.
   - rewrite from_assumption. destruct H; by rewrite sep_elim_l.
 Qed.
 
@@ -497,7 +497,7 @@ Lemma tac_false_destruct Δ i p P Q :
   Δ ⊢ Q.
 Proof.
   intros ? ->. rewrite envs_lookup_sound //; simpl.
-  by rewrite bare_persistently_if_elim sep_elim_l False_elim.
+  by rewrite affinely_persistently_if_elim sep_elim_l False_elim.
 Qed.
 
 (** * Pure *)
@@ -511,13 +511,13 @@ Lemma tac_pure Δ Δ' i p P φ Q :
   (φ → Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros ?? HPQ HQ. rewrite envs_lookup_delete_sound //; simpl. destruct p; simpl.
-  - rewrite (into_pure P) -persistently_and_bare_sep_l persistently_pure.
+  - rewrite (into_pure P) -persistently_and_affinely_sep_l persistently_pure.
     by apply pure_elim_l.
   - destruct HPQ.
-    + rewrite -(affine_bare P) (into_pure P) -persistent_and_bare_sep_l.
+    + rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_l.
       by apply pure_elim_l.
-    + rewrite (into_pure P) (persistent_sink_bare ⌜ _ ⌝%I) sink_sep_lr.
-      rewrite -persistent_and_bare_sep_l. apply pure_elim_l=> ?. by rewrite HQ.
+    + rewrite (into_pure P) (persistent_absorbingly_affinely ⌜ _ ⌝%I) absorbingly_sep_lr.
+      rewrite -persistent_and_affinely_sep_l. apply pure_elim_l=> ?. by rewrite HQ.
 Qed.
 
 Lemma tac_pure_revert Δ φ Q : (Δ ⊢ ⌜φ⌝ → Q) → (φ → Δ ⊢ Q).
@@ -531,8 +531,8 @@ Lemma tac_persistently_intro Δ a p Q Q' :
 Proof.
   intros ? Haffine HQ. rewrite -(from_persistent a p Q') -HQ. destruct p=> /=.
   - rewrite envs_clear_spatial_sound.
-    rewrite {1}(env_spatial_is_nil_bare_persistently (envs_clear_spatial Δ)) //.
-    destruct a=> /=. by rewrite sep_elim_l. by rewrite bare_elim sep_elim_l.
+    rewrite {1}(env_spatial_is_nil_affinely_persistently (envs_clear_spatial Δ)) //.
+    destruct a=> /=. by rewrite sep_elim_l. by rewrite affinely_elim sep_elim_l.
   - destruct a=> //=. apply and_intro; auto using tac_emp_intro.
 Qed.
 
@@ -547,11 +547,11 @@ Proof.
   destruct p; simpl.
   - by rewrite -(into_persistent _ P) /= wand_elim_r.
   - destruct HPQ.
-    + rewrite -(affine_bare P) (_ : P = bi_persistently_if false P)%I //
+    + rewrite -(affine_affinely 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.
+      by rewrite {1}(persistent_absorbingly_affinely (bi_persistently _)%I)
+                 absorbingly_sep_l wand_elim_r HQ.
 Qed.
 
 (** * Implication and wand *)
@@ -562,16 +562,16 @@ Proof. intros. apply wand_elim_l'. eapply envs_app_singleton_sound. eauto. Qed.
 Lemma tac_impl_intro Δ Δ' i P P' Q :
   (if env_spatial_is_nil Δ then TCTrue else Persistent P) →
   envs_app false (Esnoc Enil i P') Δ = Some Δ' →
-  FromBare P' P →
+  FromAffinely P' P →
   (Δ' ⊢ Q) → Δ ⊢ P → Q.
 Proof.
   intros ??? <-. destruct (env_spatial_is_nil Δ) eqn:?.
-  - rewrite (env_spatial_is_nil_bare_persistently Δ) //; simpl. apply impl_intro_l.
+  - rewrite (env_spatial_is_nil_affinely_persistently Δ) //; simpl. apply impl_intro_l.
     rewrite envs_app_singleton_sound //; simpl.
-    rewrite -(from_bare P') -bare_and_lr.
-    by rewrite persistently_and_bare_sep_r bare_persistently_elim wand_elim_r.
+    rewrite -(from_affinely P') -affinely_and_lr.
+    by rewrite persistently_and_affinely_sep_r affinely_persistently_elim wand_elim_r.
   - apply impl_intro_l. rewrite envs_app_singleton_sound //; simpl.
-    by rewrite -(from_bare P') persistent_and_bare_sep_l_1 wand_elim_r.
+    by rewrite -(from_affinely P') persistent_and_affinely_sep_l_1 wand_elim_r.
 Qed.
 Lemma tac_impl_intro_persistent Δ Δ' i P P' Q :
   IntoPersistent false P P' →
@@ -580,7 +580,7 @@ Lemma tac_impl_intro_persistent Δ Δ' i P P' Q :
 Proof.
   intros ?? <-. rewrite envs_app_singleton_sound //; simpl. apply impl_intro_l.
   rewrite (_ : P = bi_persistently_if false P)%I // (into_persistent false P).
-  by rewrite persistently_and_bare_sep_l wand_elim_r.
+  by rewrite persistently_and_affinely_sep_l wand_elim_r.
 Qed.
 Lemma tac_pure_impl_intro Δ (φ ψ : Prop) :
   (φ → Δ ⊢ ⌜ψ⌝) → Δ ⊢ ⌜φ → ψ⌝.
@@ -606,11 +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 = bi_persistently_if false P)%I //
+  - rewrite -(affine_affinely 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 (bi_persistently _)%I) sink_sep_l
-               wand_elim_r HQ.
+    by rewrite {1}(persistent_absorbingly_affinely (bi_persistently _)%I)
+               absorbingly_sep_l wand_elim_r HQ.
 Qed.
 Lemma tac_wand_intro_pure Δ P φ Q :
   IntoPure P φ →
@@ -618,10 +618,10 @@ Lemma tac_wand_intro_pure Δ P φ Q :
   (φ → Δ ⊢ Q) → Δ ⊢ P -∗ Q.
 Proof.
   intros ? HPQ HQ. apply wand_intro_l. destruct HPQ.
-  - rewrite -(affine_bare P) (into_pure P) -persistent_and_bare_sep_l.
+  - rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_l.
     by apply pure_elim_l.
-  - rewrite (into_pure P) (persistent_sink_bare ⌜ _ ⌝%I) sink_sep_lr.
-    rewrite -persistent_and_bare_sep_l. apply pure_elim_l=> ?. by rewrite HQ.
+  - rewrite (into_pure P) (persistent_absorbingly_affinely ⌜ _ ⌝%I) absorbingly_sep_lr.
+    rewrite -persistent_and_affinely_sep_l. apply pure_elim_l=> ?. by rewrite HQ.
 Qed.
 Lemma tac_wand_intro_drop Δ P Q :
   TCOr (Affine P) (Absorbing Q) →
@@ -645,9 +645,9 @@ Proof.
   intros [? ->]%envs_lookup_delete_Some ??? <-. destruct p.
   - rewrite envs_lookup_persistent_sound //.
     rewrite envs_simple_replace_singleton_sound //; simpl.
-    rewrite -bare_persistently_if_idemp -bare_persistently_idemp into_wand /=.
-    rewrite assoc (bare_persistently_bare_persistently_if q).
-    by rewrite bare_persistently_if_sep_2 wand_elim_r wand_elim_r.
+    rewrite -affinely_persistently_if_idemp -affinely_persistently_idemp into_wand /=.
+    rewrite assoc (affinely_persistently_affinely_persistently_if q).
+    by rewrite affinely_persistently_if_sep_2 wand_elim_r wand_elim_r.
   - rewrite envs_lookup_sound //; simpl.
     rewrite envs_lookup_sound // (envs_replace_singleton_sound' _ Δ'') //; simpl.
     by rewrite into_wand /= assoc wand_elim_r wand_elim_r.
@@ -696,8 +696,8 @@ Lemma tac_specialize_assert_pure Δ Δ' j q R P1 P2 φ Q :
   φ → (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros. rewrite envs_simple_replace_singleton_sound //; simpl.
-  rewrite -bare_persistently_if_idemp into_wand /= -(from_pure P1).
-  rewrite pure_True // persistently_pure bare_True_emp bare_emp.
+  rewrite -affinely_persistently_if_idemp into_wand /= -(from_pure P1).
+  rewrite pure_True // persistently_pure affinely_True_emp affinely_emp.
   by rewrite emp_wand wand_elim_r.
 Qed.
 
@@ -705,7 +705,7 @@ Lemma tac_specialize_assert_persistent Δ Δ' Δ'' j q P1 P1' P2 R Q :
   envs_lookup_delete j Δ = Some (q, R, Δ') →
   IntoWand q true R P1 P2 →
   Persistent P1 →
-  IntoSink P1' P1 →
+  IntoAbsorbingly P1' P1 →
   envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'' →
   (Δ' ⊢ P1') → (Δ'' ⊢ Q) → Δ ⊢ Q.
 Proof.
@@ -713,11 +713,11 @@ Proof.
   rewrite envs_lookup_sound //.
   rewrite -(idemp bi_and (envs_delete _ _ _)).
   rewrite {2}envs_simple_replace_singleton_sound' //; simpl.
-  rewrite {1}HP1 (into_sink P1') (persistent_persistently_2 P1) sink_persistently.
-  rewrite persistently_and_bare_sep_l assoc.
-  rewrite -bare_persistently_if_idemp -bare_persistently_idemp.
-  rewrite (bare_persistently_bare_persistently_if q) bare_persistently_if_sep_2.
-  by rewrite into_wand wand_elim_l wand_elim_r.
+  rewrite {1}HP1 (into_absorbingly P1') (persistent_persistently_2 P1).
+  rewrite absorbingly_persistently persistently_and_affinely_sep_l assoc.
+  rewrite -affinely_persistently_if_idemp -affinely_persistently_idemp.
+  rewrite (affinely_persistently_affinely_persistently_if q).
+  by rewrite affinely_persistently_if_sep_2 into_wand wand_elim_l wand_elim_r.
 Qed.
 
 Lemma tac_specialize_persistent_helper Δ Δ'' j q P R R' Q :
@@ -731,9 +731,9 @@ Proof.
   intros ? HR ? Hpos ? <-. rewrite -(idemp bi_and Δ) {1}HR.
   rewrite envs_replace_singleton_sound //; destruct q; simpl.
   - 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.
+      absorbingly_persistently sep_elim_r persistently_and_affinely_sep_l wand_elim_r.
+  - by rewrite (absorbing_absorbingly R) (_ : R = bi_persistently_if false R)%I //
+       (into_persistent _ R) sep_elim_r persistently_and_affinely_sep_l wand_elim_r.
 Qed.
 
 Lemma tac_revert Δ Δ' i p P Q :
@@ -762,9 +762,9 @@ Lemma tac_revert_ih Δ P Q {φ : Prop} (Hφ : φ) :
   (of_envs Δ ⊢ Q).
 Proof.
   rewrite /IntoIH. intros HP ? HPQ.
-  rewrite (env_spatial_is_nil_bare_persistently Δ) //.
+  rewrite (env_spatial_is_nil_affinely_persistently Δ) //.
   rewrite -(idemp bi_and (□ Δ)%I) {1}HP // HPQ.
-  by rewrite -{1}persistently_idemp !bare_persistently_elim impl_elim_r.
+  by rewrite -{1}persistently_idemp !affinely_persistently_elim impl_elim_r.
 Qed.
 
 Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P P' Q :
@@ -780,25 +780,26 @@ Qed.
 Lemma tac_assert_persistent Δ Δ1 Δ2 Δ' lr js j P P' Q :
   envs_split lr js Δ = Some (Δ1,Δ2) →
   Persistent P →
-  FromBare P' P →
+  FromAffinely P' P →
   envs_app false (Esnoc Enil j P') Δ = Some Δ' →
   (Δ1 ⊢ P) → (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros ???? HP <-. rewrite -(idemp bi_and Δ) {1}envs_split_sound //.
   rewrite HP. rewrite (persistent_persistently_2 P) sep_elim_l.
-  rewrite persistently_and_bare_sep_l -bare_idemp bare_persistently_elim from_bare.
-  rewrite envs_app_singleton_sound //; simpl. by rewrite wand_elim_r.
+  rewrite persistently_and_affinely_sep_l -affinely_idemp.
+  rewrite affinely_persistently_elim from_affinely envs_app_singleton_sound //=.
+  by rewrite wand_elim_r.
 Qed.
 
 Lemma tac_assert_pure Δ Δ' j P P' φ Q :
   FromPure P φ →
-  FromBare P' P →
+  FromAffinely P' P →
   envs_app false (Esnoc Enil j P') Δ = Some Δ' →
   φ → (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros ???? <-. rewrite envs_app_singleton_sound //; simpl.
-  rewrite -(from_bare P') -(from_pure P) pure_True //.
-  by rewrite bare_True_emp bare_emp emp_wand.
+  rewrite -(from_affinely P') -(from_pure P) pure_True //.
+  by rewrite affinely_True_emp affinely_emp emp_wand.
 Qed.
 
 Lemma tac_pose_proof Δ Δ' j P Q :
@@ -807,7 +808,7 @@ Lemma tac_pose_proof Δ Δ' j P Q :
   (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros HP ? <-. rewrite envs_app_singleton_sound //; simpl.
-  by rewrite -HP bare_persistently_emp emp_wand.
+  by rewrite -HP affinely_persistently_emp emp_wand.
 Qed.
 
 Lemma tac_pose_proof_hyp Δ Δ' Δ'' i p j P Q :
@@ -842,7 +843,7 @@ Lemma tac_rewrite Δ i p Pxy (lr : bool) Q :
 Proof.
   intros ? A x y ? HPxy -> ?; apply internal_eq_rewrite'; auto.
   rewrite {1}envs_lookup_sound //.
-  rewrite HPxy bare_persistently_if_elim sep_elim_l.
+  rewrite HPxy affinely_persistently_if_elim sep_elim_l.
   destruct lr; auto using internal_eq_sym.
 Qed.
 
@@ -859,9 +860,9 @@ Proof.
   intros ?? A Δ' x y Φ HPxy HP ?? <-.
   rewrite -(idemp bi_and Δ) {2}(envs_lookup_sound _ i) //.
   rewrite (envs_simple_replace_singleton_sound _ _ j) //; simpl.
-  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.
+  rewrite HP HPxy (affinely_persistently_if_elim _ (_ ≡ _)%I) sep_elim_l.
+  rewrite persistent_and_affinely_sep_r -assoc. apply wand_elim_r'.
+  rewrite -persistent_and_affinely_sep_r. apply impl_elim_r'. destruct lr.
   - 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.
@@ -947,7 +948,8 @@ Lemma tac_frame_pure Δ (φ : Prop) P Q :
   φ → Frame true ⌜φ⌝ P Q → (Δ ⊢ Q) → Δ ⊢ P.
 Proof.
   intros ?? ->. rewrite -(frame ⌜φ⌝ P) /=.
-  rewrite -persistently_and_bare_sep_l persistently_pure. auto using and_intro, pure_intro.
+  rewrite -persistently_and_affinely_sep_l persistently_pure.
+  auto using and_intro, pure_intro.
 Qed.
 
 Lemma tac_frame Δ Δ' i p R P Q :
@@ -973,7 +975,7 @@ Lemma tac_or_destruct Δ Δ1 Δ2 i p j1 j2 P P1 P2 Q :
   (Δ1 ⊢ Q) → (Δ2 ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros ???? HP1 HP2. rewrite envs_lookup_sound //.
-  rewrite (into_or P) bare_persistently_if_or sep_or_r; apply or_elim.
+  rewrite (into_or P) affinely_persistently_if_or sep_or_r; apply or_elim.
   - rewrite (envs_simple_replace_singleton_sound' _ Δ1) //.
     by rewrite wand_elim_r.
   - rewrite (envs_simple_replace_singleton_sound' _ Δ2) //.
@@ -1014,7 +1016,7 @@ Lemma tac_exist_destruct {A} Δ i p j P (Φ : A → PROP) Q :
   Δ ⊢ Q.
 Proof.
   intros ?? HΦ. rewrite envs_lookup_sound //.
-  rewrite (into_exist P) bare_persistently_if_exist sep_exist_r.
+  rewrite (into_exist P) affinely_persistently_if_exist sep_exist_r.
   apply exist_elim=> a; destruct (HΦ a) as (Δ'&?&?).
   rewrite envs_simple_replace_singleton_sound' //; simpl. by rewrite wand_elim_r.
 Qed.
@@ -1030,7 +1032,7 @@ Lemma tac_modal_elim Δ Δ' i p P' P Q Q' :
   (Δ' ⊢ Q') → Δ ⊢ Q.
 Proof.
   intros ??? HΔ. rewrite envs_replace_singleton_sound //; simpl.
-  rewrite HΔ bare_persistently_if_elim. by apply elim_modal.
+  rewrite HΔ affinely_persistently_if_elim. by apply elim_modal.
 Qed.
 End bi_tactics.
 
@@ -1064,11 +1066,11 @@ Lemma into_laterN_env_sound n Δ1 Δ2 :
   IntoLaterNEnvs n Δ1 Δ2 → Δ1 ⊢ ▷^n (Δ2 : bi_car _).
 Proof.
   intros [Hp Hs]; rewrite /of_envs /= !laterN_and !laterN_sep.
-  rewrite -{1}laterN_intro -laterN_bare_persistently_2.
+  rewrite -{1}laterN_intro -laterN_affinely_persistently_2.
   apply and_mono, sep_mono.
   - apply pure_mono; destruct 1; constructor;
       naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
-  - apply bare_mono, persistently_mono.
+  - apply affinely_mono, persistently_mono.
     induction Hp; rewrite /= ?laterN_and. apply laterN_intro. by apply and_mono.
   - induction Hs; rewrite /= ?laterN_sep. apply laterN_intro. by apply sep_mono.
 Qed.
@@ -1082,11 +1084,11 @@ Lemma tac_löb Δ Δ' i Q :
   envs_app true (Esnoc Enil i (▷ Q)%I) Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
-  intros ?? HQ. rewrite (env_spatial_is_nil_bare_persistently Δ) //.
+  intros ?? HQ. rewrite (env_spatial_is_nil_affinely_persistently Δ) //.
   rewrite -(persistently_and_emp_elim Q). apply and_intro; first apply: affine.
   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.
+  rewrite persistently_and_affinely_sep_l -{1}affinely_persistently_idemp.
+  by rewrite affinely_persistently_sep_2 wand_elim_r affinely_elim.
 Qed.
 End sbi_tactics.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index a97e6ba1d3d41f6d3bf87720cb9611a3b41db7b1..7039f6ebc633743393189a8d3f5ae6be032c0802 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -1269,8 +1269,8 @@ Instance copy_destruct_impl {PROP : bi} (P Q : PROP) :
   CopyDestruct Q → CopyDestruct (P → Q).
 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 (bi_bare P).
+Instance copy_destruct_affinely {PROP : bi} (P : PROP) :
+  CopyDestruct P → CopyDestruct (bi_affinely P).
 Instance copy_destruct_persistently {PROP : bi} (P : PROP) :
   CopyDestruct P → CopyDestruct (bi_persistently P).
 
@@ -1771,7 +1771,7 @@ Hint Extern 1 (of_envs _ ⊢ _ ∧ _) => iSplit.
 Hint Extern 1 (of_envs _ ⊢ _ ∗ _) => iSplit.
 Hint Extern 1 (of_envs _ ⊢ ▷ _) => iNext.
 Hint Extern 1 (of_envs _ ⊢ bi_persistently _) => iAlways.
-Hint Extern 1 (of_envs _ ⊢ bi_bare _) => iAlways.
+Hint Extern 1 (of_envs _ ⊢ bi_affinely _) => 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 327767326caf59db56d50f95a5f42c12bf3fa3f0..f1feeb821c73892ce128f3e9b0314addbbd820a4 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -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 -∗ bi_bare (z ≡ y)) -∗ (P -∗ P ∧ (x,x) ≡ (y,x)).
+  □ (∀ z, P -∗ bi_affinely (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 -∗ bi_bare (P ∗ Q).
+  P ∧ emp -∗ emp ∧ Q -∗ bi_affinely (P ∗ Q).
 Proof. iIntros "[#? _] [_ #?]". auto. Qed.
 
 Lemma test_iIntros_persistent P Q `{!Persistent Q} : (P → Q → P ∧ Q)%I.
@@ -110,17 +110,18 @@ 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) :
-  φ → bi_bare ⌜y ≡ z⌝ -∗ (⌜ φ ⌝ ∧ ⌜ φ ⌝ ∧ y ≡ z : PROP).
+  φ → bi_affinely ⌜y ≡ z⌝ -∗ (⌜ φ ⌝ ∧ ⌜ φ ⌝ ∧ y ≡ z : PROP).
 Proof. iIntros (Hv) "#Hxy". iFrame (Hv) "Hxy". Qed.
 
 Lemma test_iAssert_modality P : ◇ False -∗ ▷ P.
 Proof.
   iIntros "HF".
-  iAssert (bi_bare False)%I with "[> -]" as %[].
+  iAssert (bi_affinely False)%I with "[> -]" as %[].
   by iMod "HF".
 Qed.
 
-Lemma test_iMod_bare_timeless P `{!Timeless P} : bi_bare (▷ P) -∗ ◇ bi_bare P.
+Lemma test_iMod_affinely_timeless P `{!Timeless P} :
+  bi_affinely (▷ P) -∗ ◇ bi_affinely P.
 Proof. iIntros "H". iMod "H". done. Qed.
 
 Lemma test_iAssumption_False P : False -∗ P.
@@ -220,7 +221,8 @@ 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 : bi_bare (▷ (Q ≡ P)) -∗ bi_bare (▷ Q) -∗ bi_bare (▷ P).
+Lemma test_foo P Q :
+  bi_affinely (▷ (Q ≡ P)) -∗ bi_affinely (▷ Q) -∗ bi_affinely (▷ P).
 Proof.
   iIntros "#HPQ HQ !#". iNext. by iRewrite "HPQ" in "HQ".
 Qed.
@@ -234,10 +236,10 @@ Proof.
 Qed.
 
 Lemma test_iNext_affine P Q :
-  bi_bare (▷ (Q ≡ P)) -∗ bi_bare (▷ Q) -∗ bi_bare (▷ P).
+  bi_affinely (▷ (Q ≡ P)) -∗ bi_affinely (▷ Q) -∗ bi_affinely (▷ P).
 Proof. iIntros "#HPQ HQ !#". iNext. by iRewrite "HPQ" in "HQ". Qed.
 
 Lemma test_iAlways P Q R :
-  □ P -∗ bi_persistently Q → R -∗ bi_persistently (bi_bare (bi_bare P)) ∗ □ Q.
+  □ P -∗ bi_persistently Q → R -∗ bi_persistently (bi_affinely (bi_affinely P)) ∗ □ Q.
 Proof. iIntros "#HP #HQ HR". iSplitL. iAlways. done. iAlways. done. Qed.
 End tests.