From 5bd2042e0829d5b4982bfbd00f306263f756c5fb Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 23 Nov 2016 11:29:10 +0100
Subject: [PATCH] =?UTF-8?q?Handle=20=E2=8A=A3=E2=8A=A2=20consistently=20in?=
=?UTF-8?q?=20iProof=20instead=20of=20iSplit.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
proofmode/tactics.v | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 00c6b395a..ec00c04ab 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -47,6 +47,7 @@ Tactic Notation "iProof" :=
| |- of_envs _ ⊢ _ => fail "iProof: already in Iris proofmode"
| |- True ⊢ _ => apply tac_adequate
| |- _ ⊢ _ => apply uPred.wand_entails, tac_adequate
+ | |- _ ⊣⊢ _ => apply uPred.iff_equiv, tac_adequate
end.
(** * Context manipulation *)
@@ -508,12 +509,12 @@ Local Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) :=
(** * Conjunction and separating conjunction *)
Tactic Notation "iSplit" :=
+ try iProof;
lazymatch goal with
| |- _ ⊢ _ =>
eapply tac_and_split;
[let P := match goal with |- FromAnd ?P _ _ => P end in
apply _ || fail "iSplit:" P "not a conjunction"| |]
- | |- _ ⊣⊢ _ => apply (anti_symm (⊢))
end.
Tactic Notation "iSplitL" constr(Hs) :=
--
GitLab