diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 15bf8ab76e12c994f29a6121adb40b1e3421c2cd..477105c84aa61c7e293ebb5250780fe555f0f606 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -89,7 +89,7 @@ Section sep_list.
     Proper (Forall2 (⊢) ==> (⊢)) (big_opL (@bi_sep M) (λ _ P, P)).
   Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
 
-  Lemma big_sepL_emp l : ([∗ list] k↦y ∈ l, emp) ⊣⊢ (emp : PROP).
+  Lemma big_sepL_emp l : ([∗ list] k↦y ∈ l, emp) ⊣⊢@{PROP} emp.
   Proof. by rewrite big_opL_unit. Qed.
 
   Lemma big_sepL_lookup_acc Φ l i x :
diff --git a/theories/bi/derived_laws_bi.v b/theories/bi/derived_laws_bi.v
index d9ed36cb0e1e092c593b06f6879c5d4585877ef6..0143774a780fe4062f5c425254d7027085597568 100644
--- a/theories/bi/derived_laws_bi.v
+++ b/theories/bi/derived_laws_bi.v
@@ -21,8 +21,8 @@ Implicit Types A : Type.
 Hint Extern 100 (NonExpansive _) => solve_proper.
 
 (* Force implicit argument PROP *)
-Notation "P ⊢ Q" := (@bi_entails PROP P%I Q%I).
-Notation "P ⊣⊢ Q" := (equiv (A:=bi_car PROP) P%I Q%I).
+Notation "P ⊢ Q" := (P ⊢@{PROP} Q).
+Notation "P ⊣⊢ Q" := (P ⊣⊢@{PROP} Q).
 
 (* Derived stuff about the entailment *)
 Global Instance entails_anti_sym : AntiSymm (⊣⊢) (@bi_entails PROP).
