diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 63edca3efe3deb94a723d554ec6746c367c71763..ba9756cf8725e0a3686e578dd185d40a717b54c1 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -3511,6 +3511,7 @@ Global Hint Extern 0 (envs_entails _ (∀.. _, _)) => iIntros (?) : core.
 
 Global Hint Extern 1 (envs_entails _ (_ ∧ _)) => iSplit : core.
 Global Hint Extern 1 (envs_entails _ (_ ∗ _)) => iSplit : core.
+Global Hint Extern 1 (envs_entails _ (_ ↔ _)) => iSplit : core.
 Global Hint Extern 1 (envs_entails _ (_ ∗-∗ _)) => iSplit : core.
 Global Hint Extern 1 (envs_entails _ (â–· _)) => iNext : core.
 Global Hint Extern 1 (envs_entails _ (â–  _)) => iModIntro : core.