From b014183112294d10d21bf86dc678d52b067a78f7 Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Wed, 11 Nov 2020 10:46:53 -0600
Subject: [PATCH] Add back a proofmode test for issue #288

This test is incompatible with Coq 8.8 and Coq 8.9, but Iris no longer
supports those versions.
---
 tests/proofmode.v | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/tests/proofmode.v b/tests/proofmode.v
index a7c3a1dc4..5aa0f8f9f 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -410,15 +410,13 @@ Proof.
 Qed.
 
 (* Test for issue #288 *)
-(* FIXME: Restore once we drop support for Coq 8.8 and Coq 8.9.
-Lemma test_iExists_unused : (∃ P : PROP, ∃ x : nat, P)%I.
+Lemma test_iExists_unused : ⊢ ∃ P : PROP, ∃ x : nat, P.
 Proof.
   iExists _.
   iExists 10.
   iAssert emp%I as "H"; first done.
   iExact "H".
 Qed.
-*)
 
 (* Check coercions *)
 Lemma test_iExist_coercion (P : Z → PROP) : (∀ x, P x) -∗ ∃ x, P x.
-- 
GitLab