From eb83cf17b8c2d5cd5cb332e58358a084c904f719 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 21 Jul 2023 12:31:02 +0200
Subject: [PATCH] Add test.
---
tests/proofmode.v | 8 ++++++--
1 file changed, 6 insertions(+), 2 deletions(-)
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 2326056ad..7ebd11da3 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -9,10 +9,14 @@ Section tests.
Context {PROP : bi}.
Implicit Types P Q R : PROP.
-Lemma test_eauto_emp_isplit_biwand P : emp ⊢ P ∗-∗ P.
+Lemma test_eauto_iSplit_emp_wand_iff P : emp ⊢ P ∗-∗ P.
Proof. eauto 6. Qed.
-Lemma test_eauto_isplit_biwand P : ⊢ P ∗-∗ P.
+Lemma test_eauto_iSplit_wand_iff P : ⊢ P ∗-∗ P.
+Proof. eauto. Qed.
+
+(** We get the [⊢] automatically from the notation in [stdpp_scope]. *)
+Lemma test_eauto_iSplit_wand_iff_std_scope P : P ∗-∗ P.
Proof. eauto. Qed.
Fixpoint test_fixpoint (n : nat) {struct n} : True → emp ⊢@{PROP} ⌜ (n + 0)%nat = n âŒ.
--
GitLab