From 163e26ee28edc75dc1cfabac143c5482c2367ac9 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 27 Jul 2021 15:20:00 +0200
Subject: [PATCH] improve view shift and Hoare triple printing

to avoid bad regressions, some other notations also ha to be tweaked
---
 iris/base_logic/lib/fancy_updates_from_vs.v |  4 +-
 iris/bi/lib/counterexamples.v               |  3 +-
 iris/bi/notation.v                          | 32 ++++++-------
 iris/bi/weakestpre.v                        | 40 ++++++++---------
 iris/program_logic/atomic.v                 |  8 ++--
 iris/proofmode/notation.v                   |  8 ++--
 tests/atomic.ref                            | 40 ++++++++---------
 tests/heap_lang_printing.ref                | 50 +++++++++------------
 tests/one_shot.ref                          | 18 ++++----
 tests/one_shot_once.ref                     | 20 ++++-----
 tests/proofmode.ref                         | 36 +++++++--------
 tests/proofmode_ascii.ref                   |  4 +-
 tests/proofmode_iris.ref                    |  8 ++--
 13 files changed, 128 insertions(+), 143 deletions(-)

diff --git a/iris/base_logic/lib/fancy_updates_from_vs.v b/iris/base_logic/lib/fancy_updates_from_vs.v
index a3d331e04..e6b7150aa 100644
--- a/iris/base_logic/lib/fancy_updates_from_vs.v
+++ b/iris/base_logic/lib/fancy_updates_from_vs.v
@@ -34,9 +34,7 @@ Context (vs_persistent_intro_r : ∀ E1 E2 P Q R,
 Definition fupd (E1 E2 : coPset) (P : uPred M) : uPred M :=
   ∃ R, R ∗ vs E1 E2 R P.
 
-Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q)
-  (at level 99, E1, E2 at level 50, Q at level 200,
-   format "|={ E1 , E2 }=>  Q") : bi_scope.
+Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q) : bi_scope.
 
 Global Instance fupd_ne E1 E2 : NonExpansive (@fupd E1 E2).
 Proof. solve_proper. Qed.
diff --git a/iris/bi/lib/counterexamples.v b/iris/bi/lib/counterexamples.v
index 405653f33..034ba66db 100644
--- a/iris/bi/lib/counterexamples.v
+++ b/iris/bi/lib/counterexamples.v
@@ -55,8 +55,7 @@ Module savedprop. Section savedprop.
   Implicit Types P : PROP.
 
   Context (bupd : PROP → PROP).
-  Notation "|==> Q" := (bupd Q)
-    (at level 99, Q at level 200, format "|==>  Q") : bi_scope.
+  Notation "|==> Q" := (bupd Q) : bi_scope.
 
   Hypothesis bupd_intro : ∀ P, P ⊢ |==> P.
   Hypothesis bupd_mono : ∀ P Q, (P ⊢ Q) → (|==> P) ⊢ |==> Q.
diff --git a/iris/bi/notation.v b/iris/bi/notation.v
index fa03f472b..b2f1b3845 100644
--- a/iris/bi/notation.v
+++ b/iris/bi/notation.v
@@ -34,10 +34,10 @@ which successfully undergoes automatic left-factoring. *)
 (** * BI connectives *)
 Reserved Notation "'emp'".
 Reserved Notation "'⌜' φ '⌝'" (at level 1, φ at level 200, format "⌜ φ ⌝").
-Reserved Notation "P ∗ Q" (at level 80, right associativity).
+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 ⎤".
 
@@ -76,51 +76,51 @@ Reserved Notation "'<obj>' P" (at level 20, right associativity).
 Reserved Notation "'<subj>' P" (at level 20, right associativity).
 
 (** * Update modalities *)
-Reserved Notation "|==> Q" (at level 99, Q at level 200, format "|==>  Q").
+Reserved Notation "|==> Q" (at level 99, Q at level 200, format "'[  ' |==>  '/' Q ']'").
 Reserved Notation "P ==∗ Q"
