From 19f72a6037f09722d15e6d1c9dde84b05397988e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 2 Feb 2018 14:00:25 +0100
Subject: [PATCH] Tests for framing under conjunctions.

---
 theories/tests/proofmode.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 04276bb3b..660d174cb 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -110,6 +110,13 @@ Proof. iIntros "#HP1 HQ2 HP2". iFrame "HP1 HQ2 HP2". Qed.
 Lemma test_iFrame_disjunction_2 P : P -∗ (True ∨ True) ∗ P.
 Proof. iIntros "HP". iFrame "HP". auto. Qed.
 
+Lemma test_iFrame_conjunction_1 P Q :
+  P -∗ Q -∗ (P ∗ Q) ∧ (P ∗ Q).
+Proof. iIntros "HP HQ". iFrame "HP HQ". Qed.
+Lemma test_iFrame_conjunction_2 P Q :
+  P -∗ Q -∗ (P ∧ P) ∗ (Q ∧ Q).
+Proof. iIntros "HP HQ". iFrame "HP HQ". Qed.
+
 Lemma test_iAssert_persistent P Q : P -∗ Q -∗ True.
 Proof.
   iIntros "HP HQ".
-- 
GitLab