From 07ea98fe6c875193fc6c7dfaceb5b09091c560e0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 31 May 2018 17:30:28 +0200
Subject: [PATCH] =?UTF-8?q?When=20framing,=20`=E2=96=B7=20emp`=20should=20?=
 =?UTF-8?q?be=20turned=20into=20`emp`=20if=20the=20BI=20is=20affine.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

If the BI is not affine, this should not happen, as it may lead to
information loss.

This commit fixes issue #190.
---
 tests/proofmode.v                    | 3 +++
 theories/proofmode/frame_instances.v | 3 +++
 2 files changed, 6 insertions(+)

diff --git a/tests/proofmode.v b/tests/proofmode.v
index 4443bbb9d..197fed735 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -158,6 +158,9 @@ Lemma test_iFrame_conjunction_2 P Q :
   P -∗ Q -∗ (P ∧ P) ∗ (Q ∧ Q).
 Proof. iIntros "HP HQ". iFrame "HP HQ". Qed.
 
+Lemma test_iFrame_later `{BiAffine PROP} P Q : P -∗ Q -∗ ▷ P ∗ Q.
+Proof. iIntros "H1 H2". by iFrame "H1". Qed.
+
 Lemma test_iAssert_modality P : ◇ False -∗ ▷ P.
 Proof.
   iIntros "HF".
diff --git a/theories/proofmode/frame_instances.v b/theories/proofmode/frame_instances.v
index 387608462..b382f7f90 100644
--- a/theories/proofmode/frame_instances.v
+++ b/theories/proofmode/frame_instances.v
@@ -270,6 +270,9 @@ Proof. rewrite /Frame /MakeEmbed -embed_internal_eq. apply (frame_embed p P Q).
 
 Global Instance make_laterN_true n : @KnownMakeLaterN PROP n True True | 0.
 Proof. by rewrite /KnownMakeLaterN /MakeLaterN laterN_True. Qed.
+Global Instance make_laterN_emp `{!BiAffine PROP} n :
+  @KnownMakeLaterN PROP n emp emp | 0.
+Proof. by rewrite /KnownMakeLaterN /MakeLaterN laterN_emp. Qed.
 Global Instance make_laterN_0 P : MakeLaterN 0 P P | 0.
 Proof. by rewrite /MakeLaterN. Qed.
 Global Instance make_laterN_1 P : MakeLaterN 1 P (â–· P) | 2.
-- 
GitLab