-  (at level 99, Q at level 200, format "'[' P  '/' ==∗  Q ']'").
+  (at level 99, Q at level 200, format "'[' P  ==∗  '/' Q ']'").
 
 Reserved Notation "|={ E1 , E2 }=> Q"
   (at level 99, E1, E2 at level 50, Q at level 200,
-   format "|={ 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").
+   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"
   (at level 99, E1, E2 at level 50, Q at level 200,
-   format "|={ 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").
+   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"
   (at level 99, E1, E2 at level 50, n at level 9, Q at level 200,
-   format "|={ 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").
+   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/iris/bi/weakestpre.v b/iris/bi/weakestpre.v
index c248f3411..d3ca7a42b 100644
--- a/iris/bi/weakestpre.v
+++ b/iris/bi/weakestpre.v
@@ -84,48 +84,48 @@ Notation "'{{{' P } } } e @ s ; E {{{ x .. y , 'RET' pat ; Q } } }" :=
   (□ ∀ Φ,
       P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E {{ Φ }})%I
     (at level 20, x closed binder, y closed binder,
-     format "'[hv' {{{  P  } } }  '/  ' e  '/' @  s ;  E  {{{  x  ..  y ,  RET  pat ;  Q  } } } ']'") : bi_scope.
+     format "'[hv' {{{  '[' P  ']' } } }  '/  ' e  '/' @  '[' s ;  '/' E  ']' '/' {{{  '[' x  ..  y ,  RET  pat ;  '/' Q  ']' } } } ']'") : bi_scope.
 Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
   (□ ∀ Φ,
       P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E {{ Φ }})%I
     (at level 20, x closed binder, y closed binder,
-     format "'[hv' {{{  P  } } }  '/  ' e  '/' @  E  {{{  x  ..  y ,  RET  pat ;  Q  } } } ']'") : bi_scope.
+     format "'[hv' {{{  '[' P  ']' } } }  '/  ' e  '/' @  E  '/' {{{  '[' x  ..  y ,  RET  pat ;  '/' Q  ']' } } } ']'") : bi_scope.
 Notation "'{{{' P } } } e @ E ? {{{ x .. y , 'RET' pat ; Q } } }" :=
   (□ ∀ Φ,
       P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E ?{{ Φ }})%I
     (at level 20, x closed binder, y closed binder,
-     format "'[hv' {{{  P  } } }  '/  ' e  '/' @  E  ? {{{  x  ..  y ,  RET  pat ;  Q  } } } ']'") : bi_scope.
+     format "'[hv' {{{  '[' P  ']' } } }  '/  ' e  '/' @  E  '/' ? {{{  '[' x  ..  y ,  RET  pat ;  '/' Q  ']' } } } ']'") : bi_scope.
 Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" :=
   (□ ∀ Φ,
       P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e {{ Φ }})%I
     (at level 20, x closed binder, y closed binder,
-     format "'[hv' {{{  P  } } }  '/  ' e  '/' {{{  x  ..  y ,  RET  pat ;  Q  } } } ']'") : bi_scope.
+     format "'[hv' {{{  '[' P  ']' } } }  '/  ' e  '/' {{{  '[' x  ..  y ,  RET  pat ;  '/' Q  ']' } } } ']'") : bi_scope.
 Notation "'{{{' P } } } e ? {{{ x .. y , 'RET' pat ; Q } } }" :=
   (□ ∀ Φ,
       P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e ?{{ Φ }})%I
     (at level 20, x closed binder, y closed binder,
-     format "'[hv' {{{  P  } } }  '/  ' e  '/' ? {{{  x  ..  y ,   RET  pat ;  Q  } } } ']'") : bi_scope.
+     format "'[hv' {{{  '[' P  ']' } } }  '/  ' e  '/' ? {{{  '[' x  ..  y ,   RET  pat ;  '/' Q  ']' } } } ']'") : bi_scope.
 
 Notation "'{{{' P } } } e @ s ; E {{{ 'RET' pat ; Q } } }" :=
   (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ s; E {{ Φ }})%I
     (at level 20,
-     format "'[hv' {{{  P  } } }  '/  ' e  '/' @  s ;  E  {{{  RET  pat ;  Q  } } } ']'") : bi_scope.
+     format "'[hv' {{{  '[' P  ']' } } }  '/  ' e  '/' @  '[' s ;  '/' E  ']' '/' {{{  '[' RET  pat ;  '/' Q  ']' } } } ']'") : bi_scope.
 Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
   (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E {{ Φ }})%I
     (at level 20,
-     format "'[hv' {{{  P  } } }  '/  ' e  '/' @  E  {{{  RET  pat ;  Q  } } } ']'") : bi_scope.
+     format "'[hv' {{{  '[' P  ']' } } }  '/  ' e  '/' @  E  '/' {{{  '[' RET  pat ;  '/' Q  ']' } } } ']'") : bi_scope.
 Notation "'{{{' P } } } e @ E ? {{{ 'RET' pat ; Q } } }" :=
   (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E ?{{ Φ }})%I
     (at level 20,
-     format "'[hv' {{{  P  } } }  '/  ' e  '/' @  E  ? {{{  RET  pat ;  Q  } } } ']'") : bi_scope.
+     format "'[hv' {{{  '[' P  ']' } } }  '/  ' e  '/' @  E  '/' ? {{{  '[' RET  pat ;  '/' Q  ']' } } } ']'") : bi_scope.
 Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
   (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e {{ Φ }})%I
     (at level 20,
-     format "'[hv' {{{  P  } } }  '/  ' e  '/' {{{  RET  pat ;  Q  } } } ']'") : bi_scope.
+     format "'[hv' {{{  '[' P  ']' } } }  '/  ' e  '/' {{{  '[' RET  pat ;  '/' Q  ']' } } } ']'") : bi_scope.
 Notation "'{{{' P } } } e ? {{{ 'RET' pat ; Q } } }" :=
   (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e ?{{ Φ }})%I
     (at level 20,
-     format "'[hv' {{{  P  } } }  '/  ' e  '/' ? {{{  RET  pat ;  Q  } } } ']'") : bi_scope.
+     format "'[hv' {{{  '[' P  ']' } } }  '/  ' e  '/' ? {{{  '[' RET  pat ;  '/' Q  ']' } } } ']'") : bi_scope.
 
 (** Aliases for stdpp scope -- they inherit the levels and format from above. *)
 Notation "'{{{' P } } } e @ s ; E {{{ x .. y , 'RET' pat ; Q } } }" :=