@@ -629,9 +629,9 @@ Proof. rewrite /bi_affinely. apply (anti_symm _); auto. Qed.
 Lemma absorbing_absorbingly P `{!Absorbing P} : <absorb> P ⊣⊢ P.
 Proof. by apply (anti_symm _), absorbingly_intro. Qed.
 
-Lemma True_affine_all_affine P : Affine (True%I : PROP) → Affine P.
+Lemma True_affine_all_affine P : Affine (PROP:=PROP) True → Affine P.
 Proof. rewrite /Affine=> <-; auto. Qed.
-Lemma emp_absorbing_all_absorbing P : Absorbing (emp%I : PROP) → Absorbing P.
+Lemma emp_absorbing_all_absorbing P : Absorbing (PROP:=PROP) emp → Absorbing P.
 Proof.
   intros. rewrite /Absorbing -{2}(left_id emp%I _ P).
   by rewrite -(absorbing emp) absorbingly_sep_l left_id.
@@ -1257,7 +1257,7 @@ Section persistent_bi_absorbing.
 End persistent_bi_absorbing.
 
 (* Affine instances *)
-Global Instance emp_affine_l : Affine (emp%I : PROP).
+Global Instance emp_affine_l : Affine (PROP:=PROP) emp.
 Proof. by rewrite /Affine. Qed.
 Global Instance and_affine_l P Q : Affine P → Affine (P ∧ Q).
 Proof. rewrite /Affine=> ->; auto. Qed.
@@ -1280,7 +1280,7 @@ Global Instance intuitionistically_affine P : Affine (â–¡ P).
 Proof. rewrite /bi_intuitionistically. apply _. Qed.
 
 (* Absorbing instances *)
-Global Instance pure_absorbing φ : Absorbing (⌜φ⌝%I : PROP).
+Global Instance pure_absorbing φ : Absorbing (PROP:=PROP) ⌜φ⌝.
 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 absorbingly_and_1 !absorbing. Qed.
@@ -1324,9 +1324,9 @@ Global Instance persistently_if_absorbing P p :
 Proof. intros; destruct p; simpl; apply _. Qed.
 
 (* Persistence instances *)
-Global Instance pure_persistent φ : Persistent (⌜φ⌝%I : PROP).
+Global Instance pure_persistent φ : Persistent (PROP:=PROP) ⌜φ⌝.
 Proof. by rewrite /Persistent persistently_pure. Qed.
-Global Instance emp_persistent : Persistent (emp%I : PROP).
+Global Instance emp_persistent : Persistent (PROP:=PROP) emp.
 Proof. rewrite /Persistent. apply persistently_emp_intro. Qed.
 Global Instance and_persistent P Q :
   Persistent P → Persistent Q → Persistent (P ∧ Q).
diff --git a/theories/bi/derived_laws_sbi.v b/theories/bi/derived_laws_sbi.v
index db012d4bcff9a35a262f4685b2a97641733d8281..147a2f7397a2f27020d323b553c3a675d13c27ed 100644
--- a/theories/bi/derived_laws_sbi.v
+++ b/theories/bi/derived_laws_sbi.v
@@ -13,8 +13,8 @@ Implicit Types Ps : list PROP.
 Implicit Types A : Type.
 
 (* Force implicit argument PROP *)
-Notation "P ⊢ Q" := (@bi_entails PROP P%I Q%I).
-Notation "P ⊣⊢ Q" := (equiv (A:=bi_car PROP) P%I Q%I).
+Notation "P ⊢ Q" := (P ⊢@{PROP} Q).
+Notation "P ⊣⊢ Q" := (P ⊣⊢@{PROP} Q).
 
 Hint Resolve or_elim or_intro_l' or_intro_r' True_intro False_elim.
 Hint Resolve and_elim_l' and_elim_r' and_intro forall_intro.
@@ -127,10 +127,10 @@ Proof.
 Qed.
 
 Global Instance internal_eq_absorbing {A : ofeT} (x y : A) :
-  Absorbing (x ≡ y : PROP)%I.
+  Absorbing (PROP:=PROP) (x ≡ y).
 Proof. by rewrite /Absorbing absorbingly_internal_eq. Qed.
 Global Instance internal_eq_persistent {A : ofeT} (a b : A) :
-  Persistent (a ≡ b : PROP)%I.
+  Persistent (PROP:=PROP) (a ≡ b).
 Proof. by intros; rewrite /Persistent persistently_internal_eq. Qed.
 
 (* Equality under a later. *)
@@ -351,7 +351,7 @@ Proof. by rewrite {1}(except_0_intro P) except_0_sep. Qed.
 Lemma except_0_frame_r P Q : ◇ P ∗ Q ⊢ ◇ (P ∗ Q).
 Proof. by rewrite {1}(except_0_intro Q) except_0_sep. Qed.
 
-Lemma later_affinely_1 `{!Timeless (emp%I : PROP)} P : ▷ <affine> P ⊢ ◇ <affine> ▷ P.
+Lemma later_affinely_1 `{!Timeless (PROP:=PROP) emp} P : ▷ <affine> P ⊢ ◇ <affine> ▷ P.
 Proof.
   rewrite /bi_affinely later_and (timeless emp%I) except_0_and.
   by apply and_mono, except_0_intro.
@@ -366,12 +366,12 @@ Proof. rewrite /sbi_except_0; apply _. Qed.
 Global Instance Timeless_proper : Proper ((≡) ==> iff) (@Timeless PROP).
 Proof. solve_proper. Qed.
 
-Global Instance pure_timeless φ : Timeless (⌜φ⌝ : PROP)%I.
+Global Instance pure_timeless φ : Timeless (PROP:=PROP) ⌜φ⌝.
 Proof.
   rewrite /Timeless /sbi_except_0 pure_alt later_exist_false.
   apply or_elim, exist_elim; [auto|]=> Hφ. rewrite -(exist_intro Hφ). auto.
 Qed.
-Global Instance emp_timeless `{BiAffine PROP} : Timeless (emp : PROP)%I.
+Global Instance emp_timeless `{BiAffine PROP} : Timeless (PROP:=PROP) emp.
 Proof. rewrite -True_emp. apply _. Qed.
 
 Global Instance and_timeless P Q : Timeless P → Timeless Q → Timeless (P ∧ Q).
@@ -420,13 +420,13 @@ Proof.
 Qed.
 
 Global Instance affinely_timeless P :
-  Timeless (emp%I : PROP) → Timeless P → Timeless (<affine> P).
+  Timeless (PROP:=PROP) emp → Timeless P → Timeless (<affine> P).
 Proof. rewrite /bi_affinely; apply _. Qed.
 Global Instance absorbingly_timeless P : Timeless P → Timeless (<absorb> P).
 Proof. rewrite /bi_absorbingly; apply _. Qed.
 
 Global Instance eq_timeless {A : ofeT} (a b : A) :
-  Discrete a → Timeless (a ≡ b : PROP)%I.
+  Discrete a → Timeless (PROP:=PROP) (a ≡ b).
 Proof. intros. rewrite /Discrete !discrete_eq. apply (timeless _). Qed.
 Global Instance from_option_timeless {A} P (Ψ : A → PROP) (mx : option A) :
   (∀ x, Timeless (Ψ x)) → Timeless P → Timeless (from_option Ψ P mx).
diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index 90453b0e6571d12706cba8f8ea4d3aa5f8544163..ee071f187b83628a4e13ce37317cab77b646368f 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -36,21 +36,21 @@ Arguments bi_embed_embed : simpl never.
 Class SbiEmbed (PROP1 PROP2 : sbi) `{BiEmbed PROP1 PROP2} := {
   embed_internal_eq_1 (A : ofeT) (x y : A) : ⎡x ≡ y⎤ ⊢ x ≡ y;
   embed_later P : ⎡▷ P⎤ ⊣⊢ ▷ ⎡P⎤;
-  embed_interal_inj (PROP' : sbi) (P Q : PROP1) : ⎡P⎤ ≡ ⎡Q⎤ ⊢ (P ≡ Q : PROP');
+  embed_interal_inj (PROP' : sbi) (P Q : PROP1) : ⎡P⎤ ≡ ⎡Q⎤ ⊢@{PROP'} (P ≡ Q);
 }.
 Hint Mode SbiEmbed ! - - : typeclass_instances.
 Hint Mode SbiEmbed - ! - : typeclass_instances.
 
 Class BiEmbedBUpd (PROP1 PROP2 : bi)
       `{BiEmbed PROP1 PROP2, BiBUpd PROP1, BiBUpd PROP2} := {
-  embed_bupd  P : ⎡|==> P⎤ ⊣⊢ bupd (PROP:=PROP2) ⎡P⎤
+  embed_bupd  P : ⎡|==> P⎤ ⊣⊢@{PROP2} |==> ⎡P⎤
 }.
 Hint Mode BiEmbedBUpd - ! - - - : typeclass_instances.
 Hint Mode BiEmbedBUpd ! - - - - : typeclass_instances.
 
 Class BiEmbedFUpd (PROP1 PROP2 : sbi)
       `{BiEmbed PROP1 PROP2, BiFUpd PROP1, BiFUpd PROP2} := {
-  embed_fupd E1 E2 P : ⎡|={E1,E2}=> P⎤ ⊣⊢ fupd (PROP:=PROP2) E1 E2 ⎡P⎤
+  embed_fupd E1 E2 P : ⎡|={E1,E2}=> P⎤ ⊣⊢@{PROP2} |={E1,E2}=> ⎡P⎤
 }.
 Hint Mode BiEmbedFUpd - ! - - - : typeclass_instances.
 Hint Mode BiEmbedFUpd ! - - - - : typeclass_instances.
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 178fe6717abd66e0959dc5eeff148325555467c5..b90fdfd99dd4835864b8968ca058b45a277574f2 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -2,6 +2,11 @@ From iris.algebra Require Export ofe.
 Set Primitive Projections.
 
 Reserved Notation "P ⊢ Q" (at level 99, Q at level 200, right associativity).
