From 9eb65b87c8853dbdd9c08b46fffd27bf2052695f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 28 Oct 2017 16:58:21 +0200
Subject: [PATCH] Temporarily remove a test that fails in Coq 8.6. See #108 for
 details.

---
 theories/tests/proofmode.v | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 4aa097847..1ed83a72f 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -233,9 +233,6 @@ Qed.
 Lemma test_iIntros_rewrite P (x1 x2 x3 x4 : nat) :
   x1 = x2 → (⌜ x2 = x3 ⌝ ∗ ⌜ x3 ≡ x4 ⌝ ∗ P) -∗ ⌜ x1 = x4 ⌝ ∗ P.
 Proof. iIntros (?) "(-> & -> & $)"; auto. Qed.
-
-Lemma test_iItros_pure : (⌜ ¬False ⌝ : uPred M)%I.
-Proof. by iIntros (?). Qed.
 End tests.
 
 Section more_tests.
-- 
GitLab