@@ -185,48 +185,48 @@ Notation "'[[{' P } ] ] e @ s ; E [[{ x .. y , 'RET' pat ; Q } ] ]" :=
   (□ ∀ Φ,
       P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E [{ Φ }])%I
     (at level 20, x closed binder, y closed binder,
-     format "'[hv' [[{  P  } ] ]  '/  ' e  '/' @  s ;  E  [[{  x  ..  y ,  RET  pat ;  Q  } ] ] ']'") : bi_scope.
+     format "'[hv' [[{  '[' P  ']' } ] ]  '/  ' e  '/' @  '[' s ;  '/' E  ']' '/' [[{  '[hv' x  ..  y ,  RET  pat ;  '/' Q  ']' } ] ] ']'") : bi_scope.
 Notation "'[[{' P } ] ] e @ E [[{ x .. y , 'RET' pat ; Q } ] ]" :=
   (□ ∀ Φ,
       P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E [{ Φ }])%I
     (at level 20, x closed binder, y closed binder,
-     format "'[hv' [[{  P  } ] ]  '/  ' e  '/' @  E  [[{  x  ..  y ,  RET  pat ;  Q  } ] ] ']'") : bi_scope.
+     format "'[hv' [[{  '[' P  ']' } ] ]  '/  ' e  '/' @  E  '/' [[{  '[hv' x  ..  y ,  RET  pat ;  '/' Q  ']' } ] ] ']'") : bi_scope.
 Notation "'[[{' P } ] ] e @ E ? [[{ x .. y , 'RET' pat ; Q } ] ]" :=
   (□ ∀ Φ,
       P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E ?[{ Φ }])%I
     (at level 20, x closed binder, y closed binder,
-     format "'[hv' [[{  P  } ] ]  '/  ' e  '/' @  E  ? [[{  x  ..  y ,  RET  pat ;  Q  } ] ] ']'") : bi_scope.
+     format "'[hv' [[{  '[' P  ']' } ] ]  '/  ' e  '/' @  E  '/' ? [[{  '[hv' x  ..  y ,  RET  pat ;  '/' Q  ']' } ] ] ']'") : bi_scope.
 Notation "'[[{' P } ] ] e [[{ x .. y , 'RET' pat ; Q } ] ]" :=
   (□ ∀ Φ,
       P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e [{ Φ }])%I
     (at level 20, x closed binder, y closed binder,
-     format "'[hv' [[{  P  } ] ]  '/  ' e  '/' [[{  x  ..  y ,  RET  pat ;  Q  } ] ] ']'") : bi_scope.
+     format "'[hv' [[{  '[' P  ']' } ] ]  '/  ' e  '/' [[{  '[hv' x  ..  y ,  RET  pat ;  '/' Q  ']' } ] ] ']'") : bi_scope.
 Notation "'[[{' P } ] ] e ? [[{ x .. y , 'RET' pat ; Q } ] ]" :=
   (□ ∀ Φ,
       P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e ?[{ Φ }])%I
     (at level 20, x closed binder, y closed binder,
-     format "'[hv' [[{  P  } ] ]  '/  ' e  '/' ? [[{  x  ..  y ,   RET  pat ;  Q  } ] ] ']'") : bi_scope.
+     format "'[hv' [[{  '[' P  ']' } ] ]  '/  ' e  '/' ? [[{  '[hv' x  ..  y ,   RET  pat ;  '/' Q  ']' } ] ] ']'") : bi_scope.
 
 Notation "'[[{' P } ] ] e @ s ; E [[{ 'RET' pat ; Q } ] ]" :=
   (□ ∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ s; E [{ Φ }])%I
     (at level 20,
-     format "'[hv' [[{  P  } ] ]  '/  ' e  '/' @  s ;  E  [[{  RET  pat ;  Q  } ] ] ']'") : bi_scope.
+     format "'[hv' [[{  '[' P  ']' } ] ]  '/  ' e  '/' @  '[' s ;  '/' E  ']' '/' [[{  '[hv' RET  pat ;  '/' Q  ']' } ] ] ']'") : bi_scope.
 Notation "'[[{' P } ] ] e @ E [[{ 'RET' pat ; Q } ] ]" :=
   (□ ∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ E [{ Φ }])%I
     (at level 20,
-     format "'[hv' [[{  P  } ] ]  '/  ' e  '/' @  E  [[{  RET  pat ;  Q  } ] ] ']'") : bi_scope.
+     format "'[hv' [[{  '[' P  ']' } ] ]  '/  ' e  '/' @  E  '/' [[{  '[hv' RET  pat ;  '/' Q  ']' } ] ] ']'") : bi_scope.
 Notation "'[[{' P } ] ] e @ E ? [[{ 'RET' pat ; Q } ] ]" :=
   (□ ∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ E ?[{ Φ }])%I
     (at level 20,
-     format "'[hv' [[{  P  } ] ]  '/  ' e  '/' @  E  ? [[{  RET  pat ;  Q  } ] ] ']'") : bi_scope.
+     format "'[hv' [[{  '[' P  ']' } ] ]  '/  ' e  '/' @  E  '/' ? [[{  '[hv' RET  pat ;  '/' Q  ']' } ] ] ']'") : bi_scope.
 Notation "'[[{' P } ] ] e [[{ 'RET' pat ; Q } ] ]" :=
   (□ ∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e [{ Φ }])%I
     (at level 20,
-     format "'[hv' [[{  P  } ] ]  '/  ' e  '/' [[{  RET  pat ;  Q  } ] ] ']'") : bi_scope.
+     format "'[hv' [[{  '[' P  ']' } ] ]  '/  ' e  '/' [[{  '[hv' RET  pat ;  '/' Q  ']' } ] ] ']'") : bi_scope.
 Notation "'[[{' P } ] ] e ? [[{ 'RET' pat ; Q } ] ]" :=
   (□ ∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e ?[{ Φ }])%I
     (at level 20,
-     format "'[hv' [[{  P  } ] ]  '/  ' e  '/' ? [[{  RET  pat ;  Q  } ] ] ']'") : bi_scope.
+     format "'[hv' [[{  '[' P  ']' } ] ]  '/  ' e  '/' ? [[{  '[hv' RET  pat ;  '/' Q  ']' } ] ] ']'") : bi_scope.
 
 (** Aliases for stdpp scope -- they inherit the levels and format from above. *)
 Notation "'[[{' P } ] ] e @ s ; E [[{ x .. y , 'RET' pat ; Q } ] ]" :=
