diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index c50c6dbd85d7114a304455dee26bb56873731de1..6d832da446c74d8a41e11ebbff3914bf9c525a8a 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -964,7 +964,8 @@ Local Tactic Notation "iExistDestruct" constr(H)
 (** * Modality introduction *)
 Tactic Notation "iModIntro" open_constr(M) :=
   iStartProof;
-  eapply tac_modal_intro with M _ _ _ _;
+  let bi := lazymatch goal with |- @envs_entails ?bi _ _ => bi end in
+  eapply (tac_modal_intro (PROP2 := bi)) with M _ _ _ _;
     [apply _  ||
      fail "iModIntro: the goal is not a modality"
     |apply _ ||
diff --git a/theories/tests/proofmode_monpred.v b/theories/tests/proofmode_monpred.v
index af40b762f84c0d373fbae6aff9689be6fa746491..efdff63786c74f612c54a3c7b9f639bac4904ebd 100644
--- a/theories/tests/proofmode_monpred.v
+++ b/theories/tests/proofmode_monpred.v
@@ -114,4 +114,8 @@ Section tests.
     iIntros "[$ #HP]". iFrame "HP".
   Qed.
 
+  Lemma test_iNext_Bi P :
+    @bi_entails monPredI (â–· P) (â–· P).
+  Proof. iIntros "H". by iNext. Qed.
+
 End tests.