From c3ceb58374a98f8cef6b4110e8cda8741abe807f Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com> Date: Thu, 7 Nov 2019 20:20:59 +0100 Subject: [PATCH] =?UTF-8?q?Add=20missing=20`iSplit`=20hint=20for=20`?= =?UTF-8?q?=E2=88=97-=E2=88=97`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- theories/proofmode/ltac_tactics.v | 1 + 1 file changed, 1 insertion(+) diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v index f25bfb91a..e71666741 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. -- GitLab