diff --git a/iris/program_logic/atomic.v b/iris/program_logic/atomic.v
index 8feb932af..006be9ca7 100644
--- a/iris/program_logic/atomic.v
+++ b/iris/program_logic/atomic.v
@@ -42,7 +42,7 @@ Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ E '<<<' ∃ y1 .. yn , β , 'RET' v
                         ) .. )
   )
   (at level 20, E, α, β, v at level 200, x1 binder, xn binder, y1 binder, yn binder,
-   format "'[hv' '<<<'  ∀  x1  ..  xn ,  α  '>>>'  '/  ' e  @  E  '/' '[    ' '<<<'  ∃  y1  ..  yn ,  β ,  '/' 'RET'  v  '>>>' ']' ']'")
+   format "'[hv' '[     ' '<<<'  ∀  x1  ..  xn ,  α  '>>>'  ']' '/  ' e  @  E  '/' '[    ' '<<<'  ∃  y1  ..  yn ,  β ,  '/' 'RET'  v  '>>>' ']' ']'")
   : bi_scope.
 
 Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ E '<<<' β , 'RET' v '>>>'" :=
@@ -62,7 +62,7 @@ Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ E '<<<' β , 'RET' v '>>>'" :=
                         ) .. )
   )
   (at level 20, E, α, β, v at level 200, x1 binder, xn binder,
-   format "'[hv' '<<<'  ∀  x1  ..  xn ,  α  '>>>'  '/  ' e  @  E  '/' '[    ' '<<<'  β ,  '/' 'RET'  v  '>>>' ']' ']'")
+   format "'[hv' '[     ' '<<<'  ∀  x1  ..  xn ,  α  '>>>'  ']' '/  ' e  @  E  '/' '[    ' '<<<'  β ,  '/' 'RET'  v  '>>>' ']' ']'")
   : bi_scope.
 
 Notation "'<<<' α '>>>' e @ E '<<<' ∃ y1 .. yn , β , 'RET' v '>>>'" :=
