diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index c01ce3b5321503eb3afa02566b85f236803ec2bb..58f729c7f2e59838389b1721423098ac9e0d53d1 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -827,17 +827,6 @@ Proof.
   intros. rewrite /Frame intuitionistically_if_elim affinely_elim.
   apply sep_elim_l, _.
 Qed.
-Global Instance frame_intuitionistically_here_absorbing p R :
-  Absorbing R → Frame p (□ R) R True | 0.
-Proof.
-  intros. rewrite /Frame intuitionistically_if_elim intuitionistically_elim.
-  apply sep_elim_l, _.
-Qed.
-Global Instance frame_intuitionistically_here p R : Frame p (â–¡ R) R emp | 1.
-Proof.
-  intros. rewrite /Frame intuitionistically_if_elim intuitionistically_elim.
-  apply sep_elim_l, _.
-Qed.
 
 Global Instance frame_here_pure p φ Q : FromPure false Q φ → Frame p ⌜φ⌝ Q True.
 Proof.
diff --git a/theories/proofmode/modality_instances.v b/theories/proofmode/modality_instances.v
index b780300aa385d4cbc0165cfb5e1e4ef22563868c..6018b7aaee6f7ebd95ae9b71236a8d7601ad1862 100644
--- a/theories/proofmode/modality_instances.v
+++ b/theories/proofmode/modality_instances.v
@@ -25,7 +25,7 @@ Section bi_modalities.
     Modality _ modality_affinely_mixin.
 
   Lemma modality_intuitionistically_mixin :
-    modality_mixin (λ P : PROP, □ P)%I MIEnvId MIEnvIsEmpty.
+    modality_mixin (@bi_intuitionistically PROP) MIEnvId MIEnvIsEmpty.
   Proof.
     split; simpl; eauto using equiv_entails_sym, intuitionistically_emp,
       affinely_mono, persistently_mono, intuitionistically_idemp,