From e6084d75cad77511075a911227025c2f9ea93c02 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 8 Feb 2018 22:56:26 +0100
Subject: [PATCH] Regression test for issue #55.

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

diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 97d711b50..aa433d1c8 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -303,6 +303,14 @@ Lemma test_iNext_plus_3 P Q n m k :
   ▷^m ▷^(2 + S n + k) P -∗ ▷^m ▷ ▷^(2 + S n) Q -∗ ▷^k ▷ ▷^(S (S n + S m)) (P ∗ Q).
 Proof. iIntros "H1 H2". iNext. iNext. iNext. iFrame. Qed.
 
+Lemma test_iNext_unfold P Q n m (R := (â–·^n P)%I) :
+  R ⊢ ▷^m True.
+Proof.
+  iIntros "HR". iNext.
+  match goal with |-  context [ R ] => idtac | |- _ => fail end.
+  done.
+Qed.
+
 Lemma test_iEval x y : ⌜ (y + x)%nat = 1 ⌝ -∗ ⌜ S (x + y) = 2%nat ⌝ : uPred M.
 Proof.
   iIntros (H).
-- 
GitLab