From 7319e95eac7c1562935928f8d635923fa68b9101 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 10 Jun 2018 18:15:19 +0200
Subject: [PATCH] test via printing that the goal looks like it should

---
 tests/proofmode.ref | 11 +++++++++++
 tests/proofmode.v   |  4 ++--
 2 files changed, 13 insertions(+), 2 deletions(-)

diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 4dcf318a5..558ea48ba 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -31,6 +31,17 @@
   --------------------------------------â–¡
   <affine> (P ∗ Q)
   
+1 subgoal
+  
+  PROP : sbi
+  H : BiAffine PROP
+  P, Q : PROP
+  ============================
+  _ : â–¡ P
+  _ : Q
+  --------------------------------------∗
+  â–¡ P
+  
 1 subgoal
   
   PROP : sbi
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 3905f8bb7..2c340bc11 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -482,9 +482,9 @@ Qed.
 
 Lemma test_and_sep_affine_bi `{BiAffine PROP} P Q : □ P ∧ Q ⊢ □ P ∗ Q.
 Proof.
-  iIntros "[??]". iSplit; last done.
-  lazymatch goal with |- coq_tactics.envs_entails _ (â–¡ P) => done end.
+  iIntros "[??]". iSplit; last done. Show. done.
 Qed.
+
 End tests.
 
 (** Test specifically if certain things print correctly. *)
-- 
GitLab