From 34f64c8df4f2acb5e97899e2e1cb2ce108e49743 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 4 Jul 2018 14:17:02 +0200
Subject: [PATCH] remove big_opL from prettification list

List literals reduce with a spurious `emp` at the end, which is not pretty.
---
 tests/proofmode.ref            | 26 ++++++++++++++++++++++++++
 tests/proofmode.v              |  4 ++--
 theories/proofmode/reduction.v |  2 +-
 3 files changed, 29 insertions(+), 3 deletions(-)

diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index d9611c679..dd0a97deb 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -100,6 +100,19 @@ Tactic failure: iFrame: cannot frame Q.
   --------------------------------------∗
   â–¡ P
   
+1 subgoal
+  
+  PROP : sbi
+  x : nat
+  l : list nat
+  P : PROP
+  ============================
+  "HP" : P
+  _ : [∗ list] y ∈ l, <affine> ⌜y = y⌝
+  _ : [∗ list] y ∈ (x :: l), <affine> ⌜y = y⌝
+  --------------------------------------∗
+  P
+  
 1 subgoal
   
   PROP : sbi
@@ -113,6 +126,19 @@ Tactic failure: iFrame: cannot frame Q.
   --------------------------------------∗
   P
   
+1 subgoal
+  
+  PROP : sbi
+  x1, x2 : nat
+  l1, l2 : list nat
+  P : PROP
+  ============================
+  "HP" : P
+  _ : [∗ list] y1;y2 ∈ [];l2, <affine> ⌜y1 = y2⌝
+  _ : [∗ list] y1;y2 ∈ (x1 :: l1);((x2 :: l2) ++ l2), <affine> ⌜y1 = y2⌝
+  --------------------------------------∗
+  P ∨ ([∗ list] _;_ ∈ (x1 :: l1);(x2 :: l2), True)
+  
 1 subgoal
   
   PROP : sbi
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 48d83b752..7cef4f3e7 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -490,14 +490,14 @@ Lemma test_big_sepL_simpl x (l : list nat) P :
   ([∗ list] k↦y ∈ l, <affine> ⌜ y = y ⌝) -∗
   ([∗ list] y ∈ x :: l, <affine> ⌜ y = y ⌝) -∗
   P.
-Proof. iIntros "HP ??". Show. done. Qed.
+Proof. iIntros "HP ??". Show. simpl. Show. done. Qed.
 
 Lemma test_big_sepL2_simpl x1 x2 (l1 l2 : list nat) P :
   P -∗
   ([∗ list] k↦y1;y2 ∈ []; l2, <affine> ⌜ y1 = y2 ⌝) -∗
   ([∗ list] y1;y2 ∈ x1 :: l1; (x2 :: l2) ++ l2, <affine> ⌜ y1 = y2 ⌝) -∗
   P ∨ ([∗ list] y1;y2 ∈ x1 :: l1; x2 :: l2, True).
-Proof. iIntros "HP ?? /=". Show. by iLeft. Qed.
+Proof. iIntros "HP ??". Show. simpl. Show. by iLeft. Qed.
 
 Lemma test_big_sepL2_iDestruct (Φ : nat → nat → PROP) x1 x2 (l1 l2 : list nat) :
   ([∗ list] y1;y2 ∈ x1 :: l1; x2 :: l2, Φ y1 y2) -∗
diff --git a/theories/proofmode/reduction.v b/theories/proofmode/reduction.v
index 79dde2343..cda25a14c 100644
--- a/theories/proofmode/reduction.v
+++ b/theories/proofmode/reduction.v
@@ -22,7 +22,7 @@ Declare Reduction pm_cbn := cbn [
   tele_fold tele_bind tele_app
   (* BI connectives *)
   bi_persistently_if bi_affinely_if bi_intuitionistically_if
-  bi_wandM sbi_laterN big_opL
+  bi_wandM sbi_laterN
   bi_tforall bi_texist
 ].
 Ltac pm_eval t :=
-- 
GitLab