From 082ba8f2e7106cc21c24a1df6b201b0bd32b04c8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 2 Feb 2018 13:51:08 +0100
Subject: [PATCH] Frame in both sides of a conjunction.

---
 theories/proofmode/class_instances.v | 14 ++++++++------
 theories/tests/proofmode.v           |  2 +-
 2 files changed, 9 insertions(+), 7 deletions(-)

diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index df0bcffb5..7212515e4 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -565,12 +565,14 @@ Global Instance make_and_true_r P : MakeAnd P True P.
 Proof. by rewrite /MakeAnd right_id. Qed.
 Global Instance make_and_default P Q : MakeAnd P Q (P ∧ Q) | 100.
 Proof. done. Qed.
-Global Instance frame_and_l p R P1 P2 Q Q' :
-  Frame p R P1 Q → MakeAnd Q P2 Q' → Frame p R (P1 ∧ P2) Q' | 9.
-Proof. rewrite /Frame /MakeAnd => <- <-; eauto 10 with I. Qed.
-Global Instance frame_and_r p R P1 P2 Q Q' :
-  Frame p R P2 Q → MakeAnd P1 Q Q' → Frame p R (P1 ∧ P2) Q' | 10.
-Proof. rewrite /Frame /MakeAnd => <- <-; eauto 10 with I. Qed.
+
+Global Instance frame_and p progress1 progress2 R P1 P2 Q1 Q2 Q' :
+  MaybeFrame p R P1 Q1 progress1 →
+  MaybeFrame p R P2 Q2 progress2 →
+  TCEq (progress1 || progress2) true →
+  MakeAnd Q1 Q2 Q' →
+  Frame p R (P1 ∧ P2) Q' | 9.
+Proof. rewrite /MaybeFrame /Frame /MakeAnd => <- <- _ <-; eauto 10 with I. Qed.
 
 Class MakeOr (P Q PQ : uPred M) := make_or : P ∨ Q ⊣⊢ PQ.
 Global Instance make_or_true_l P : MakeOr True P True.
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 45717fcca..04276bb3b 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -102,7 +102,7 @@ Proof. iIntros "[H [? _]]". by iFrame. Qed.
 
 Lemma test_iFrame_pure (x y z : M) :
   ✓ x → ⌜y ≡ z⌝ -∗ (✓ x ∧ ✓ x ∧ y ≡ z : uPred M).
-Proof. iIntros (Hv) "Hxy". by iFrame (Hv Hv) "Hxy". Qed.
+Proof. iIntros (Hv) "Hxy". iFrame (Hv) "Hxy". Qed.
 
 Lemma test_iFrame_disjunction_1 P1 P2 Q1 Q2 :
   □ P1 -∗ Q2 -∗ P2 -∗ (P1 ∗ P2 ∗ False ∨ P2) ∗ (Q1 ∨ Q2).
-- 
GitLab