From b6859ed1d2d2159d63d8c7c06f3878346e0ea3c5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 10 Feb 2020 16:43:42 +0100
Subject: [PATCH] Disable test, since it's not compatible with Coq 8.8 and 8.9.

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

diff --git a/tests/proofmode.v b/tests/proofmode.v
index b0d52b54c..6057efb1c 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -239,6 +239,8 @@ Proof.
   iFrame.
 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.
 Proof.
   iExists _.
@@ -246,6 +248,7 @@ Proof.
   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