From 8ca3fc9b6f448a4e4561a63d3a2517021bf493b5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 16 Jun 2016 15:27:06 +0200
Subject: [PATCH] =?UTF-8?q?Make=20iSplit=20work=20on=20goals=20of=20the=20?=
 =?UTF-8?q?shape=20=E2=8A=A3=E2=8A=A2.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 proofmode/tactics.v | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index b076e5b79..944b2118d 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -333,9 +333,13 @@ Local Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) :=
 
 (** * Conjunction and separating conjunction *)
 Tactic Notation "iSplit" :=
-  eapply tac_and_split;
-    [let P := match goal with |- AndSplit ?P _ _ => P end in
-     apply _ || fail "iSplit:" P "not a conjunction"| |].
+  lazymatch goal with
+  | |- _ ⊢ _ =>
+    eapply tac_and_split;
+      [let P := match goal with |- AndSplit ?P _ _ => P end in
+       apply _ || fail "iSplit:" P "not a conjunction"| |]
+  | |- _ ⊣⊢ _ => apply (anti_symm (⊢))
+  end.
 
 Tactic Notation "iSplitL" constr(Hs) :=
   let Hs := words Hs in
-- 
GitLab