+Reserved Notation "P '⊢@{' PROP } Q" (at level 99, Q at level 200, right associativity).
+Reserved Notation "('⊢@{' PROP } )" (at level 99).
+Reserved Notation "P ⊣⊢ Q" (at level 95, no associativity).
+Reserved Notation "P '⊣⊢@{' PROP } Q" (at level 95, no associativity).
+Reserved Notation "('⊣⊢@{' PROP } )" (at level 95).
 Reserved Notation "'emp'".
 Reserved Notation "'⌜' φ '⌝'" (at level 1, φ at level 200, format "⌜ φ ⌝").
 Reserved Notation "P ∗ Q" (at level 80, right associativity).
@@ -265,11 +270,14 @@ Instance bi_rewrite_relation (PROP : bi) : RewriteRelation (@bi_entails PROP).
 Instance bi_inhabited {PROP : bi} : Inhabited PROP := populate (bi_pure True).
 
 Notation "P ⊢ Q" := (bi_entails P%I Q%I) : stdpp_scope.
+Notation "P ⊢@{ PROP } Q" := (bi_entails (PROP:=PROP) P%I Q%I) (only parsing) : stdpp_scope.
 Notation "(⊢)" := bi_entails (only parsing) : stdpp_scope.
+Notation "(⊢@{ PROP } )" := (bi_entails (PROP:=PROP)) (only parsing) : stdpp_scope.
 
