From 8c94e3fb277866f65f796bc4bf0ef37760188cfb Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 10 Mar 2017 09:43:28 +0100
Subject: [PATCH] add test for iNext with evars

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

diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 5ea81c851..b32d5780a 100644
--- 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.
-- 
GitLab