From 21bf312c7dabd83bd3f0c4eb708a7b78534f0ac2 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Fri, 8 Nov 2019 15:59:28 +0100
Subject: [PATCH 1/3] Drop trailing whitespace

---
 tests/proofmode.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/proofmode.v b/tests/proofmode.v
index adfc17780..85903527a 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -158,7 +158,7 @@ Proof.
   iIntros "H".
   let H1 := iFresh in
   let H2 := iFresh in
-  let pat :=constr:(IList [cons (IIdent H1) (cons (IIdent H2) nil)]) in 
+  let pat :=constr:(IList [cons (IIdent H1) (cons (IIdent H2) nil)]) in
   iDestruct "H" as pat.
   iFrame.
 Qed.
-- 
GitLab


From 0f5eca6768ce158983e2d86096cf99436c157472 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Fri, 8 Nov 2019 15:57:50 +0100
Subject: [PATCH 2/3] Test new hint for `bi_wand` (from !331)

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

diff --git a/tests/proofmode.v b/tests/proofmode.v
index 85903527a..4a962019c 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -6,6 +6,12 @@ Section tests.
 Context {PROP : sbi}.
 Implicit Types P Q R : PROP.
 
+Lemma test_eauto_emp_isplit_biwand P : emp ⊢ P ∗-∗ P.
+Proof. eauto 6. Qed.
+
+Lemma test_eauto_isplit_biwand P : (P ∗-∗ P)%I.
+Proof. iStartProof. eauto. Qed.
+
 Check "demo_0".
 Lemma demo_0 P Q : □ (P ∨ Q) -∗ (∀ x, ⌜x = 0⌝ ∨ ⌜x = 1⌝) → (Q ∨ P).
 Proof.
-- 
GitLab


From ee17a74d846ba7622990add3565d5f95523a457c Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Fri, 8 Nov 2019 15:59:01 +0100
Subject: [PATCH 3/3] Add another missing hint

---
 tests/proofmode.v                 | 2 +-
 theories/proofmode/ltac_tactics.v | 1 +
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/tests/proofmode.v b/tests/proofmode.v
index 4a962019c..fe6b8969a 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -10,7 +10,7 @@ Lemma test_eauto_emp_isplit_biwand P : emp ⊢ P ∗-∗ P.
 Proof. eauto 6. Qed.
 
 Lemma test_eauto_isplit_biwand P : (P ∗-∗ P)%I.
-Proof. iStartProof. eauto. Qed.
+Proof. eauto. Qed.
 
 Check "demo_0".
 Lemma demo_0 P Q : □ (P ∨ Q) -∗ (∀ x, ⌜x = 0⌝ ∨ ⌜x = 1⌝) → (Q ∨ P).
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index e71666741..6edfd4516 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -3153,6 +3153,7 @@ Tactic Notation "iAccu" :=
 
 (** Automation *)
 Hint Extern 0 (_ ⊢ _) => iStartProof : core.
+Hint Extern 0 (bi_emp_valid _) => iStartProof : core.
 
 (* Make sure that by and done solve trivial things in proof mode *)
 Hint Extern 0 (envs_entails _ _) => iPureIntro; try done : core.
-- 
GitLab