-Notation "P ⊣⊢ Q" := (equiv (A:=bi_car _) P%I Q%I)
-  (at level 95, no associativity) : stdpp_scope.
+Notation "P ⊣⊢ Q" := (equiv (A:=bi_car _) P%I Q%I) : stdpp_scope.
+Notation "P ⊣⊢@{ PROP } Q" := (equiv (A:=bi_car PROP) P%I Q%I) (only parsing) : stdpp_scope.
 Notation "(⊣⊢)" := (equiv (A:=bi_car _)) (only parsing) : stdpp_scope.
+Notation "(⊣⊢@{ PROP } )" := (equiv (A:=bi_car PROP)) (only parsing) : stdpp_scope.
 
 Notation "P -∗ Q" := (P ⊢ Q) : stdpp_scope.
 
@@ -340,7 +348,7 @@ Lemma pure_intro P (φ : Prop) : φ → P ⊢ ⌜ φ ⌝.
 Proof. eapply bi_mixin_pure_intro, bi_bi_mixin. Qed.
 Lemma pure_elim' (φ : Prop) P : (φ → True ⊢ P) → ⌜ φ ⌝ ⊢ P.
 Proof. eapply bi_mixin_pure_elim', bi_bi_mixin. Qed.
-Lemma pure_forall_2 {A} (φ : A → Prop) : (∀ a, ⌜ φ a ⌝ : PROP) ⊢ ⌜ ∀ a, φ a ⌝.
+Lemma pure_forall_2 {A} (φ : A → Prop) : (∀ a, ⌜ φ a ⌝) ⊢@{PROP} ⌜ ∀ a, φ a ⌝.
 Proof. eapply bi_mixin_pure_forall_2, bi_bi_mixin. Qed.
 
 Lemma and_elim_l P Q : P ∧ Q ⊢ P.
@@ -394,7 +402,7 @@ Proof. eapply bi_mixin_persistently_mono, bi_bi_mixin. Qed.
 Lemma persistently_idemp_2 P : <pers> P ⊢ <pers> <pers> P.
 Proof. eapply bi_mixin_persistently_idemp_2, bi_bi_mixin. Qed.
 
-Lemma persistently_emp_2 : (emp : PROP) ⊢ <pers> emp.
+Lemma persistently_emp_2 : emp ⊢@{PROP} <pers> emp.
 Proof. eapply bi_mixin_persistently_emp_2, bi_bi_mixin. Qed.
 
 Lemma persistently_forall_2 {A} (Ψ : A → PROP) :
@@ -425,21 +433,23 @@ Lemma internal_eq_rewrite {A : ofeT} a b (Ψ : A → PROP) :
   NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b.
 Proof. eapply sbi_mixin_internal_eq_rewrite, sbi_sbi_mixin. Qed.
 
-Lemma fun_ext {A} {B : A → ofeT} (f g : ofe_fun B) : (∀ x, f x ≡ g x) ⊢ (f ≡ g : PROP).
+Lemma fun_ext {A} {B : A → ofeT} (f g : ofe_fun B) :
+  (∀ x, f x ≡ g x) ⊢@{PROP} f ≡ g.
 Proof. eapply sbi_mixin_fun_ext, sbi_sbi_mixin. Qed.
