From 14fe028c525af10e7925c08e4b719f8b18c7739d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 12 Mar 2017 13:48:59 +0100
Subject: [PATCH] also add my original testcase, just to be sure

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

diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index a5eb0623d..f8c169ca0 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -154,10 +154,16 @@ Proof.
   iIntros "?". iNext. iAssumption.
 Qed.
 
-Lemma test_iNext_sep (M : ucmraT) (P Q : uPred M)
+Lemma test_iNext_sep1 (M : ucmraT) (P Q : uPred M)
     (R1 := (P ∗ Q)%I) (R2 := (▷ P ∗ ▷ Q)%I) :
   (▷ P ∗ ▷ Q) ∗ R1 ∗ R2 -∗ ▷ (P ∗ Q) ∗ ▷ R1 ∗ R2.
 Proof.
   iIntros "H". iNext.
   rewrite {1 2}(lock R1). (* check whether R1 has not been unfolded *) done.
 Qed.
+
+Lemma test_iNext_sep2 (M : ucmraT) (P Q : uPred M) :
+  ▷ P ∗ ▷ Q -∗ ▷ (P ∗ Q).
+Proof.
+  iIntros "H". iNext. iExact "H". (* Check that the laters are all gone. *)
+Qed.
-- 
GitLab