From a881b6b965e051c4468f9fd204520ca8a12b1a87 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Thu, 2 Apr 2020 16:34:46 +0200
Subject: [PATCH] Fix testcase from !404

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

diff --git a/tests/proofmode.v b/tests/proofmode.v
index f27ba2444..9ff9c88a3 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -5,9 +5,9 @@ Section tests.
 Context {PROP : sbi}.
 Implicit Types P Q R : PROP.
 
-Lemma type_sbi_internal_eq_annot P :
-  P ≡@{PROP} P ∧ (≡@{PROP}) P P ∧ (P ≡.) P ∧ (.≡ P) P.
-Proof. done. Qed.
+Lemma test_sbi_internal_eq_annot_sections P :
+  ⊢@{PROP} P ≡@{PROP} P ∧ (≡@{PROP}) P P ∧ (P ≡.) P ∧ (.≡ P) P.
+Proof. by iSplit. Qed.
 
 Lemma test_eauto_emp_isplit_biwand P : emp ⊢ P ∗-∗ P.
 Proof. eauto 6. Qed.
-- 
GitLab