add test for iNext with evars

8c94e3fb · Ralf Jung · 1e241cca · 8c94e3fb
Commit 8c94e3fb authored Mar 10, 2017 by Ralf Jung
Hide whitespace changes
Inline Side-by-side

Showing with 7 additions and 0 deletions

theories/tests/proofmode.v theories/tests/proofmode.v +7 -0

No files found.
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -146,3 +146,10 @@ Proof. eauto with iFrame. Qed.
 Lemma demo_17 (M : ucmraT) (P Q R : uPred M) `{!PersistentP R} :
  P -∗ Q -∗ R -∗ R ∗ Q ∗ P ∗ R ∨ False.
 Proof. iIntros "HP HQ #HR". iCombine "HR HQ HP HR" as "H". auto. Qed.
+
+Lemma test_iNext_evar (M : ucmraT) (P : uPred M) :
+  P -∗ True.
+Proof.
+  iIntros "HP". iAssert (▷ _ -∗ ▷ P)%I as "?"; last done.
+  iIntros "?". iNext. iAssumption.
+Qed.