From f6040640d4651471e6ca705e598eff5e587e7987 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 3 Dec 2017 18:53:32 +0100
Subject: [PATCH] Remove notation for `bi_absorbingly`.

We do not have a notation for `bi_affinely` either, so this is at
least consistent.
---
 theories/bi/derived.v                | 67 +++++++++++++++-------------
 theories/proofmode/class_instances.v | 40 ++++++++---------
 theories/proofmode/classes.v         |  3 +-
 theories/proofmode/coq_tactics.v     |  2 +-
 4 files changed, 59 insertions(+), 53 deletions(-)

diff --git a/theories/bi/derived.v b/theories/bi/derived.v
index 49e209bb4..b19bd48e0 100644
--- a/theories/bi/derived.v
+++ b/theories/bi/derived.v
@@ -49,9 +49,8 @@ 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.
+Class Absorbing {PROP : bi} (P : PROP) := absorbing : bi_absorbingly P âŠ¢ P.
 Arguments Absorbing {_} _%I : simpl never.
 Arguments absorbing {_} _%I.
 
@@ -767,53 +766,57 @@ Global Instance absorbingly_flip_mono' :
   Proper (flip (âŠ¢) ==> flip (âŠ¢)) (@bi_absorbingly PROP).
 Proof. solve_proper. Qed.
 
-Lemma absorbingly_intro P : P âŠ¢ â–² P.
+Lemma absorbingly_intro P : P âŠ¢ bi_absorbingly P.
 Proof. by rewrite /bi_absorbingly -True_sep_2. Qed.
-Lemma absorbingly_mono P Q : (P âŠ¢ Q) â†’ â–² P âŠ¢ â–² Q.
+Lemma absorbingly_mono P Q : (P âŠ¢ Q) â†’ bi_absorbingly P âŠ¢ bi_absorbingly Q.
 Proof. by intros ->. Qed.
-Lemma absorbingly_idemp P : â–² â–² P âŠ£âŠ¢ â–² P.
+Lemma absorbingly_idemp P : bi_absorbingly (bi_absorbingly P) âŠ£âŠ¢ bi_absorbingly P.
 Proof.
   apply (anti_symm _), absorbingly_intro.
   rewrite /bi_absorbingly assoc. apply sep_mono; auto.
 Qed.
 
-Lemma absorbingly_pure Ï† : â–² âŒœ Ï† âŒ âŠ£âŠ¢ âŒœ Ï† âŒ.
+Lemma absorbingly_pure Ï† : bi_absorbingly âŒœ Ï† âŒ âŠ£âŠ¢ âŒœ Ï† âŒ.
 Proof.
   apply (anti_symm _), absorbingly_intro.
   apply wand_elim_r', pure_elim'=> ?. apply wand_intro_l; auto.
 Qed.
-Lemma absorbingly_or P Q : â–² (P âˆ¨ Q) âŠ£âŠ¢ â–² P âˆ¨ â–² Q.
+Lemma absorbingly_or P Q :
+  bi_absorbingly (P âˆ¨ Q) âŠ£âŠ¢ bi_absorbingly P âˆ¨ bi_absorbingly Q.
 Proof. by rewrite /bi_absorbingly sep_or_l. Qed.
-Lemma absorbingly_and P Q : â–² (P âˆ§ Q) âŠ¢ â–² P âˆ§ â–² Q.
+Lemma absorbingly_and P Q :
+  bi_absorbingly (P âˆ§ Q) âŠ¢ bi_absorbingly P âˆ§ bi_absorbingly Q.
 Proof. apply and_intro; apply absorbingly_mono; auto. Qed.
-Lemma absorbingly_forall {A} (Î¦ : A â†’ PROP) : â–² (âˆ€ a, Î¦ a) âŠ¢ âˆ€ a, â–² Î¦ a.
+Lemma absorbingly_forall {A} (Î¦ : A â†’ PROP) :
+  bi_absorbingly (âˆ€ a, Î¦ a) âŠ¢ âˆ€ a, bi_absorbingly (Î¦ a).
 Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed.
