From ae62c6845a206a1b260c0986088d8043d30c4932 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 30 May 2023 07:41:34 +0200
Subject: [PATCH] Add test case.

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

diff --git a/tests/proofmode.v b/tests/proofmode.v
index b235b26eb..5e06d6df4 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1405,6 +1405,11 @@ Lemma test_iFrame_not_add_emp_for_intuitionistically `{!BiAffine PROP} (P : PROP
   □ P -∗ ∃ _ : nat, □ P.
 Proof. iIntros "#H". iFrame "H". Show. by iExists 0. Qed.
 
+Lemma test_auto_iff P : ⊢ P ↔ P.
+Proof. auto. Qed.
+
+Lemma test_auto_wand_iff P : ⊢ P ∗-∗ P.
+Proof. auto. Qed.
 End tests.
 
 Section parsing_tests.
-- 
GitLab