From 688de43532e5d7aba507756e0268b4c58c62026a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Sat, 20 Jan 2018 19:34:51 +0100
Subject: [PATCH] Test cases for issue #141.
---
theories/tests/proofmode.v | 7 +++++++
1 file changed, 7 insertions(+)
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index a3cad0ca..caaabaec 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -278,6 +278,13 @@ Proof.
iSpecialize ("Hφ" with "[% //] HP"). done.
Qed.
+Lemma test_iNext_laterN_later P n : ▷ ▷^n P ⊢ ▷^n ▷ P.
+Proof. iIntros "H". iNext. by iNext. Qed.
+Lemma test_iNext_later_laterN P n : ▷^n ▷ P ⊢ ▷ ▷^n P.
+Proof. iIntros "H". iNext. by iNext. Qed.
+Lemma test_iNext_laterN_laterN P n1 n2 : ▷ ▷^n1 ▷^n2 P ⊢ ▷^n1 ▷^n2 ▷ P.
+Proof. iIntros "H". iNext. iNext. by iNext. Qed.
+
(* TODO: This test is broken in Coq 8.6. Should be restored once we drop Coq
8.6 support. See also issue #108. *)
(*
--
2.21.0