-Lemma absorbingly_exist {A} (Î¦ : A â†’ PROP) : â–² (âˆƒ a, Î¦ a) âŠ£âŠ¢ âˆƒ a, â–² Î¦ a.
+Lemma absorbingly_exist {A} (Î¦ : A â†’ PROP) :
+  bi_absorbingly (âˆƒ a, Î¦ a) âŠ£âŠ¢ âˆƒ a, bi_absorbingly (Î¦ a).
 Proof. by rewrite /bi_absorbingly sep_exist_l. Qed.
 
-Lemma absorbingly_internal_eq {A : ofeT} (x y : A) : â–² (x â‰¡ y) âŠ£âŠ¢ x â‰¡ y.
+Lemma absorbingly_internal_eq {A : ofeT} (x y : A) : bi_absorbingly (x â‰¡ y) âŠ£âŠ¢ x â‰¡ y.
 Proof.
   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 absorbingly_sep P Q : â–² (P âˆ— Q) âŠ£âŠ¢ â–² P âˆ— â–² Q.
+Lemma absorbingly_sep P Q : bi_absorbingly (P âˆ— Q) âŠ£âŠ¢ bi_absorbingly P âˆ— bi_absorbingly Q.
 Proof. by rewrite -{1}absorbingly_idemp /bi_absorbingly !assoc -!(comm _ P) !assoc. Qed.
-Lemma absorbingly_True_emp : â–² True âŠ£âŠ¢ â–² emp.
+Lemma absorbingly_True_emp : bi_absorbingly True âŠ£âŠ¢ bi_absorbingly emp.
 Proof. by rewrite absorbingly_pure /bi_absorbingly right_id. Qed.
-Lemma absorbingly_wand P Q : â–² (P -âˆ— Q) âŠ¢ â–² P -âˆ— â–² Q.
+Lemma absorbingly_wand P Q : bi_absorbingly (P -âˆ— Q) âŠ¢ bi_absorbingly P -âˆ— bi_absorbingly Q.
 Proof. apply wand_intro_l. by rewrite -absorbingly_sep wand_elim_r. Qed.
 
-Lemma absorbingly_sep_l P Q : â–² P âˆ— Q âŠ£âŠ¢ â–² (P âˆ— Q).
+Lemma absorbingly_sep_l P Q : bi_absorbingly P âˆ— Q âŠ£âŠ¢ bi_absorbingly (P âˆ— Q).
 Proof. by rewrite /bi_absorbingly assoc. Qed.
-Lemma absorbingly_sep_r P Q : P âˆ— â–² Q âŠ£âŠ¢ â–² (P âˆ— Q).
+Lemma absorbingly_sep_r P Q : P âˆ— bi_absorbingly Q âŠ£âŠ¢ bi_absorbingly (P âˆ— Q).
 Proof. by rewrite /bi_absorbingly !assoc (comm _ P). Qed.
-Lemma absorbingly_sep_lr P Q : â–² P âˆ— Q âŠ£âŠ¢ P âˆ— â–² Q.
+Lemma absorbingly_sep_lr P Q : bi_absorbingly P âˆ— Q âŠ£âŠ¢ P âˆ— bi_absorbingly Q.
 Proof. by rewrite absorbingly_sep_l absorbingly_sep_r. Qed.
 
 Lemma affinely_absorbingly `{!PositiveBI PROP} P :
-  bi_affinely (â–² P) âŠ£âŠ¢ bi_affinely P.
+  bi_affinely (bi_absorbingly P) âŠ£âŠ¢ bi_affinely P.
 Proof.
   apply (anti_symm _), affinely_mono, absorbingly_intro.
   by rewrite /bi_absorbingly affinely_sep affinely_True_emp affinely_emp left_id.
@@ -872,13 +875,13 @@ 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 absorbingly_wand !absorbing -absorbingly_intro. Qed.
 
-Global Instance absorbingly_absorbing P : Absorbing (â–² P).
+Global Instance absorbingly_absorbing P : Absorbing (bi_absorbingly P).
 Proof. rewrite /bi_absorbingly. apply _. Qed.
 
 (* Properties of affine and absorbing propositions *)
 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.
+Lemma absorbing_absorbingly P `{!Absorbing P} : bi_absorbingly P âŠ£âŠ¢ P.
 Proof. by apply (anti_symm _), absorbingly_intro. Qed.
 
 Lemma True_affine_all_affine P : Affine (True%I : PROP) â†’ Affine P.