@@ -79,7 +79,7 @@ Notation "'<<<' α '>>>' e @ E '<<<' ∃ y1 .. yn , β , 'RET' v '>>>'" :=
                          (λ y1, .. (λ yn, v%V) .. ))
   )
   (at level 20, E, α, β, v at level 200, y1 binder, yn binder,
-   format "'[hv' '<<<'  α  '>>>'  '/  ' e  @  E  '/' '[    ' '<<<'  ∃  y1  ..  yn ,  β ,  '/' 'RET'  v  '>>>' ']' ']'")
+   format "'[hv' '[     ' '<<<'  α  '>>>'  ']' '/  ' e  @  E  '/' '[    ' '<<<'  ∃  y1  ..  yn ,  β ,  '/' 'RET'  v  '>>>' ']' ']'")
   : bi_scope.
 
 Notation "'<<<' α '>>>' e @ E '<<<' β , 'RET' v '>>>'" :=
@@ -92,7 +92,7 @@ Notation "'<<<' α '>>>' e @ E '<<<' β , 'RET' v '>>>'" :=
              (tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) v%V)
   )
   (at level 20, E, α, β, v at level 200,
-   format "'[hv' '<<<'  α  '>>>'  '/  ' e  @  E  '/' '[    ' '<<<'  β ,  '/' 'RET'  v  '>>>' ']' ']'")
+   format "'[hv' '[     ' '<<<'  α  '>>>'  ']' '/  ' e  @  E  '/' '[    ' '<<<'  β ,  '/' 'RET'  v  '>>>' ']' ']'")
   : bi_scope.
 
 (** Theory *)
diff --git a/iris/proofmode/notation.v b/iris/proofmode/notation.v
index 0521f8a7e..0dfb1c1e5 100644
--- a/iris/proofmode/notation.v
+++ b/iris/proofmode/notation.v
@@ -19,15 +19,15 @@ Notation "Γ '_' : P" := (Esnoc Γ (IAnon _) P%I)
 Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ∗ Q" :=
   (envs_entails (Envs Γ Δ _) Q%I)
   (at level 1, Q at level 200, left associativity,
-  format "Γ '--------------------------------------' □ '//' Δ '--------------------------------------' ∗ '//' Q '//'", only printing) :
+  format "Γ '--------------------------------------' □ '//' Δ '--------------------------------------' ∗ '//' '[' Q ']' '//'", only printing) :
   stdpp_scope.
 Notation "Δ '--------------------------------------' ∗ Q" :=
   (envs_entails (Envs Enil Δ _) Q%I)
   (at level 1, Q at level 200, left associativity,
-  format "Δ '--------------------------------------' ∗ '//' Q '//'", only printing) : stdpp_scope.
+  format "Δ '--------------------------------------' ∗ '//' '[' Q ']' '//'", only printing) : stdpp_scope.
 Notation "Γ '--------------------------------------' □ Q" :=
   (envs_entails (Envs Γ Enil _) Q%I)
   (at level 1, Q at level 200, left associativity,
-  format "Γ '--------------------------------------' □ '//' Q '//'", only printing)  : stdpp_scope.
+  format "Γ '--------------------------------------' □ '//' '[' Q ']' '//'", only printing)  : stdpp_scope.
 Notation "'--------------------------------------' ∗ Q" := (envs_entails (Envs Enil Enil _) Q%I)
-  (at level 1, Q at level 200, format "'--------------------------------------' ∗ '//' Q '//'", only printing) : stdpp_scope.
+  (at level 1, Q at level 200, format "'--------------------------------------' ∗ '//' '[' Q ']' '//'", only printing) : stdpp_scope.
diff --git a/tests/atomic.ref b/tests/atomic.ref
index bd5518b0b..fba1915ac 100644
--- a/tests/atomic.ref
+++ b/tests/atomic.ref
@@ -177,7 +177,7 @@
   heapGS0 : heapGS Σ
   l : loc
   ============================
-  ⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x >>>
+  ⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x >>> 
       code @ ∅
     <<< ∃ y : val, l ↦ y, RET #() >>>
 1 goal
@@ -198,7 +198,7 @@
   heapGS0 : heapGS Σ
   l : loc
   ============================
-  ⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
+  ⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> 
       code @ ∅
     <<< ∃ y : val, l ↦ y, RET #() >>>
 1 goal
@@ -219,7 +219,7 @@
   heapGS0 : heapGS Σ
   l : loc
   ============================
-  ⊢ <<< ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
+  ⊢ <<< ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> 
       code @ ∅
     <<< ∃ yyyy : val, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
         RET #() >>>
@@ -232,9 +232,8 @@
   ============================
   _ : AU << ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> 
          @ ⊤ ∖ ∅, ∅ 
-         << ∃ yyyy : val, l ↦ yyyy
-                          ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
-            COMM Φ #() >>
+         << ∃ yyyy : val, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗
+            l ↦ xx, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -244,7 +243,7 @@
   heapGS0 : heapGS Σ
   l : loc
   ============================
-  ⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
+  ⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> 
       code @ ∅
     <<< l ↦ x, RET #() >>>
 1 goal
@@ -266,7 +265,7 @@
   l : loc
   x : val
   ============================
