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 _ ||