@@ -965,7 +968,8 @@ Global Instance persistently_flip_mono' :
   Proper (flip (âŠ¢) ==> flip (âŠ¢)) (@bi_persistently PROP).
 Proof. intros P Q; apply persistently_mono. Qed.
 
-Lemma absorbingly_persistently P : â–² bi_persistently P âŠ£âŠ¢ bi_persistently P.
+Lemma absorbingly_persistently P :
+  bi_absorbingly (bi_persistently P) âŠ£âŠ¢ bi_persistently P.
 Proof.
   apply (anti_symm _), absorbingly_intro.
   by rewrite /bi_absorbingly comm persistently_absorbing.
@@ -987,7 +991,7 @@ 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_absorbingly P : bi_persistently P âŠ¢ â–² P.
+Lemma persistently_elim_absorbingly P : bi_persistently P âŠ¢ bi_absorbingly 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.
@@ -1171,7 +1175,7 @@ Global Instance plainly_flip_mono' :
   Proper (flip (âŠ¢) ==> flip (âŠ¢)) (@bi_plainly PROP).
 Proof. intros P Q; apply plainly_mono. Qed.
 
-Lemma absorbingly_plainly P : â–² bi_plainly P âŠ£âŠ¢ bi_plainly P.
+Lemma absorbingly_plainly P : bi_absorbingly (bi_plainly P) âŠ£âŠ¢ bi_plainly P.
 Proof.
   apply (anti_symm _), absorbingly_intro.
   by rewrite /bi_absorbingly comm plainly_absorbing.
@@ -1195,7 +1199,7 @@ Proof.
 Qed.
 Lemma plainly_and_emp_elim P : emp âˆ§ bi_plainly P âŠ¢ P.
 Proof. by rewrite plainly_elim_persistently persistently_and_emp_elim. Qed.