-  ⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
+  ⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> 
       code @ ∅
     <<< ∃ y : val, l ↦ y, RET #() >>>
 1 goal
@@ -289,7 +288,7 @@
   l : loc
   x : val
   ============================
-  ⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
+  ⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> 
       code @ ∅
     <<< l ↦ #(), RET #() >>>
 1 goal
@@ -312,7 +311,7 @@
   l : loc
   xx, yyyy : val
   ============================
-  ⊢ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
+  ⊢ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> 
       code @ ∅
     <<< l ↦ yyyy, RET #() >>>
 1 goal
@@ -323,8 +322,8 @@
   xx, yyyy : val
   Φ : language.val heap_lang → iProp Σ
   ============================
-  "AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>
-            @ ⊤ ∖ ∅, ∅ << l ↦ yyyy, COMM Φ #() >>
+  "AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗
+            l ↦ xx >> @ ⊤ ∖ ∅, ∅ << l ↦ yyyy, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -335,7 +334,7 @@
   l : loc
   xx, yyyy : val
   ============================
-  ⊢ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
+  ⊢ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> 
       code @ ∅
     <<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
         RET #() >>>
@@ -348,8 +347,8 @@
   Φ : language.val heap_lang → iProp Σ
   ============================
   "AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤ ∖ ∅, ∅ 
-            << l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
-               COMM Φ #() >>
+            << l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗
+               l ↦ xx, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -362,12 +361,11 @@
   P : val → iProp Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  "AU" : ∃ x : val,
-           P x
-           ∗ (P x
-              ={∅,⊤}=∗ AU << ∀ x0 : val, P x0 >> @ ⊤ ∖ ∅, ∅ 
-                          << ∃ y : val, P y, COMM Φ #() >>)
-             ∧ (∀ x0 : val, P x0 ={∅,⊤}=∗ Φ #())
+  "AU" : ∃ x : val, P x ∗
+           (P x ={∅,⊤}=∗
+            AU << ∀ x0 : val, P x0 >> @ ⊤ ∖ ∅, ∅ 
+               << ∃ y : val, P y, COMM Φ #() >>)
+           ∧ (∀ x0 : val, P x0 ={∅,⊤}=∗ Φ #())
   --------------------------------------∗
   WP ! #0 @ ∅ {{ v, |={∅,⊤}=> Φ v }}
   
diff --git a/tests/heap_lang_printing.ref b/tests/heap_lang_printing.ref
index d45a1612f..596127e1b 100644
--- a/tests/heap_lang_printing.ref
+++ b/tests/heap_lang_printing.ref
@@ -44,9 +44,8 @@
   WP let: "val1" := fun1 #() in
      let: "val2" := fun2 "val1" in
      let: "v" := fun3 "v" in if: "v" = "v" then "v" else "v"
-  {{ _,
-     long_post
-     ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post }}
+  {{ _, long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗
+     long_post ∗ long_post }}
   
 1 goal
   
@@ -61,10 +60,8 @@
      WP let: "val1" := v in
         let: "val2" := fun2 "val1" in
         let: "v" := fun3 "v" in if: "v" = "v" then "v" else "v"
-     {{ _,
-        long_post
-        ∗ long_post
-          ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post }} }}
+     {{ _, long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗
+        long_post ∗ long_post }} }}
   
 1 goal
   
@@ -83,9 +80,8 @@
      let: "val2" := fun2 "val1" in
      let: "v" := fun3 "v" in if: "v" = "v" then "v" else "v"
   @ E_long
-  {{ _,
-     long_post
-     ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post }}
+  {{ _, long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗
+     long_post ∗ long_post }}
   
 1 goal
   
@@ -107,10 +103,8 @@
         let: "val2" := fun2 "val1" in
         let: "v" := fun3 "v" in if: "v" = "v" then "v" else "v"
      @ E_long
-     {{ _,
-        long_post
-        ∗ long_post
-          ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post }} }}
+     {{ _, long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗
+        long_post ∗ long_post }} }}
   
 1 goal
   
@@ -127,18 +121,13 @@
   WP ! #l1
   @ E_long ∖ ↑N
   {{ v,
-     |={E_long ∖ ↑N}=> ▷ True
-                       ∗ WP let: "val1" := v in
-                            let: "val2" := fun2 "val1" in
-                            let: "v" := fun3 "v" in
-                            if: "v" = "v" then "v" else "v"
-                         @ E_long
-                         {{ _,
-                            long_post
-                            ∗ long_post
-                              ∗ long_post
-                                ∗ long_post
-                                  ∗ long_post ∗ long_post ∗ long_post }} }}
+     |={E_long ∖ ↑N}=> ▷ True ∗
+       WP let: "val1" := v in
+          let: "val2" := fun2 "val1" in
+          let: "v" := fun3 "v" in if: "v" = "v" then "v" else "v"
+       @ E_long
+       {{ _, long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗
+          long_post ∗ long_post }} }}
   
 1 goal
   
