From 2fb9976683ad5db22492fb0bd65b4d7c0eb5333b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 5 Sep 2020 14:56:02 +0200
Subject: [PATCH] Remove duplicate test of `test_iIntros_pure_not`.

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

diff --git a/tests/proofmode.v b/tests/proofmode.v
index 56aa97a8d..d84511d9d 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -778,9 +778,6 @@ Check "test_iSimpl_in4".
 Lemma test_iSimpl_in4 x y : ⌜ (3 + x)%nat = y ⌝ -∗ ⌜ S (S (S x)) = y ⌝ : PROP.
 Proof. iIntros "H". Fail iSimpl in "%". by iSimpl in "H". Qed.
 
-Lemma test_iIntros_pure_neg : ⊢@{PROP} ⌜ ¬False ⌝.
-Proof. by iIntros (?). Qed.
-
 Lemma test_iPureIntro_absorbing (φ : Prop) :
   φ → ⊢@{PROP} <absorb> ⌜φ⌝.
 Proof. intros ?. iPureIntro. done. Qed.
-- 
GitLab