Skip to content
Snippets Groups Projects
Commit 688de435 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Test cases for issue #141.

parent 0b949f98
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/tests/proofmode.v
+ 7
− 0
View file @ 688de435
...@@ -278,6 +278,13 @@ Proof. ...@@ -278,6 +278,13 @@ Proof.
iSpecialize ("Hφ" with "[% //] HP"). done. iSpecialize ("Hφ" with "[% //] HP"). done.
Qed. 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 (* TODO: This test is broken in Coq 8.6. Should be restored once we drop Coq
8.6 support. See also issue #108. *) 8.6 support. See also issue #108. *)
(* (*
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment