From b3c142a2ca5188cbd27fb99fc1649d34ca57bf7f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 29 Jul 2021 11:00:54 +0200
Subject: [PATCH] make binary wand/view shift connectives 'block' formated

---
 iris/bi/notation.v       | 14 +++++++-------
 tests/proofmode.ref      |  8 ++++----
 tests/proofmode_iris.ref |  2 +-
 3 files changed, 12 insertions(+), 12 deletions(-)

diff --git a/iris/bi/notation.v b/iris/bi/notation.v
index b2f1b3845..4ca6fddcb 100644
--- a/iris/bi/notation.v
+++ b/iris/bi/notation.v
@@ -37,7 +37,7 @@ Reserved Notation "'⌜' φ '⌝'" (at level 1, φ at level 200, format "⌜ φ
 Reserved Notation "P ∗ Q" (at level 80, right associativity, format "P  ∗  '/' Q").
 Reserved Notation "P -∗ Q"
   (at level 99, Q at level 200, right associativity,
-   format "'[' P  -∗  '/' Q ']'").
+   format "'[' P  -∗  '/' '[' Q ']' ']'").
 
 Reserved Notation "⎡ P ⎤".
 
@@ -85,14 +85,14 @@ Reserved Notation "|={ E1 , E2 }=> Q"
    format "'[  ' |={ E1 , E2 }=>  '/' Q ']'").
 Reserved Notation "P ={ E1 , E2 }=∗ Q"
   (at level 99, E1,E2 at level 50, Q at level 200,
-   format "'[' P  ={ E1 , E2 }=∗  '/' Q ']'").
+   format "'[' P  ={ E1 , E2 }=∗  '/' '[' Q ']' ']'").
 
 Reserved Notation "|={ E }=> Q"
   (at level 99, E at level 50, Q at level 200,
    format "'[  ' |={ E }=>  '/' Q ']'").
 Reserved Notation "P ={ E }=∗ Q"
   (at level 99, E at level 50, Q at level 200,
-   format "'[' P  ={ E }=∗  '/' Q ']'").
+   format "'[' P  ={ E }=∗  '/' '[' Q ']' ']'").
 
 (** Step-taking fancy updates *)
 Reserved Notation "|={ E1 } [ E2 ]â–·=> Q"
@@ -100,13 +100,13 @@ Reserved Notation "|={ E1 } [ E2 ]â–·=> Q"
    format "'[  ' |={ E1 } [ E2 ]â–·=>  '/' Q ']'").
 Reserved Notation "P ={ E1 } [ E2 ]▷=∗ Q"
   (at level 99, E1, E2 at level 50, Q at level 200,
-   format "'[' P  ={ E1 } [ E2 ]▷=∗  '/' Q ']'").
+   format "'[' P  ={ E1 } [ E2 ]▷=∗  '/' '[' Q ']' ']'").
 Reserved Notation "|={ E }â–·=> Q"
   (at level 99, E at level 50, Q at level 200,
    format "'[  ' |={ E }â–·=>  '/' Q ']'").
 Reserved Notation "P ={ E }▷=∗ Q"
   (at level 99, E at level 50, Q at level 200,
-   format "'[' P  ={ E }▷=∗  '/' Q ']'").
+   format "'[' P  ={ E }▷=∗  '/' '[' Q ']' ']'").
 
 (** Multi-step-taking fancy updates *)
 Reserved Notation "|={ E1 } [ E2 ]â–·=>^ n Q"
@@ -114,13 +114,13 @@ Reserved Notation "|={ E1 } [ E2 ]â–·=>^ n Q"
    format "'[  ' |={ E1 } [ E2 ]â–·=>^ n  '/' Q ']'").
 Reserved Notation "P ={ E1 } [ E2 ]▷=∗^ n Q"
   (at level 99, E1, E2 at level 50, n at level 9, Q at level 200,
-   format "'[' P  ={ E1 } [ E2 ]▷=∗^ n  '/' Q ']'").
+   format "'[' P  ={ E1 } [ E2 ]▷=∗^ n  '/' '[' Q ']' ']'").
 Reserved Notation "|={ E }â–·=>^ n Q"
   (at level 99, E at level 50, n at level 9, Q at level 200,
    format "'[  ' |={ E }â–·=>^ n  '/' Q ']'").
 Reserved Notation "P ={ E }▷=∗^ n Q"
   (at level 99, E at level 50, n at level 9, Q at level 200,
-   format "'[' P  ={ E }▷=∗^ n  '/' Q ']'").
+   format "'[' P  ={ E }▷=∗^ n  '/' '[' Q ']' ']'").
 
 (** * Big Ops *)
 Reserved Notation "'[∗' 'list]' k ↦ x ∈ l , P"
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 78d3fc66c..e2b369c4a 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -456,8 +456,8 @@ Tactic failure: iFrame: cannot frame Q.
   PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
   ============================
   --------------------------------------∗
-  PPPPPPPPPPPPPPPPP -∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗
-  QQQQQQQQQQQQQQQQQQ
+  PPPPPPPPPPPPPPPPP -∗
+  QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
 "long_wand_nested"
      : string
 1 goal
@@ -480,8 +480,8 @@ Tactic failure: iFrame: cannot frame Q.
   PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
   ============================
   --------------------------------------∗
-  PPPPPPPPPPPPPPPPP ={E}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗
-  QQQQQQQQQQQQQQQQQQ
+  PPPPPPPPPPPPPPPPP ={E}=∗
+  QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
 "long_fupd_nested"
      : string
 1 goal
diff --git a/tests/proofmode_iris.ref b/tests/proofmode_iris.ref
index 1c66decee..f7d43a2cc 100644
--- a/tests/proofmode_iris.ref
+++ b/tests/proofmode_iris.ref
@@ -111,7 +111,7 @@
   P : iProp Σ
   ============================
   ↑N ⊆ E2
-  → na_inv t N (<pers> P) ∗ na_own t E1 ∗ na_own t E2 ={⊤}=∗ 
+  → na_inv t N (<pers> P) ∗ na_own t E1 ∗ na_own t E2 ={⊤}=∗
     na_own t E1 ∗ na_own t E2 ∗ ▷ P
 1 goal
   
-- 
GitLab