From e8debd6d60abbd4a430a25e9a19fd1c8b90bd0c1 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 7 Mar 2018 19:15:20 +0100
Subject: [PATCH] test iAssumption-based evar instantiation

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

diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 5d5e8dff1..45c124d98 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -408,4 +408,12 @@ Proof.
   eexists. split. iIntros "#? ? ? ?". iAccu. done.
 Qed.
 
+Lemma test_iAssumption_evar P : âˆƒ R, (R âŠ¢ P) /\ R = P.
+Proof.
+  eexists. split.
+  - iIntros "H". iAssumption.
+  (* Now verify that the evar was chosen as desired (i.e., it should not pick False). *)
+  - reflexivity.
+Qed.
+
 End tests.
-- 
GitLab