-Lemma sig_eq {A : ofeT} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊢ (x ≡ y : PROP).
+Lemma sig_eq {A : ofeT} (P : A → Prop) (x y : sig P) :
+  `x ≡ `y ⊢@{PROP} x ≡ y.
 Proof. eapply sbi_mixin_sig_eq, sbi_sbi_mixin. Qed.
 Lemma discrete_eq_1 {A : ofeT} (a b : A) :
-  Discrete a → a ≡ b ⊢ (⌜a ≡ b⌝ : PROP).
+  Discrete a → a ≡ b ⊢@{PROP} ⌜a ≡ b⌝.
 Proof. eapply sbi_mixin_discrete_eq_1, sbi_sbi_mixin. Qed.
 
 (* Later *)
 Global Instance later_contractive : Contractive (@sbi_later PROP).
 Proof. eapply sbi_mixin_later_contractive, sbi_sbi_mixin. Qed.
 
-Lemma later_eq_1 {A : ofeT} (x y : A) : Next x ≡ Next y ⊢ ▷ (x ≡ y : PROP).
+Lemma later_eq_1 {A : ofeT} (x y : A) : Next x ≡ Next y ⊢@{PROP} ▷ (x ≡ y).
 Proof. eapply sbi_mixin_later_eq_1, sbi_sbi_mixin. Qed.
