diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index d369d746b6567fcb2c05a8e16b8108df65dffdb8..c2998995f07dfbf422dda6f7165ce573d29b2242 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -220,6 +220,11 @@ Section iris_tests.
     iIntros "H"; iInv "H" as (v1 v2 v3) "(?&?&_)".
     eauto.
   Qed.
+
+  Theorem test_iApply_inG `{!inG Σ A} γ (x x' : A) :
+    x' ≼ x →
+    own γ x -∗ own γ x'.
+  Proof. intros. by iApply own_mono. Qed.
 End iris_tests.
 
 Section monpred_tests.
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 6edfd45160554634552608a4cbf16473baa94828..fbde9ca80de9cf704c3f7da69bf0efa094d89c34 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -70,7 +70,7 @@ Tactic Notation "iStartProof" :=
   | |- envs_entails _ _ => idtac
   | |- ?φ => notypeclasses refine (as_emp_valid_2 φ _ _);
                [iSolveTC || fail "iStartProof: not a BI assertion"
-               |apply tac_start]
+               |notypeclasses refine (tac_start _ _)]
   end.
 
 (* Same as above, with 2 differences :