@@ -162,8 +151,8 @@
     let: "val1" := fun1 #() in
     let: "val2" := fun2 "val1" in
     let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
-  @ E_mask_is_long_too {{{ (x y : val) (z : Z), RET 
-  (x, y, #z); True }}}
+  @ E_mask_is_long_too
+  {{{ (x y : val) (z : Z), RET (x, y, #z); True }}}
 1 goal
   
   Σ : gFunctors
@@ -176,5 +165,6 @@
     let: "val1" := fun1 #() in
     let: "val2" := fun2 "val1" in
     let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
-  @ E_mask_is_long_too {{{ (x y : val) (z : Z), RET 
-  (x, y, #z); long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post }}}
+  @ E_mask_is_long_too
+  {{{ (x y : val) (z : Z), RET (x, y, #z); long_post ∗ long_post ∗
+      long_post ∗ long_post ∗ long_post }}}
diff --git a/tests/one_shot.ref b/tests/one_shot.ref
index a4b6aa006..bd5c8d7fe 100644
--- a/tests/one_shot.ref
+++ b/tests/one_shot.ref
@@ -13,9 +13,9 @@
   "Hl" : l ↦ InjLV #()
   _ : own γ Pending
   --------------------------------------∗
-  one_shot_inv γ l
-  ∗ (⌜InjLV #() = InjLV #()⌝
-     ∨ (∃ n : Z, ⌜InjLV #() = InjRV #n⌝ ∗ own γ (Shot n)))
+  one_shot_inv γ l ∗
+  (⌜InjLV #() = InjLV #()⌝
+   ∨ (∃ n : Z, ⌜InjLV #() = InjRV #n⌝ ∗ own γ (Shot n)))
   
 1 goal
   
@@ -34,11 +34,11 @@
   "Hl" : l ↦ InjRV #m'
   "Hγ" : own γ (Shot m')
   --------------------------------------∗
-  |={⊤ ∖ ↑N}=> ▷ one_shot_inv γ l
-               ∗ WP match: InjRV #m' with
-                      InjL <> => assert: #false
-                    | InjR "m" => assert: #m = "m"
-                    end
-                 {{ _, True }}
+  |={⊤ ∖ ↑N}=> ▷ one_shot_inv γ l ∗
+    WP match: InjRV #m' with
+         InjL <> => assert: #false
+       | InjR "m" => assert: #m = "m"
+       end
+    {{ _, True }}
   
 Closed under the global context
diff --git a/tests/one_shot_once.ref b/tests/one_shot_once.ref
index 5fb4112bd..48311b6a3 100644
--- a/tests/one_shot_once.ref
+++ b/tests/one_shot_once.ref
@@ -13,9 +13,9 @@
   "Hl" : l ↦ InjLV #()
   _ : own γ (Pending (1 / 2))
   --------------------------------------∗
-  one_shot_inv γ l
-  ∗ (⌜InjLV #() = InjLV #()⌝
-     ∨ (∃ n : Z, ⌜InjLV #() = InjRV #n⌝ ∗ own γ (Shot n)))
+  one_shot_inv γ l ∗
+  (⌜InjLV #() = InjLV #()⌝
+   ∨ (∃ n : Z, ⌜InjLV #() = InjRV #n⌝ ∗ own γ (Shot n)))
   
 1 goal
   
@@ -34,11 +34,11 @@
   "Hl" : l ↦ InjRV #m'
   "Hγ" : own γ (Shot m')
   --------------------------------------∗
-  |={⊤ ∖ ↑N}=> ▷ one_shot_inv γ l
-               ∗ WP let: "y'" := InjRV #m' in
-                    match: InjRV #m with
-                      InjL <> => #()
-                    | InjR <> => assert: InjRV #m = "y'"
-                    end
-                 {{ _, True }}
+  |={⊤ ∖ ↑N}=> ▷ one_shot_inv γ l ∗
+    WP let: "y'" := InjRV #m' in
+       match: InjRV #m with
+         InjL <> => #()
+       | InjR <> => assert: InjRV #m = "y'"
+       end
+    {{ _, True }}
   
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index ac5e9cf57..ce883c7eb 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -310,8 +310,8 @@ Tactic failure: iFrame: cannot frame Q.
   ============================
   "HP" : P
   _ : [∗ list] y1;y2 ∈ [];l2, <affine> ⌜y1 = y2⌝
-  _ : <affine> ⌜x1 = x2⌝
-      ∗ ([∗ list] y1;y2 ∈ l1;(l2 ++ l2), <affine> ⌜y1 = y2⌝)
+  _ : <affine> ⌜x1 = x2⌝ ∗
+      ([∗ list] y1;y2 ∈ l1;(l2 ++ l2), <affine> ⌜y1 = y2⌝)
   --------------------------------------∗
   P ∨ True ∗ ([∗ list] _;_ ∈ l1;l2, True)
   
@@ -418,8 +418,8 @@ Tactic failure: iFrame: cannot frame Q.
   BiFUpd0 : BiFUpd PROP
   P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP
   ============================
-  "HP" : P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P
-         ∗ P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P
+  "HP" : P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P ∗
+         P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P
   --------------------------------------∗
   True
   
@@ -429,8 +429,8 @@ Tactic failure: iFrame: cannot frame Q.
   BiFUpd0 : BiFUpd PROP
   P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP
   ============================
-  _ : P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P
-      ∗ P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P
+  _ : P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P ∗
+      P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P
   --------------------------------------∗
   True
   
@@ -467,8 +467,8 @@ Tactic failure: iFrame: cannot frame Q.
   PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
   ============================
   --------------------------------------∗
-  PPPPPPPPPPPPPPPPP
-  → QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
+  PPPPPPPPPPPPPPPPP → QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗
+  QQQQQQQQQQQQQQQQQQ
   
 "long_impl_nested"
      : string
@@ -492,8 +492,8 @@ Tactic failure: iFrame: cannot frame Q.
   PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
   ============================
   --------------------------------------∗
-  PPPPPPPPPPPPPPPPP
-  -∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
+  PPPPPPPPPPPPPPPPP -∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗
+  QQQQQQQQQQQQQQQQQQ
   
 "long_wand_nested"
      : string
@@ -504,9 +504,9 @@ Tactic failure: iFrame: cannot frame Q.
   PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
   ============================
   --------------------------------------∗
-  PPPPPPPPPPPPPPPPP
-  -∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
-     -∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
+  PPPPPPPPPPPPPPPPP -∗
+  QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ -∗
+  QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
   
 "long_fupd"
      : string
@@ -518,8 +518,8 @@ Tactic failure: iFrame: cannot frame Q.
   PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
   ============================
   --------------------------------------∗
-  PPPPPPPPPPPPPPPPP
-  ={E}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
+  PPPPPPPPPPPPPPPPP ={E}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗
+  QQQQQQQQQQQQQQQQQQ
   
 "long_fupd_nested"
      : string
@@ -531,9 +531,9 @@ Tactic failure: iFrame: cannot frame Q.
   PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
   ============================
   --------------------------------------∗
-  PPPPPPPPPPPPPPPPP
-  ={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
-             ={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
+  PPPPPPPPPPPPPPPPP ={E1,E2}=∗
+  QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ={E1,E2}=∗
+  QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
   
 "iStopProof_not_proofmode"
      : string
diff --git a/tests/proofmode_ascii.ref b/tests/proofmode_ascii.ref
index b0d84bf2c..a1843eb61 100644
--- a/tests/proofmode_ascii.ref
+++ b/tests/proofmode_ascii.ref
@@ -83,8 +83,8 @@
   "Hown1" : na_own t E1
   "Hown2" : na_own t (E2 ∖ ↑N)
   --------------------------------------∗
-  |={⊤}=> (▷ <pers> P ∗ na_own t (E2 ∖ ↑N))
-          ∗ (na_own t E2 ={⊤}=∗ na_own t E1 ∗ na_own t E2 ∗ ▷ P)
+  |={⊤}=> (▷ <pers> P ∗ na_own t (E2 ∖ ↑N)) ∗
+    (na_own t E2 ={⊤}=∗ na_own t E1 ∗ na_own t E2 ∗ ▷ P)
   
 1 goal
   
diff --git a/tests/proofmode_iris.ref b/tests/proofmode_iris.ref
index d049912e2..4d3be4eae 100644
--- a/tests/proofmode_iris.ref
+++ b/tests/proofmode_iris.ref
@@ -95,8 +95,8 @@
   "Hown1" : na_own t E1
   "Hown2" : na_own t (E2 ∖ ↑N)
   --------------------------------------∗
-  |={⊤}=> (▷ <pers> P ∗ na_own t (E2 ∖ ↑N))
-          ∗ (na_own t E2 ={⊤}=∗ na_own t E1 ∗ na_own t E2 ∗ ▷ P)
+  |={⊤}=> (▷ <pers> P ∗ na_own t (E2 ∖ ↑N)) ∗
+    (na_own t E2 ={⊤}=∗ na_own t E1 ∗ na_own t E2 ∗ ▷ P)
   
 1 goal
   
@@ -110,8 +110,8 @@
   P : iProp Σ
   ============================
   ↑N ⊆ E2
-  → na_inv t N (<pers> P) ∗ na_own t E1 ∗ na_own t E2
-    ={⊤}=∗ na_own t E1 ∗ na_own t E2 ∗ ▷ P
+  → 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
   
   Σ : gFunctors
-- 
GitLab