-Lemma later_eq_2 {A : ofeT} (x y : A) : ▷ (x ≡ y) ⊢ (Next x ≡ Next y : PROP).
+Lemma later_eq_2 {A : ofeT} (x y : A) : ▷ (x ≡ y) ⊢@{PROP} Next x ≡ Next y.
 Proof. eapply sbi_mixin_later_eq_2, sbi_sbi_mixin. Qed.
 
 Lemma later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q.
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index d24572362542790c383acd6a663f4cfeeca35c4d..4de962442ec86acc4008d9eba0aefe813c745153 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -823,7 +823,7 @@ Lemma monPred_at_except_0 i P : (◇ P) i ⊣⊢ ◇ P i.
 Proof. by unseal. Qed.
 
 Lemma monPred_equivI {PROP' : sbi} P Q :
-  sbi_internal_eq (PROP:=PROP') P Q ⊣⊢ ∀ i, P i ≡ Q i.
+  P ≡ Q ⊣⊢@{PROP'} ∀ i, P i ≡ Q i.
 Proof.
   apply bi.equiv_spec. split.
   - apply bi.forall_intro=>?. apply (bi.f_equiv (flip monPred_at _)).
diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v
index dc97f4e88fe96777f6a09b16649ec326076ff089..7f15fee347ba612055377ed20a23602d1074e986 100644
--- a/theories/bi/plainly.v
+++ b/theories/bi/plainly.v
@@ -161,7 +161,7 @@ Proof. apply (anti_symm _); auto using plainly_idemp_1, plainly_idemp_2. Qed.
 Lemma plainly_intro' P Q : (■ P ⊢ Q) → ■ P ⊢ ■ Q.
 Proof. intros <-. apply plainly_idemp_2. Qed.
 
-Lemma plainly_pure φ : ■ ⌜φ⌝ ⊣⊢ bi_pure (PROP:=PROP) φ.
+Lemma plainly_pure φ : ■ ⌜φ⌝ ⊣⊢@{PROP} ⌜φ⌝.
 Proof.
   apply (anti_symm _); auto.
   - by rewrite plainly_elim_persistently persistently_pure.
@@ -204,7 +204,7 @@ Proof. by rewrite -{1}(left_id emp%I _ Q%I) plainly_and_sep_assoc and_elim_l. Qe
 Lemma plainly_and_sep_r_1 P Q : P ∧ ■ Q ⊢ P ∗ ■ Q.
 Proof. by rewrite !(comm _ P) plainly_and_sep_l_1. Qed.
 
-Lemma plainly_True_emp : ■ True ⊣⊢ ■ (@bi_emp PROP).
+Lemma plainly_True_emp : ■ True ⊣⊢@{PROP} ■ emp.
 Proof. apply (anti_symm _); eauto using plainly_mono, plainly_emp_intro. Qed.
 Lemma plainly_and_sep P Q : ■ (P ∧ Q) ⊢ ■ (P ∗ Q).
 Proof.
@@ -273,7 +273,7 @@ Proof. rewrite -!impl_wand_affinely_plainly. apply plainly_impl_plainly. Qed.
 Section plainly_affine_bi.
   Context `{BiAffine PROP}.
 
-  Lemma plainly_emp : ■ emp ⊣⊢ bi_emp (PROP:=PROP).
+  Lemma plainly_emp : ■ emp ⊣⊢@{PROP} emp.
   Proof. by rewrite -!True_emp plainly_pure. Qed.
 
   Lemma plainly_and_sep_l P Q : ■ P ∧ Q ⊣⊢ ■ P ∗ Q.
@@ -311,7 +311,7 @@ Proof. solve_proper. Qed.
 Lemma plainly_if_mono p P Q : (P ⊢ Q) → ■?p P ⊢ ■?p Q.
 Proof. by intros ->. Qed.
 
-Lemma plainly_if_pure p φ : ■?p ⌜φ⌝ ⊣⊢ bi_pure (PROP:=PROP) φ.
+Lemma plainly_if_pure p φ : ■?p ⌜φ⌝ ⊣⊢@{PROP} ⌜φ⌝.
 Proof. destruct p; simpl; auto using plainly_pure. Qed.
 Lemma plainly_if_and p P Q : ■?p (P ∧ Q) ⊣⊢ ■?p P ∧ ■?p Q.
 Proof. destruct p; simpl; auto using plainly_and. Qed.
@@ -406,7 +406,7 @@ Global Instance limit_preserving_Plain {A:ofeT} `{Cofe A} (Φ : A → PROP) :
 Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
 
 (* Plainness instances *)
-Global Instance pure_plain φ : Plain (⌜φ⌝%I : PROP).
+Global Instance pure_plain φ : Plain (PROP:=PROP) ⌜φ⌝.
 Proof. by rewrite /Plain plainly_pure. Qed.
 Global Instance emp_plain : Plain (PROP:=PROP) emp.
 Proof. apply plainly_emp_intro. Qed.
@@ -458,7 +458,7 @@ Global Instance from_option_plain {A} P (Ψ : A → PROP) (mx : option A) :
 Proof. destruct mx; apply _. Qed.
 
 (* Interaction with equality *)
-Lemma plainly_internal_eq {A:ofeT} (a b : A) : plainly (A:=PROP) (a ≡ b) ⊣⊢ a ≡ b.
+Lemma plainly_internal_eq {A:ofeT} (a b : A) : ■ (a ≡ b) ⊣⊢@{PROP} a ≡ b.
 Proof.
   apply (anti_symm (⊢)).
   { by rewrite plainly_elim. }
@@ -511,7 +511,7 @@ Lemma except_0_plainly `{!BiPlainlyExist PROP} P : ◇ ■ P ⊣⊢ ■ ◇ P.
 Proof. by rewrite /sbi_except_0 plainly_or -later_plainly plainly_pure. Qed.
 
 Global Instance internal_eq_plain {A : ofeT} (a b : A) :
-  Plain (a ≡ b : PROP)%I.
+  Plain (PROP:=PROP) (a ≡ b).
 Proof. by intros; rewrite /Plain plainly_internal_eq. Qed.
 
 Global Instance later_plain P : Plain P → Plain (▷ P).
diff --git a/theories/proofmode/class_instances_sbi.v b/theories/proofmode/class_instances_sbi.v
index 18c60184ee059465bd5965c73b0a264de20d0857..9ae1b1d9583d1ea3b7f01ad5e14a0cb54c4b2a62 100644
--- a/theories/proofmode/class_instances_sbi.v
+++ b/theories/proofmode/class_instances_sbi.v
@@ -225,7 +225,7 @@ 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_affinely_later `{!Timeless (emp%I : PROP)} P Q1 Q2 :
+Global Instance into_sep_affinely_later `{!Timeless (PROP:=PROP) emp} P Q1 Q2 :
   IntoSep P Q1 Q2 → Affine Q1 → Affine Q2 →
   IntoSep (<affine> â–· P) (<affine> â–· Q1) (<affine> â–· Q2).
 Proof.