From 8fd3233e600849807b5382fb07828cef45e7d9df Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 1 Jun 2018 10:32:10 +0200
Subject: [PATCH] tests/mosel_paper: show the two goals separately

---
 tests/mosel_paper.ref | 22 ++++++++++++++--------
 tests/mosel_paper.v   |  6 +++---
 2 files changed, 17 insertions(+), 11 deletions(-)

diff --git a/tests/mosel_paper.ref b/tests/mosel_paper.ref
index 3031fbef6..700e1159a 100644
--- a/tests/mosel_paper.ref
+++ b/tests/mosel_paper.ref
@@ -10,7 +10,7 @@
   --------------------------------------∗
   ∃ a : A, P ∗ Φ a ∨ P ∗ Ψ a
   
-2 subgoals
+1 subgoal
   
   PROP : bi
   A : Type
@@ -23,13 +23,19 @@
   --------------------------------------∗
   ∃ a : A, P ∗ Φ a ∨ P ∗ Ψ a
   
-
-subgoal 2 is:
- "HP" : P
-"H2" : Ψ x
---------------------------------------∗
-∃ a : A, P ∗ Φ a ∨ P ∗ Ψ a
-
+1 subgoal
+  
+  PROP : bi
+  A : Type
+  P : PROP
+  Φ, Ψ : A → PROP
+  x : A
+  ============================
+  "HP" : P
+  "H2" : Ψ x
+  --------------------------------------∗
+  ∃ a : A, P ∗ Φ a ∨ P ∗ Ψ a
+  
 1 subgoal
   
   PROP : bi
diff --git a/tests/mosel_paper.v b/tests/mosel_paper.v
index e5e08f8c4..25211740a 100644
--- a/tests/mosel_paper.v
+++ b/tests/mosel_paper.v
@@ -12,9 +12,9 @@ Lemma example_1 {PROP : bi} {A : Type} (P : PROP) (Φ Ψ : A → PROP) :
   P ∗ (∃ a, Φ a ∨ Ψ a) -∗ ∃ a, (P ∗ Φ a) ∨ (P ∗ Ψ a).
 Proof.
   iIntros "[HP H]". Show.
-  iDestruct "H" as (x) "[H1|H2]". Show.
-  - iExists x. iLeft. iSplitL "HP"; iAssumption.
-  - iExists x. iRight. iSplitL "HP"; iAssumption.
+  iDestruct "H" as (x) "[H1|H2]".
+  - Show. iExists x. iLeft. iSplitL "HP"; iAssumption.
+  - Show. iExists x. iRight. iSplitL "HP"; iAssumption.
 Qed.
 Lemma example {PROP : bi} {A : Type} (P : PROP) (Φ Ψ : A → PROP) :
 P ∗ (∃ a, Φ a ∨ Ψ a) -∗ ∃ a, (P ∗ Φ a) ∨ (P ∗ Ψ a).
-- 
GitLab