-Lemma plainly_elim_absorbingly P : bi_plainly P âŠ¢ â–² P.
+Lemma plainly_elim_absorbingly P : bi_plainly P âŠ¢ bi_absorbingly P.
 Proof. by rewrite plainly_elim_persistently persistently_elim_absorbingly. Qed.
 Lemma plainly_elim P `{!Absorbing P} : bi_plainly P âŠ¢ P.
 Proof. by rewrite plainly_elim_persistently persistently_elim. Qed.
@@ -1662,7 +1666,7 @@ Proof.
 Qed.
 Global Instance affinely_plain P : Plain P â†’ Plain (bi_affinely P).
 Proof. rewrite /bi_affinely. apply _. Qed.
-Global Instance absorbingly_plain P : Plain P â†’ Plain (â–² P).
+Global Instance absorbingly_plain P : Plain P â†’ Plain (bi_absorbingly P).
 Proof. rewrite /bi_absorbingly. apply _. Qed.
 Global Instance from_option_palin {A} P (Î¨ : A â†’ PROP) (mx : option A) :
   (âˆ€ x, Plain (Î¨ x)) â†’ Plain P â†’ Plain (from_option Î¨ P mx).
@@ -1742,7 +1746,7 @@ Global Instance persistently_persistent P : Persistent (bi_persistently P).
 Proof. by rewrite /Persistent persistently_idemp. 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).
+Global Instance absorbingly_persistent P : Persistent P â†’ Persistent (bi_absorbingly 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).
@@ -1796,7 +1800,8 @@ 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_absorbingly_affinely P `{!Persistent P} : P âŠ¢ â–² bi_affinely P.
+Lemma persistent_absorbingly_affinely P `{!Persistent P} :
+  P âŠ¢ bi_absorbingly (bi_affinely P).
 Proof.
   by rewrite {1}(persistent_persistently_2 P) -persistently_affinely
              persistently_elim_absorbingly.
@@ -2005,7 +2010,7 @@ Lemma later_affinely_plainly_if_2 p P : â– ?p â–· P âŠ¢ â–· â– ?p P.
 Proof. destruct p; simpl; auto using later_affinely_plainly_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.
+Lemma later_absorbingly P : â–· bi_absorbingly P âŠ£âŠ¢ bi_absorbingly (â–· P).
 Proof. by rewrite /bi_absorbingly later_sep later_True. Qed.
 
 Global Instance later_plain P : Plain P â†’ Plain (â–· P).
@@ -2080,7 +2085,7 @@ Lemma laterN_affinely_plainly_if_2 n p P : â– ?p â–·^n P âŠ¢ â–·^n â– ?p P.
 Proof. destruct p; simpl; auto using laterN_affinely_plainly_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.
+Lemma laterN_absorbingly n P : â–·^n (bi_absorbingly P) âŠ£âŠ¢ bi_absorbingly (â–·^n P).
 Proof. by rewrite /bi_absorbingly laterN_sep laterN_True. Qed.
 
 Global Instance laterN_plain n P : Plain P â†’ Plain (â–·^n P).
@@ -2163,7 +2168,7 @@ Lemma except_0_affinely_plainly_if_2 p P : â– ?p â—‡ P âŠ¢ â—‡ â– ?p P.
 Proof. destruct p; simpl; auto using except_0_affinely_plainly_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.
+Lemma except_0_absorbingly P : â—‡ (bi_absorbingly P) âŠ£âŠ¢ bi_absorbingly (â—‡ P).
 Proof. by rewrite /bi_absorbingly except_0_sep except_0_True. Qed.
 
 Lemma except_0_frame_l P Q : P âˆ— â—‡ Q âŠ¢ â—‡ (P âˆ— Q).
@@ -2250,7 +2255,7 @@ 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).
+Global Instance absorbingly_timeless P : Timeless P â†’ Timeless (bi_absorbingly P).
 Proof. rewrite /bi_absorbingly; apply _. Qed.
 
 Global Instance eq_timeless {A : ofeT} (a b : A) :
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 90f3c2737..035f37995 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -18,7 +18,7 @@ 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.
+Global Instance into_absorbingly_default P : IntoAbsorbingly (bi_absorbingly P) P | 100.
 Proof. by rewrite /IntoAbsorbingly. Qed.
 
 (* FromAssumption *)
@@ -35,7 +35,7 @@ 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).
+  FromAssumption p P Q â†’ FromAssumption p P (bi_absorbingly Q).
 Proof. rewrite /FromAssumption /= =><-. apply absorbingly_intro. Qed.
 
 Global Instance from_assumption_affinely_plainly_l p P Q :
@@ -108,7 +108,7 @@ Proof. rewrite /FromPure /IntoPure=> <- ->. by rewrite pure_impl impl_wand_2. Qe
 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) Ï†.
+Global Instance into_pure_absorbingly P Ï† : IntoPure P Ï† â†’ IntoPure (bi_absorbingly P) Ï†.
 Proof. rewrite /IntoPure=> ->. by rewrite absorbingly_pure. Qed.
 Global Instance into_pure_plainly P Ï† : IntoPure P Ï† â†’ IntoPure (bi_plainly P) Ï†.
 Proof. rewrite /IntoPure=> ->. apply: plainly_elim. Qed.
@@ -159,7 +159,7 @@ Proof. rewrite /FromPure=> <-. by rewrite persistently_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) Ï†.
+Global Instance from_pure_absorbingly P Ï† : FromPure P Ï† â†’ FromPure (bi_absorbingly P) Ï†.
 Proof. rewrite /FromPure=> <-. by rewrite absorbingly_pure. Qed.
 
 (* IntoInternalEq *)
@@ -170,7 +170,7 @@ 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.
+  IntoInternalEq P x y â†’ IntoInternalEq (bi_absorbingly P) x y.
 Proof. rewrite /IntoInternalEq=> ->. by rewrite absorbingly_internal_eq. Qed.
 Global Instance into_internal_eq_plainly {A : ofeT} (x y : A) P :
   IntoInternalEq P x y â†’ IntoInternalEq (bi_plainly P) x y.
@@ -353,7 +353,7 @@ 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).
+  FromSep P Q1 Q2 â†’ FromSep (bi_absorbingly P) (bi_absorbingly Q1) (bi_absorbingly Q2).
 Proof. rewrite /FromSep=> <-. by rewrite absorbingly_sep. Qed.
 Global Instance from_sep_plainly P Q1 Q2 :
   FromSep P Q1 Q2 â†’
@@ -491,7 +491,7 @@ 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).
+  FromOr P Q1 Q2 â†’ FromOr (bi_absorbingly P) (bi_absorbingly Q1) (bi_absorbingly Q2).
 Proof. rewrite /FromOr=> <-. by rewrite absorbingly_or. Qed.
 Global Instance from_or_plainly P Q1 Q2 :
   FromOr P Q1 Q2 â†’ FromOr (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
@@ -510,7 +510,7 @@ 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).
+  IntoOr P Q1 Q2 â†’ IntoOr (bi_absorbingly P) (bi_absorbingly Q1) (bi_absorbingly Q2).
 Proof. rewrite /IntoOr=>->. by rewrite absorbingly_or. Qed.
 Global Instance into_or_plainly P Q1 Q2 :
   IntoOr P Q1 Q2 â†’ IntoOr (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
@@ -530,7 +530,7 @@ 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.
+  FromExist P Î¦ â†’ FromExist (bi_absorbingly P) (Î» a, bi_absorbingly (Î¦ a))%I.
 Proof. rewrite /FromExist=> <-. by rewrite absorbingly_exist. Qed.
 Global Instance from_exist_plainly {A} P (Î¦ : A â†’ PROP) :
   FromExist P Î¦ â†’ FromExist (bi_plainly P) (Î» a, bi_plainly (Î¦ a))%I.
@@ -562,7 +562,7 @@ Proof.
   rewrite -exist_intro //. apply sep_elim_r, _.
 Qed.
 Global Instance into_exist_absorbingly {A} P (Î¦ : A â†’ PROP) :
-  IntoExist P Î¦ â†’ IntoExist (â–² P) (Î» a, â–² (Î¦ a))%I.
+  IntoExist P Î¦ â†’ IntoExist (bi_absorbingly P) (Î» a, bi_absorbingly (Î¦ a))%I.
 Proof. rewrite /IntoExist=> HP. by rewrite HP absorbingly_exist. Qed.
 Global Instance into_exist_plainly {A} P (Î¦ : A â†’ PROP) :
   IntoExist P Î¦ â†’ IntoExist (bi_plainly P) (Î» a, bi_plainly (Î¦ a))%I.
@@ -633,7 +633,7 @@ 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_absorbingly P Q : Absorbing Q â†’ ElimModal (â–² P) P Q Q.
+Global Instance elim_modal_absorbingly P Q : Absorbing Q â†’ ElimModal (bi_absorbingly P) P Q Q.
 Proof.
   rewrite /ElimModal=> H. by rewrite absorbingly_sep_l wand_elim_r absorbing_absorbingly.
 Qed.
@@ -666,11 +666,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_absorbingly P : MakeSep True P (â–² P) | 10.
+Global Instance make_and_emp_l_absorbingly P : MakeSep True P (bi_absorbingly 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_absorbingly P : MakeSep P True (â–² P) | 10.
+Global Instance make_and_emp_r_absorbingly P : MakeSep P True (bi_absorbingly 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.
@@ -794,18 +794,18 @@ Proof.
   by rewrite -{1}affinely_idemp affinely_sep_2.
 Qed.
 
-Class MakeAbsorbingly (P Q : PROP) := make_absorbingly : â–² P âŠ£âŠ¢ Q.
+Class MakeAbsorbingly (P Q : PROP) := make_absorbingly : bi_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_absorbingly_default P : MakeAbsorbingly P (â–² P) | 100.
+Global Instance make_absorbingly_default P : MakeAbsorbingly P (bi_absorbingly P) | 100.
 Proof. by rewrite /MakeAbsorbingly. Qed.
 
 Global Instance frame_absorbingly p R P Q Q' :
-  Frame p R P Q â†’ MakeAbsorbingly Q Q' â†’ Frame p R (â–² P) Q'.
+  Frame p R P Q â†’ MakeAbsorbingly Q Q' â†’ Frame p R (bi_absorbingly P) Q'.
 Proof. rewrite /Frame /MakeAbsorbingly=> <- <- /=. by rewrite absorbingly_sep_r. Qed.
 
 Class MakePersistently (P Q : PROP) := make_persistently : bi_persistently P âŠ£âŠ¢ Q.
@@ -834,7 +834,7 @@ 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_absorbingly P : FromModal (â–² P) P.
+Global Instance from_modal_absorbingly P : FromModal (bi_absorbingly P) P.
 Proof. apply absorbingly_intro. Qed.
 End bi_instances.
 
@@ -1049,7 +1049,7 @@ Global Instance into_except_0_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_except_0_absorbingly P Q :
-  IntoExcept0 P Q â†’ IntoExcept0 (â–² P) (â–² Q).
+  IntoExcept0 P Q â†’ IntoExcept0 (bi_absorbingly P) (bi_absorbingly Q).
 Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_absorbingly. Qed.
 Global Instance into_except_0_plainly P Q :
   IntoExcept0 P Q â†’ IntoExcept0 (bi_plainly P) (bi_plainly Q).
@@ -1155,7 +1155,7 @@ 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).
+  IntoLaterN n P Q â†’ IntoLaterN n (bi_absorbingly P) (bi_absorbingly Q).
 Proof. rewrite /IntoLaterN=> ->. by rewrite laterN_absorbingly. Qed.
 Global Instance into_later_plainly n P Q :
   IntoLaterN n P Q â†’ IntoLaterN n (bi_plainly P) (bi_plainly Q).
@@ -1244,7 +1244,7 @@ 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_absorbingly n P Q :
-  FromLaterN n P Q â†’ FromLaterN n (â–² P) (â–² Q).
+  FromLaterN n P Q â†’ FromLaterN n (bi_absorbingly P) (bi_absorbingly Q).
 Proof. by rewrite /FromLaterN laterN_absorbingly=> ->. Qed.
 
 Global Instance from_later_forall {A} n (Î¦ Î¨ : A â†’ PROP) :
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 8f959e4e1..25b8d6990 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -74,7 +74,8 @@ 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.
+Class IntoAbsorbingly {PROP : bi} (P Q : PROP) :=
+  into_absorbingly : P âŠ¢ bi_absorbingly Q.
 Arguments IntoAbsorbingly {_} _%I _%I.
 Arguments into_absorbingly {_} _%I _%I {_}.
 Hint Mode IntoAbsorbingly + ! -  : typeclass_instances.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index bfddbb9a4..08708214e 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -798,7 +798,7 @@ Qed.
 
 Lemma tac_specialize_persistent_helper Î” Î”'' j q P R R' Q :
   envs_lookup j Î” = Some (q,P) â†’
-  envs_entails Î” (â–² R) â†’
+  envs_entails Î” (bi_absorbingly R) â†’
   IntoPersistent false R R' â†’
   (if q then TCTrue else AffineBI PROP) â†’
   envs_replace j q true (Esnoc Enil j R') Î” = Some Î”'' â†’
-- 
GitLab