From 0dbcaa849e9c528fe5cb1dd10962139efeec2765 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 4 Mar 2018 20:47:38 +0100
Subject: [PATCH] Add test case.

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

diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index c43c2f5c3..9d4f4061c 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -78,6 +78,11 @@ Lemma test_very_fast_iIntros P :
   ∀ x y : nat, (⌜ x = y ⌝ → P -∗ P)%I.
 Proof. by iIntros. Qed.
 
+(** Prior to 0b84351c this used to loop, now `iAssumption` instantiates `R` with
+`False` and performs false elimination. *)
+Lemma test_iAssumption_evar_ex_false : ∃ R, R ⊢ ∀ P, P.
+Proof. eexists. iIntros "?" (P). iAssumption. Qed.
+
 Lemma test_iAssumption_affine P Q R `{!Affine P, !Affine R} : P -∗ Q -∗ R -∗ Q.
 Proof. iIntros "H1 H2 H3". iAssumption. Qed.
 
-- 
GitLab