diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index f25bfb91af287a2010c8f7e86cc31965545e20d4..e716667414e4648b965d65db33d753c57cf488b8 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -3186,6 +3186,7 @@ Hint Extern 0 (envs_entails _ (∀.. _, _)) => iIntros (?) : core.
 
 Hint Extern 1 (envs_entails _ (_ ∧ _)) => iSplit : core.
 Hint Extern 1 (envs_entails _ (_ ∗ _)) => iSplit : core.
+Hint Extern 1 (envs_entails _ (_ ∗-∗ _)) => iSplit : core.
 Hint Extern 1 (envs_entails _ (â–· _)) => iNext : core.
 Hint Extern 1 (envs_entails _ (â–  _)) => iAlways : core.
 Hint Extern 1 (envs_entails _ (<pers> _)) => iAlways : core.