From efd33d41f8e6b6a1da9088a3fa98cbe7da970b88 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 30 May 2023 07:36:29 +0200
Subject: [PATCH] =?UTF-8?q?Hint=20to=20introduce=20BI=20version=20of=20?=
 =?UTF-8?q?=E2=86=94.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 iris/proofmode/ltac_tactics.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 63edca3ef..ba9756cf8 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.
-- 
GitLab