diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 9a0e3db9bd448503c3b7ab5f77ff94e2485f14e4..ca4a380349472979d2112be511b562476858c650 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -4,86 +4,6 @@ From iris.proofmode Require Export modality_instances classes.
 Set Default Proof Using "Type".
 Import bi.
 
-Section bi_modalities.
-  Context {PROP : bi}.
-
-  Lemma modality_persistently_mixin :
-    modality_mixin (@bi_persistently PROP) MIEnvId MIEnvClear.
-  Proof.
-    split; simpl; eauto using equiv_entails_sym, persistently_intro,
-      persistently_mono, persistently_sep_2 with typeclass_instances.
-  Qed.
-  Definition modality_persistently :=
-    Modality _ modality_persistently_mixin.
-
-  Lemma modality_affinely_mixin :
-    modality_mixin (@bi_affinely PROP) MIEnvId (MIEnvForall Affine).
-  Proof.
-    split; simpl; eauto using equiv_entails_sym, affinely_intro, affinely_mono,
-      affinely_sep_2 with typeclass_instances.
-  Qed.
-  Definition modality_affinely :=
-    Modality _ modality_affinely_mixin.
-
-  Lemma modality_affinely_persistently_mixin :
-    modality_mixin (λ P : PROP, □ P)%I MIEnvId MIEnvIsEmpty.
-  Proof.
-    split; simpl; eauto using equiv_entails_sym, affinely_persistently_emp,
-      affinely_mono, persistently_mono, affinely_persistently_idemp,
-      affinely_persistently_sep_2 with typeclass_instances.
-  Qed.
-  Definition modality_affinely_persistently :=
-    Modality _ modality_affinely_persistently_mixin.
-
-  Lemma modality_plainly_mixin :
-    modality_mixin (@bi_plainly PROP) (MIEnvForall Plain) MIEnvClear.
-  Proof.
-    split; simpl; split_and?; eauto using equiv_entails_sym, plainly_intro,
-      plainly_mono, plainly_and, plainly_sep_2 with typeclass_instances.
-  Qed.
-  Definition modality_plainly :=
-    Modality _ modality_plainly_mixin.
-
-  Lemma modality_affinely_plainly_mixin :
-    modality_mixin (λ P : PROP, ■ P)%I (MIEnvForall Plain) MIEnvIsEmpty.
-  Proof.
-    split; simpl; split_and?; eauto using equiv_entails_sym,
-      affinely_plainly_emp, affinely_intro,
-      plainly_intro, affinely_mono, plainly_mono, affinely_plainly_idemp,
-      affinely_plainly_and, affinely_plainly_sep_2 with typeclass_instances.
-  Qed.
-  Definition modality_affinely_plainly :=
-    Modality _ modality_affinely_plainly_mixin.
-
-  Lemma modality_embed_mixin `{BiEmbedding PROP PROP'} :
-    modality_mixin (@bi_embed PROP PROP' _)
-      (MIEnvTransform IntoEmbed) (MIEnvTransform IntoEmbed).
-  Proof.
-    split; simpl; split_and?;
-      eauto using equiv_entails_sym, bi_embed_emp, bi_embed_sep, bi_embed_and.
-    - intros P Q. rewrite /IntoEmbed=> ->.
-      by rewrite bi_embed_affinely bi_embed_persistently.
-    - by intros P Q ->.
-  Qed.
-  Definition modality_embed `{BiEmbedding PROP PROP'} :=
-    Modality _ modality_embed_mixin.
-End bi_modalities.
-
-Section sbi_modalities.
-  Context {PROP : sbi}.
-
-  Lemma modality_laterN_mixin n :
-    modality_mixin (@sbi_laterN PROP n)
-      (MIEnvTransform (MaybeIntoLaterN false n)) (MIEnvTransform (MaybeIntoLaterN false n)).
-  Proof.
-    split; simpl; split_and?; eauto using equiv_entails_sym, laterN_intro,
-      laterN_mono, laterN_and, laterN_sep with typeclass_instances.
-    rewrite /MaybeIntoLaterN=> P Q ->. by rewrite laterN_affinely_persistently_2.
-  Qed.
-  Definition modality_laterN n :=
-    Modality _ (modality_laterN_mixin n).
-End sbi_modalities.
-
 Section bi_instances.
 Context {PROP : bi}.
 Implicit Types P Q R : PROP.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 6d832da446c74d8a41e11ebbff3914bf9c525a8a..6ddb46daeacc6827950943424a4f44035c522a41 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -964,8 +964,7 @@ Local Tactic Notation "iExistDestruct" constr(H)
 (** * Modality introduction *)
 Tactic Notation "iModIntro" open_constr(M) :=
   iStartProof;
-  let bi := lazymatch goal with |- @envs_entails ?bi _ _ => bi end in
-  eapply (tac_modal_intro (PROP2 := bi)) with M _ _ _ _;
+  notypeclasses refine (tac_modal_intro M _ _ _ _ _ _ _ _ _ _ _ _);
     [apply _  ||
      fail "iModIntro: the goal is not a modality"
     |apply _ ||