From bcce68dbd158f987aee169d6dc7ea9c0b3e84182 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 21 Mar 2018 16:06:00 +0100
Subject: [PATCH] Stop iFrame from introducing modalities

Fixes #176
---
 theories/bi/lib/fixpoint.v           | 3 +--
 theories/proofmode/frame_instances.v | 8 --------
 theories/tests/proofmode.v           | 4 ++--
 3 files changed, 3 insertions(+), 12 deletions(-)

diff --git a/theories/bi/lib/fixpoint.v b/theories/bi/lib/fixpoint.v
index fff0a31fc..d02a74061 100644
--- a/theories/bi/lib/fixpoint.v
+++ b/theories/bi/lib/fixpoint.v
@@ -85,8 +85,7 @@ Section greatest.
     F (bi_greatest_fixpoint F) x ⊢ bi_greatest_fixpoint F x.
   Proof.
     iIntros "HF". iExists (CofeMor (F (bi_greatest_fixpoint F))).
-    (* FIXME: The framing here adds an <affine> modality that we have to introduce. *)
-    iIntros "{$HF} !# !#" (y) "Hy". iApply (bi_mono_pred with "[#] Hy").
+    iSplit; last done. iIntros "!#" (y) "Hy". iApply (bi_mono_pred with "[#] Hy").
     iIntros "!#" (z) "?". by iApply greatest_fixpoint_unfold_1.
   Qed.
 
diff --git a/theories/proofmode/frame_instances.v b/theories/proofmode/frame_instances.v
index c13a25033..68d2bfce7 100644
--- a/theories/proofmode/frame_instances.v
+++ b/theories/proofmode/frame_instances.v
@@ -58,12 +58,8 @@ Global Instance make_sep_emp_r P : KnownRMakeSep P emp P.
 Proof. apply right_id, _. Qed.
 Global Instance make_sep_true_l P : Absorbing P → KnownLMakeSep True P P.
 Proof. intros. apply True_sep, _. Qed.
-Global Instance make_and_emp_l_absorbingly P : KnownLMakeSep True P (<absorb> P) | 10.
-Proof. intros. by rewrite /KnownLMakeSep /MakeSep. Qed.
 Global Instance make_sep_true_r P : Absorbing P → KnownRMakeSep P True P.
 Proof. intros. by rewrite /KnownRMakeSep /MakeSep sep_True. Qed.
-Global Instance make_and_emp_r_absorbingly P : KnownRMakeSep P True (<absorb> P) | 10.
-Proof. intros. by rewrite /KnownRMakeSep /MakeSep comm. Qed.
 Global Instance make_sep_default P Q : MakeSep P Q (P ∗ Q) | 100.
 Proof. by rewrite /MakeSep. Qed.
 
@@ -101,12 +97,8 @@ Global Instance make_and_true_r P : KnownRMakeAnd P True P.
 Proof. by rewrite /KnownRMakeAnd /MakeAnd right_id. Qed.
 Global Instance make_and_emp_l P : Affine P → KnownLMakeAnd emp P P.
 Proof. intros. by rewrite /KnownLMakeAnd /MakeAnd emp_and. Qed.
-Global Instance make_and_emp_l_affinely P : KnownLMakeAnd emp P (<affine> P) | 10.
-Proof. intros. by rewrite /KnownLMakeAnd /MakeAnd. Qed.
 Global Instance make_and_emp_r P : Affine P → KnownRMakeAnd P emp P.
 Proof. intros. by rewrite /KnownRMakeAnd /MakeAnd and_emp. Qed.
-Global Instance make_and_emp_r_affinely P : KnownRMakeAnd P emp (<affine> P) | 10.
-Proof. intros. by rewrite /KnownRMakeAnd /MakeAnd comm. Qed.
 Global Instance make_and_default P Q : MakeAnd P Q (P ∧ Q) | 100.
 Proof. by rewrite /MakeAnd. Qed.
 
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index f9c38b371..e8d30aa73 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -57,7 +57,7 @@ Lemma test_iDestruct_and_emp P Q `{!Persistent P, !Persistent Q} :
 Proof. iIntros "[#? _] [_ #?]". auto. Qed.
 
 Lemma test_iIntros_persistent P Q `{!Persistent Q} : (P → Q → P ∧ Q)%I.
-Proof. iIntros "H1 #H2". by iFrame. Qed.
+Proof. iIntros "H1 #H2". by iFrame "∗#". Qed.
 
 Lemma test_iIntros_pure (ψ φ : Prop) P : ψ → (⌜ φ ⌝ → P → ⌜ φ ∧ ψ ⌝ ∧ P)%I.
 Proof. iIntros (??) "H". auto. Qed.
@@ -374,7 +374,7 @@ Lemma test_assert_affine_pure (φ : Prop) P :
 Proof. iIntros (Hφ). iAssert (<affine> ⌜φ⌝)%I with "[%]" as "$"; auto. Qed.
 Lemma test_assert_pure (φ : Prop) P :
   φ → P ⊢ P ∗ ⌜φ⌝.
-Proof. iIntros (Hφ). iAssert ⌜φ⌝%I with "[%]" as "$"; auto. Qed.
+Proof. iIntros (Hφ). iAssert ⌜φ⌝%I with "[%]" as "$"; auto with iFrame. Qed.
 
 Lemma test_iEval x y : ⌜ (y + x)%nat = 1 ⌝ -∗ ⌜ S (x + y) = 2%nat ⌝ : PROP.
 Proof.
-- 
GitLab