From 5f74d09c4181c510cdf116f4108d56f02aa550e2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 31 Aug 2017 12:43:25 +0200
Subject: [PATCH] =?UTF-8?q?Strip=20laters=20below=20=E2=96=A0=20and=20?=
 =?UTF-8?q?=E2=96=A1.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 636692cad..691d79dbe 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -932,6 +932,13 @@ Global Instance into_laterN_exist {A} n (Φ Ψ : A → PROP) :
   IntoLaterN' n (∃ x, Φ x) (∃ x, Ψ x).
 Proof. rewrite /IntoLaterN' /IntoLaterN -laterN_exist_2=> ?. by apply exist_mono. Qed.
 
+Global Instance into_later_bare n P Q :
+  IntoLaterN n P Q → IntoLaterN n (■ P) (■ Q).
+Proof. rewrite /IntoLaterN=> ->. by rewrite laterN_bare_2. Qed.
+Global Instance into_later_persistently n P Q :
+  IntoLaterN n P Q → IntoLaterN n (□ P) (□ Q).
+Proof. rewrite /IntoLaterN=> ->. by rewrite laterN_persistently. Qed.
+
 Global Instance into_laterN_sep_l n P1 P2 Q1 Q2 :
   IntoLaterN' n P1 Q1 → IntoLaterN n P2 Q2 →
   IntoLaterN' n (P1 ∗ P2) (Q1 ∗ Q2) | 10.
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 07a5175f1..e57ccad6b 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -217,6 +217,11 @@ Lemma test_iIntros_let P :
   ∀ Q, let R := emp%I in P -∗ R -∗ Q -∗ P ∗ Q.
 Proof. iIntros (Q R) "$ _ $". Qed.
 
+Lemma test_foo P Q : ■ ▷ (Q ≡ P) -∗ ■ ▷ Q -∗ ■ ▷ P.
+Proof.
+  iIntros "#HPQ HQ". iSplit; first done. iNext. by iRewrite "HPQ" in "HQ".
+Qed.
+
 Lemma test_iIntros_modalities `(!Absorbing P) :
   (□ ▷ ∀  x : nat, ⌜ x = 0 ⌝ → ⌜ x = 0 ⌝ -∗ False -∗ P -∗ P)%I.
 Proof.
@@ -224,4 +229,5 @@ Proof.
   iIntros "* **". (* Test that fast intros do not work under modalities *)
   iIntros ([]).
 Qed.
+
 End tests.
-- 
GitLab