diff --git a/tests/proofmode.v b/tests/proofmode.v
index 4a962019ca130bdf8a6449972f773baf9f816caf..fe6b8969ac8d5844a71cc8a415e37140eea87183 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -10,7 +10,7 @@ Lemma test_eauto_emp_isplit_biwand P : emp ⊢ P ∗-∗ P.
 Proof. eauto 6. Qed.
 
 Lemma test_eauto_isplit_biwand P : (P ∗-∗ P)%I.
-Proof. iStartProof. eauto. Qed.
+Proof. eauto. Qed.
 
 Check "demo_0".
 Lemma demo_0 P Q : □ (P ∨ Q) -∗ (∀ x, ⌜x = 0⌝ ∨ ⌜x = 1⌝) → (Q ∨ P).
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index e716667414e4648b965d65db33d753c57cf488b8..6edfd45160554634552608a4cbf16473baa94828 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -3153,6 +3153,7 @@ Tactic Notation "iAccu" :=
 
 (** Automation *)
 Hint Extern 0 (_ ⊢ _) => iStartProof : core.
+Hint Extern 0 (bi_emp_valid _) => iStartProof : core.
 
 (* Make sure that by and done solve trivial things in proof mode *)
 Hint Extern 0 (envs_entails _ _) => iPureIntro; try done : core.