From b59ddcd1641be5ad54278df36265b16efd193816 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 28 Aug 2017 10:04:57 +0200
Subject: [PATCH] =?UTF-8?q?Make=20it=20possible=20to=20introduce=20?=
 =?UTF-8?q?=E2=96=A1=20=E2=8C=9C=20=CF=86=20=E2=8C=9D=20as=20a=20pure=20hy?=
 =?UTF-8?q?pothesis.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/proofmode/class_instances.v | 3 +++
 theories/tests/proofmode.v           | 3 +++
 2 files changed, 6 insertions(+)

diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 23fd37412..e202bc382 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -48,6 +48,9 @@ Global Instance into_pure_cmra_valid `{CMRADiscrete A} (a : A) :
   @IntoPure M (✓ a) (✓ a).
 Proof. by rewrite /IntoPure discrete_valid. Qed.
 
+Global Instance into_pure_always P φ : IntoPure P φ → IntoPure (□ P) φ.
+Proof. rewrite /IntoPure=> ->. by rewrite always_pure. Qed.
+
 Global Instance into_pure_pure_and (φ1 φ2 : Prop) P1 P2 :
   IntoPure P1 φ1 → IntoPure P2 φ2 → IntoPure (P1 ∧ P2) (φ1 ∧ φ2).
 Proof. rewrite /IntoPure pure_and. by intros -> ->. Qed.
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 5208ff9e7..59d960c0c 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -80,6 +80,9 @@ Qed.
 Lemma test_iIntros_persistent P Q `{!PersistentP Q} : (P → Q → P ∗ Q)%I.
 Proof. iIntros "H1 H2". by iFrame. Qed.
 
+Lemma test_iIntros_pure (ψ φ : Prop) P : ψ → (⌜ φ ⌝ → P → ⌜ φ ∧ ψ ⌝ ∧ P)%I.
+Proof. iIntros (??) "H". auto. Qed.
+
 Lemma test_fast_iIntros P Q :
   (∀ x y z : nat,
     ⌜x = plus 0 x⌝ → ⌜y = 0⌝ → ⌜z = 0⌝ → P → □ Q → foo (x ≡ x))%I.
-- 
GitLab