diff --git a/CHANGELOG.md b/CHANGELOG.md
index 8ab690b221c42bac4b28759e9fc523b67967b37e..e69ff3934039fa81c3584a6aca2f4c474bbc04ae 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -68,6 +68,9 @@ Coq 8.11 is no longer supported in this version of Iris.
   by combining the embeddings of `PROP1` into `PROP2` and `PROP2` into `PROP3`.
   This construct is *not* declared as an instance to avoid TC search divergence.
   (by Hai Dang, BedRock Systems)
+* Improve notation printing around `WP`, Texan triples, and logically atomic triples.
+* Slight change to the `AACC` notation for atomic accessors (which is usually
+  only printed, not parsed): added a `,` before `ABORT`, for consistency with `COMM`.
 
 **Changes in `proofmode`:**
 
diff --git a/iris/base_logic/lib/fancy_updates_from_vs.v b/iris/base_logic/lib/fancy_updates_from_vs.v
index 1be809580332bb8ba2e5532eaa2b4d97d49a344f..b6e55d18b54a055e33f78c0c0a29df03595b9aa9 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/atomic.v b/iris/bi/lib/atomic.v
index 44e01693b37efaeaba7eb0f2d6de5772d97d25ac..9327bd16848b86b2c740be91295a1f0f6aee0640 100644
--- a/iris/bi/lib/atomic.v
+++ b/iris/bi/lib/atomic.v
@@ -113,7 +113,7 @@ Notation "'AU' '<<' ∀ x1 .. xn , α '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'C
                         ) .. )
   )
   (at level 20, Eo, Ei, α, β, Φ at level 200, x1 binder, xn binder, y1 binder, yn binder,
-   format "'[   ' 'AU'  '<<'  ∀  x1  ..  xn ,  α  '>>'  '/' '[' @  Eo ,  Ei  ']' '/' '[   ' '<<'  ∃  y1  ..  yn ,  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.
+   format "'[hv   ' 'AU'  '<<'  '[' ∀  x1  ..  xn ,  '/' α  ']' '>>'  '/' @  '[' Eo ,  '/' Ei  ']' '/' '<<'  '[' ∃  y1  ..  yn ,  '/' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
 
 Notation "'AU' '<<' ∀ x1 .. xn , α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
   (atomic_update (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
@@ -127,7 +127,7 @@ Notation "'AU' '<<' ∀ x1 .. xn , α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :
                        λ x1, .. (λ xn, tele_app (TT:=TeleO) Φ%I) .. )
   )
   (at level 20, Eo, Ei, α, β, Φ at level 200, x1 binder, xn binder,
-   format "'[   ' 'AU'  '<<'  ∀  x1  ..  xn ,  α  '>>'  '/' '[' @  Eo ,  Ei  ']' '/' '[   ' '<<'  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.
+   format "'[hv   ' 'AU'  '<<'  '[' ∀  x1  ..  xn ,  '/' α  ']' '>>'  '/' @  '[' Eo ,  '/' Ei  ']' '/' '<<'  '[' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
 
 Notation "'AU' '<<' α '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :=
   (atomic_update (TA:=TeleO)
@@ -142,7 +142,7 @@ Notation "'AU' '<<' α '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :
                                 (λ y1, .. (λ yn, Φ%I) ..))
   )
   (at level 20, Eo, Ei, α, β, Φ at level 200, y1 binder, yn binder,
-   format "'[   ' 'AU'  '<<'  α  '>>'  '/' '[' @  Eo ,  Ei  ']' '/' '[   ' '<<'  ∃  y1  ..  yn ,  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.
+   format "'[hv   ' 'AU'  '<<'  '[' α  ']' '>>'  '/' @  '[' Eo ,  '/' Ei  ']' '/' '<<'  '[' ∃  y1  ..  yn ,  '/' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
 
 Notation "'AU' '<<' α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
   (atomic_update (TA:=TeleO) (TB:=TeleO) Eo Ei
@@ -151,10 +151,10 @@ Notation "'AU' '<<' α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
                  (tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) Φ%I)
   )
   (at level 20, Eo, Ei, α, β, Φ at level 200,
-   format "'[   ' 'AU'  '<<'  α  '>>'  '/' '[' @  Eo ,  Ei  ']' '/' '[   ' '<<'  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.
+   format "'[hv   ' 'AU'  '<<'  '[' α  ']' '>>'  '/' @  '[' Eo ,  '/' Ei  ']' '/' '<<'  '[' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
 
 (** Notation: Atomic accessors *)
-Notation "'AACC' '<<' ∀ x1 .. xn , α 'ABORT' P '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :=
+Notation "'AACC' '<<' ∀ x1 .. xn , α , 'ABORT' P '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :=
   (atomic_acc (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
               (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
               Eo Ei
@@ -173,9 +173,9 @@ Notation "'AACC' '<<' ∀ x1 .. xn , α 'ABORT' P '>>' @ Eo , Ei '<<' ∃ y1 ..
                      ) .. )
   )
   (at level 20, Eo, Ei, α, P, β, Φ at level 200, x1 binder, xn binder, y1 binder, yn binder,
-   format "'[     ' 'AACC'  '[   ' '<<'  ∀  x1  ..  xn ,  α  '/' ABORT  P  '>>'  ']' '/' '[' @  Eo ,  Ei  ']' '/' '[   ' '<<'  ∃  y1  ..  yn ,  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.
+   format "'[hv     ' 'AACC'  '<<'  '[' ∀  x1  ..  xn ,  '/' α ,  '/' ABORT  P  ']' '>>'  '/' @  '[' Eo ,  '/' Ei  ']' '/' '<<'  '[' ∃  y1  ..  yn ,  '/' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
 
-Notation "'AACC' '<<' ∀ x1 .. xn , α 'ABORT' P '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
+Notation "'AACC' '<<' ∀ x1 .. xn , α , 'ABORT' P '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
   (atomic_acc (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
               (TB:=TeleO)
               Eo Ei
@@ -188,9 +188,9 @@ Notation "'AACC' '<<' ∀ x1 .. xn , α 'ABORT' P '>>' @ Eo , Ei '<<' β , 'COMM
                         λ x1, .. (λ xn, tele_app (TT:=TeleO) Φ%I) .. )
   )
   (at level 20, Eo, Ei, α, P, β, Φ at level 200, x1 binder, xn binder,
-   format "'[     ' 'AACC'  '[   ' '<<'  ∀  x1  ..  xn ,  α  '/' ABORT  P  '>>'  ']' '/' '[' @  Eo ,  Ei  ']' '/' '[   ' '<<'  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.
+   format "'[hv     ' 'AACC'  '<<'  '[' ∀  x1  ..  xn ,  '/' α ,  '/' ABORT  P  ']' '>>'  '/' @  '[' Eo ,  '/' Ei  ']' '/' '<<'  '[' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
 
-Notation "'AACC' '<<' α 'ABORT' P '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :=
+Notation "'AACC' '<<' α , 'ABORT' P '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :=
   (atomic_acc (TA:=TeleO)
               (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
               Eo Ei
@@ -204,9 +204,9 @@ Notation "'AACC' '<<' α 'ABORT' P '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM
                         (λ y1, .. (λ yn, Φ%I) ..))
   )
   (at level 20, Eo, Ei, α, P, β, Φ at level 200, y1 binder, yn binder,
-   format "'[     ' 'AACC'  '[   ' '<<'  α  '/' ABORT  P  '>>'  ']' '/' '[' @  Eo ,  Ei  ']' '/' '[   ' '<<'  ∃  y1  ..  yn ,  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.
+   format "'[hv     ' 'AACC'  '<<'  '[' α ,  '/' ABORT  P  ']' '>>'  '/' @  '[' Eo ,  '/' Ei  ']' '/' '<<'  '[' ∃  y1  ..  yn ,  '/' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
 
-Notation "'AACC' '<<' α 'ABORT' P '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
+Notation "'AACC' '<<' α , 'ABORT' P '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
   (atomic_acc (TA:=TeleO)
               (TB:=TeleO)
               Eo Ei
@@ -216,7 +216,7 @@ Notation "'AACC' '<<' α 'ABORT' P '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
                  (tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) Φ%I)
   )
   (at level 20, Eo, Ei, α, P, β, Φ at level 200,
-   format "'[     ' 'AACC'  '[   ' '<<'  α  '/' ABORT  P  '>>'  ']' '/' '[' @  Eo ,  Ei  ']' '/' '[   ' '<<'  β ,  '/' COMM  Φ  '>>' ']' ']'") : bi_scope.
+   format "'[hv     ' 'AACC'  '<<'  '[' α ,  '/' ABORT  P  ']' '>>'  '/' @  '[' Eo ,  '/' Ei  ']' '/' '<<'  '[' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
 
 (** Lemmas about AU *)
 Section lemmas.
diff --git a/iris/bi/lib/counterexamples.v b/iris/bi/lib/counterexamples.v
index 534a2e559275610eb36c58cc8f659d155b6d9e15..05995a0d4e7c612903c5bf2f5513c26fbe156196 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 fa03f472ba206e15ae9998bbe8049b64f5710c1c..b2f1b3845c380df1f64a638ae5c62f39cec58ce5 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 b2c248e6b5db44cf5fa4dfda60663115b7a744c9..d3ca7a42bd8f223b2f8710f6586e9c5e025a8660 100644
--- a/iris/bi/weakestpre.v
+++ b/iris/bi/weakestpre.v
@@ -56,72 +56,76 @@ Notation "'WP' e {{ Φ } }" := (wp NotStuck ⊤ e%E Φ)
 Notation "'WP' e ? {{ Φ } }" := (wp MaybeStuck ⊤ e%E Φ)
   (at level 20, e, Φ at level 200, only parsing) : bi_scope.
 
-(** Notations with binder.  The indentation for the inner format block is chosen
-such that *if* one has a single-character mask (e.g. [E]), the second line
-should align with the binder(s) on the first line. *)
+(** Notations with binder. *)
+(** The general approach we use for all these complex notations: an outer '[hv'
+to switch bwteen "horizontal mode" where it all fits on one line, and "vertical
+mode" where each '/' becomes a line break. Then, as appropriate, nested boxes
+('['...']') for things like preconditions and postconditions such that they are
+maximally horizontal and suitably indented inside the parentheses that surround
+them. *)
 Notation "'WP' e @ s ; E {{ v , Q } }" := (wp s E e%E (λ v, Q))
   (at level 20, e, Q at level 200,
-   format "'[' 'WP'  e  '/' '[          ' @  s ;  E  {{  v ,  Q  } } ']' ']'") : bi_scope.
+   format "'[hv' 'WP'  e  '/' @  '[' s ;  '/' E  ']' '/' {{  '[' v ,  '/' Q  ']' } } ']'") : bi_scope.
 Notation "'WP' e @ E {{ v , Q } }" := (wp NotStuck E e%E (λ v, Q))
   (at level 20, e, Q at level 200,
-   format "'[' 'WP'  e  '/' '[       ' @  E  {{  v ,  Q  } } ']' ']'") : bi_scope.
+   format "'[hv' 'WP'  e  '/' @  E  '/' {{  '[' v ,  '/' Q  ']' } } ']'") : bi_scope.
 Notation "'WP' e @ E ? {{ v , Q } }" := (wp MaybeStuck E e%E (λ v, Q))
   (at level 20, e, Q at level 200,
-   format "'[' 'WP'  e  '/' '[        ' @  E  ? {{  v ,  Q  } } ']' ']'") : bi_scope.
+   format "'[hv' 'WP'  e  '/' @  E  '/' ? {{  '[' v ,  '/' Q  ']' } } ']'") : bi_scope.
 Notation "'WP' e {{ v , Q } }" := (wp NotStuck ⊤ e%E (λ v, Q))
   (at level 20, e, Q at level 200,
-   format "'[' 'WP'  e  '/' '[   ' {{  v ,  Q  } } ']' ']'") : bi_scope.
+   format "'[hv' 'WP'  e  '/' {{  '[' v ,  '/' Q  ']' } } ']'") : bi_scope.
 Notation "'WP' e ? {{ v , Q } }" := (wp MaybeStuck ⊤ e%E (λ v, Q))
   (at level 20, e, Q at level 200,
-   format "'[' 'WP'  e  '/' '[    ' ? {{  v ,  Q  } } ']' ']'") : bi_scope.
+   format "'[hv' 'WP'  e  '/' ? {{  '[' v ,  '/' Q  ']' } } ']'") : bi_scope.
 
 (* Texan triples *)
 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 } } }" :=
@@ -159,72 +163,70 @@ Notation "'WP' e [{ Φ } ]" := (twp NotStuck ⊤ e%E Φ)
 Notation "'WP' e ? [{ Φ } ]" := (twp MaybeStuck ⊤ e%E Φ)
   (at level 20, e, Φ at level 200, only parsing) : bi_scope.
 
-(** Notations with binder.  The indentation for the inner format block is chosen
-such that *if* one has a single-character mask (e.g. [E]), the second line
-should align with the binder(s) on the first line. *)
+(** Notations with binder. *)
 Notation "'WP' e @ s ; E [{ v , Q } ]" := (twp s E e%E (λ v, Q))
   (at level 20, e, Q at level 200,
-   format "'[' 'WP'  e  '/' '[          ' @  s ;  E  [{  v ,  Q  } ] ']' ']'") : bi_scope.
+   format "'[hv' 'WP'  e  '/' @  '[' s ;  '/' E  ']' '/' [{  '[' v ,  '/' Q  ']' } ] ']'") : bi_scope.
 Notation "'WP' e @ E [{ v , Q } ]" := (twp NotStuck E e%E (λ v, Q))
   (at level 20, e, Q at level 200,
-   format "'[' 'WP'  e  '/' '[       ' @  E  [{  v ,  Q  } ] ']' ']'") : bi_scope.
+   format "'[hv' 'WP'  e  '/' @  E  '/' [{  '[' v ,  '/' Q  ']' } ] ']'") : bi_scope.
 Notation "'WP' e @ E ? [{ v , Q } ]" := (twp MaybeStuck E e%E (λ v, Q))
   (at level 20, e, Q at level 200,
-   format "'[' 'WP'  e  '/' '[        ' @  E  ? [{  v ,  Q  } ] ']' ']'") : bi_scope.
+   format "'[hv' 'WP'  e  '/' @  E  '/' ? [{  '[' v ,  '/' Q  ']' } ] ']'") : bi_scope.
 Notation "'WP' e [{ v , Q } ]" := (twp NotStuck ⊤ e%E (λ v, Q))
   (at level 20, e, Q at level 200,
-   format "'[' 'WP'  e  '/' '[   ' [{  v ,  Q  } ] ']' ']'") : bi_scope.
+   format "'[hv' 'WP'  e  '/' [{  '[' v ,  '/' Q  ']' } ] ']'") : bi_scope.
 Notation "'WP' e ? [{ v , Q } ]" := (twp MaybeStuck ⊤ e%E (λ v, Q))
   (at level 20, e, Q at level 200,
-   format "'[' 'WP'  e  '/' '[    ' ? [{  v ,  Q  } ] ']' ']'") : bi_scope.
+   format "'[hv' 'WP'  e  '/' ? [{  '[' v ,  '/' Q  ']' } ] ']'") : bi_scope.
 
 (* Texan triples *)
 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 1ca7a0f1ea390c00f8f2396a7b36587a7d5c770b..9d201ebd80293d41d3a51ef3bfbc9ca00ad5892e 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 0521f8a7e367bc94f6588fb9982edd3f9f14f70c..0dfb1c1e5ff3decaf2f4e1ccc3d628cf0a191122 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 bd5518b0b7d3fbd25928c5f94bd4e4d01009c6a5..532b1a1366e993cbcc9fdb19a513d70b0439f853 100644
--- a/tests/atomic.ref
+++ b/tests/atomic.ref
@@ -9,8 +9,9 @@
   ============================
   "Hl" : l ↦ v
   --------------------------------------∗
-  AACC << ∀ (v0 : val) (q : dfrac), l ↦{q} v0 ABORT l ↦ v >> 
-       @ ⊤ ∖ ∅, ∅ << l ↦{q} v0, COMM Q -∗ Q >>
+  AACC << ∀ (v0 : val) (q : dfrac), l ↦{q} v0, ABORT l ↦ v >>
+       @ ⊤ ∖ ∅, ∅ 
+       << l ↦{q} v0, COMM Q -∗ Q >>
   
 "non_laterable"
      : string
@@ -24,8 +25,9 @@
   ============================
   "HP" : â–· P
   --------------------------------------∗
-  AACC << ∀ (v : val) (q : dfrac), l ↦{q} v ABORT ▷ P >> 
-       @ ⊤ ∖ ∅, ∅ << l ↦{q} v, COMM True >>
+  AACC << ∀ (v : val) (q : dfrac), l ↦{q} v, ABORT ▷ P >>
+       @ ⊤ ∖ ∅, ∅ 
+       << l ↦{q} v, COMM True >>
   
 1 goal
   
@@ -37,8 +39,9 @@
   ============================
   "HP" : â–· P
   --------------------------------------∗
-  AACC << ∀ (v : val) (q : dfrac), l ↦{q} v ABORT ▷ P >> 
-       @ ⊤ ∖ ∅, ∅ << l ↦{q} v, COMM True >>
+  AACC << ∀ (v : val) (q : dfrac), l ↦{q} v, ABORT ▷ P >>
+       @ ⊤ ∖ ∅, ∅ 
+       << l ↦{q} v, COMM True >>
   
 "printing"
      : string
@@ -67,10 +70,12 @@
   P : val → iProp Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : AACC << ∀ x : val, P x
-              ABORT AU << ∀ x : val, P x >> @ ⊤ ∖ ∅, ∅ 
-                       << ∃ y : val, P y, COMM Φ #() >> >> 
-           @ ⊤ ∖ ∅, ∅ << ∃ y : val, P y, COMM Φ #() >>
+  _ : AACC << ∀ x : val, P x,
+              ABORT AU << ∀ x : val, P x >>
+                       @ ⊤ ∖ ∅, ∅ 
+                       << ∃ y : val, P y, COMM Φ #() >> >>
+           @ ⊤ ∖ ∅, ∅ 
+           << ∃ y : val, P y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -99,10 +104,12 @@
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : AACC << ∀ x : val, l ↦ x
-              ABORT AU << ∀ x : val, l ↦ x >> @ ⊤ ∖ ∅, ∅ 
-                       << l ↦ x, COMM Φ #() >> >> 
-           @ ⊤ ∖ ∅, ∅ << l ↦ x, COMM Φ #() >>
+  _ : AACC << ∀ x : val, l ↦ x,
+              ABORT AU << ∀ x : val, l ↦ x >>
+                       @ ⊤ ∖ ∅, ∅ 
+                       << l ↦ x, COMM Φ #() >> >>
+           @ ⊤ ∖ ∅, ∅ 
+           << l ↦ x, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -131,10 +138,12 @@
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : AACC << l ↦ #()
-              ABORT AU << l ↦ #() >> @ ⊤ ∖ ∅, ∅ 
-                       << ∃ y : val, l ↦ y, COMM Φ #() >> >> 
-           @ ⊤ ∖ ∅, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >>
+  _ : AACC << l ↦ #(),
+              ABORT AU << l ↦ #() >>
+                       @ ⊤ ∖ ∅, ∅ 
+                       << ∃ y : val, l ↦ y, COMM Φ #() >> >>
+           @ ⊤ ∖ ∅, ∅ 
+           << ∃ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -163,9 +172,10 @@
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : AACC << l ↦ #()
-              ABORT AU << l ↦ #() >> @ ⊤ ∖ ∅, ∅ << l ↦ #(), COMM Φ #() >> >> 
-           @ ⊤ ∖ ∅, ∅ << l ↦ #(), COMM Φ #() >>
+  _ : AACC << l ↦ #(),
+              ABORT AU << l ↦ #() >> @ ⊤ ∖ ∅, ∅ << l ↦ #(), COMM Φ #() >> >>
+           @ ⊤ ∖ ∅, ∅ 
+           << l ↦ #(), COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -187,7 +197,8 @@
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
-  "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x >> @ ⊤ ∖ ∅, ∅ 
+  "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x >>
+            @ ⊤ ∖ ∅, ∅ 
             << ∃ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
@@ -209,7 +220,8 @@
   Φ : language.val heap_lang → iProp Σ
   ============================
   "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
-            @ ⊤ ∖ ∅, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >>
+            @ ⊤ ∖ ∅, ∅ 
+            << ∃ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -230,11 +242,10 @@
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : AU << ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> 
+  _ : 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 }}
   
@@ -254,8 +265,9 @@
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
-  "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> 
-            @ ⊤ ∖ ∅, ∅ << l ↦ x, COMM Φ #() >>
+  "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
+            @ ⊤ ∖ ∅, ∅ 
+            << l ↦ x, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -277,8 +289,9 @@
   x : val
   Φ : language.val heap_lang → iProp Σ
   ============================
-  "AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> 
-            @ ⊤ ∖ ∅, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >>
+  "AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
+            @ ⊤ ∖ ∅, ∅ 
+            << ∃ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -300,8 +313,9 @@
   x : val
   Φ : language.val heap_lang → iProp Σ
   ============================
-  "AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> 
-            @ ⊤ ∖ ∅, ∅ << l ↦ #(), COMM Φ #() >>
+  "AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
+            @ ⊤ ∖ ∅, ∅ 
+            << l ↦ #(), COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -324,7 +338,8 @@
   Φ : language.val heap_lang → iProp Σ
   ============================
   "AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>
-            @ ⊤ ∖ ∅, ∅ << l ↦ yyyy, COMM Φ #() >>
+            @ ⊤ ∖ ∅, ∅ 
+            << l ↦ yyyy, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -347,9 +362,10 @@
   xx, yyyy : val
   Φ : 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 Φ #() >>
+  "AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>
+            @ ⊤ ∖ ∅, ∅ 
+            << l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗
+               l ↦ xx, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -362,12 +378,12 @@
   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.ref b/tests/heap_lang.ref
index 2cf9ac222f035deeae5075af0599ac7b9c7f0473..ecab7bdd6a9a190f402ca6ecec3c33c3ace5c769 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -32,7 +32,8 @@
   "Hl" : l ↦ #1
   --------------------------------------∗
   WP let: "x" := #l in let: "y" := ref #1 in "x" <- ! "x" + #1;; ! "x"
-  @ E [{ v, ⌜v = #2⌝ }]
+  @ E
+  [{ v, ⌜v = #2⌝ }]
   
 1 goal
   
diff --git a/tests/heap_lang_printing.ref b/tests/heap_lang_printing.ref
index df425cad2f0aac41f7656d1a9cc95a1e99df61f5..596127e1b1c41dbabc2e90fe9cdd7e3b64889f88 100644
--- a/tests/heap_lang_printing.ref
+++ b/tests/heap_lang_printing.ref
@@ -23,27 +23,111 @@
   Σ : gFunctors
   heapGS0 : heapGS Σ
   fun1, fun2, fun3 : expr
-  Φ : language.val heap_lang → iPropI Σ
+  ============================
+  --------------------------------------∗
+  WP fun1 #()
+  {{ v,
+     WP let: "val1" := v in
+        let: "val2" := fun2 "val1" in
+        let: "val3" := fun3 "val2" in
+        if: "val1" = "val2" then "val" else "val3"
+     {{ _, True }} }}
+  
+1 goal
+  
+  Σ : gFunctors
+  heapGS0 : heapGS Σ
+  fun1, fun2, fun3 : expr
+  long_post : iPropI Σ
   ============================
   --------------------------------------∗
   WP let: "val1" := fun1 #() in
      let: "val2" := fun2 "val1" in
-     let: "v" := fun3 "v" in if: "v" = "v" then "v" else "v" 
-  {{ v, Φ v }}
+     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 }}
   
 1 goal
   
   Σ : gFunctors
   heapGS0 : heapGS Σ
   fun1, fun2, fun3 : expr
-  Φ : language.val heap_lang → iPropI Σ
-  E : coPset
+  long_post : iPropI Σ
   ============================
   --------------------------------------∗
-  WP let: "val1" := fun1 #() in
+  WP fun1 #()
+  {{ v,
+     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 }} }}
+  
+1 goal
+  
+  Σ : gFunctors
+  heapGS0 : heapGS Σ
+  l1 : loc
+  fun2, fun3 : expr
+  long_post : iPropI Σ
+  N : namespace
+  E_long : coPset
+  H : ↑N ⊆ E_long
+  ============================
+  "Hinv" : inv N True
+  --------------------------------------∗
+  WP let: "val1" := ! #l1 in
      let: "val2" := fun2 "val1" in
-     let: "v" := fun3 "v" in if: "v" = "v" then "v" else "v" 
-  @ E {{ v, Φ v }}
+     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
+  
+  Σ : gFunctors
+  heapGS0 : heapGS Σ
+  l1 : loc
+  fun2, fun3 : expr
+  long_post : iPropI Σ
+  N : namespace
+  E_long : coPset
+  H : ↑N ⊆ E_long
+  ============================
+  "Hinv" : inv N True
+  --------------------------------------∗
+  WP ! #l1
+  @ E_long
+  {{ v,
+     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
+  
+  Σ : gFunctors
+  heapGS0 : heapGS Σ
+  l1 : loc
+  fun2, fun3 : expr
+  long_post : iPropI Σ
+  N : namespace
+  E_long : coPset
+  H : ↑N ⊆ E_long
+  ============================
+  --------------------------------------∗
+  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 }} }}
   
 1 goal
   
@@ -56,3 +140,31 @@
     let: "val2" := fun2 "val1" in
     let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
   {{{ (x y : val) (z : Z), RET (x, y, #z); True }}}
+1 goal
+  
+  Σ : gFunctors
+  heapGS0 : heapGS Σ
+  fun1, fun2, fun3 : expr
+  E_mask_is_long_too : coPset
+  ============================
+  {{{ True }}}
+    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 }}}
+1 goal
+  
+  Σ : gFunctors
+  heapGS0 : heapGS Σ
+  fun1, fun2, fun3 : expr
+  long_post : iPropI Σ
+  E_mask_is_long_too : coPset
+  ============================
+  {{{ True }}}
+    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 }}}
diff --git a/tests/heap_lang_printing.v b/tests/heap_lang_printing.v
index 31e92bd610f33697be896eb618178bd55f51f4c4..c580e42b7c987debe04d963a2811eef3fb3d8645 100644
--- a/tests/heap_lang_printing.v
+++ b/tests/heap_lang_printing.v
@@ -27,24 +27,32 @@ Section printing_tests.
        if: "val1" = "val2" then "val" else "val3"  {{ _, True }}.
   Proof.
     iIntros "_". Show.
+    wp_bind (fun1 #()). Show.
   Abort.
 
-  Lemma wp_print_long_expr (fun1 fun2 fun3 : expr) Φ :
+  Lemma wp_print_long_expr (fun1 fun2 fun3 : expr) long_post :
     True -∗ WP let: "val1" := fun1 #() in
        let: "val2" := fun2 "val1" in
        let: "v" := fun3 "v" in
-       if: "v" = "v" then "v" else "v"  {{ Φ }}.
+       if: "v" = "v" then "v" else "v"
+    {{ _, long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post }}.
   Proof.
     iIntros "_". Show.
+    wp_bind (fun1 #()). Show.
   Abort.
 
-  Lemma wp_print_long_expr (fun1 fun2 fun3 : expr) Φ E :
-    True -∗ WP let: "val1" := fun1 #() in
+  Lemma wp_print_long_expr (l1 : loc) (fun2 fun3 : expr) long_post N E_long :
+    ↑N ⊆ E_long →
+    inv N True -∗ WP let: "val1" := ! #l1 in
        let: "val2" := fun2 "val1" in
        let: "v" := fun3 "v" in
-       if: "v" = "v" then "v" else "v" @ E {{ Φ }}.
+       if: "v" = "v" then "v" else "v"
+    @ E_long
+    {{ _, long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post }}.
   Proof.
-    iIntros "_". Show.
+    iIntros (?) "Hinv". Show.
+    wp_bind (! #l1)%E. Show.
+    iInv "Hinv" as "_". Show.
   Abort.
 
   Lemma texan_triple_long_expr (fun1 fun2 fun3 : expr) :
@@ -56,4 +64,24 @@ Section printing_tests.
     {{{ (x y : val) (z : Z), RET (x, y, #z); True }}}.
   Proof. Show. Abort.
 
+  Lemma texan_triple_long_expr_mask (fun1 fun2 fun3 : expr) E_mask_is_long_too :
+    {{{ True }}}
+       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 }}}.
+  Proof. Show. Abort.
+
+  Lemma texan_triple_long_expr_mask_post (fun1 fun2 fun3 : expr) long_post E_mask_is_long_too :
+    {{{ True }}}
+       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 }}}.
+  Proof. Show. Abort.
+
 End printing_tests.
diff --git a/tests/list_reverse.ref b/tests/list_reverse.ref
index cd47ff4bdd1763eb219c002b3b74f50dd5d0308e..f673d83d48d901ecd528dbb5b0fe60093d725090 100644
--- a/tests/list_reverse.ref
+++ b/tests/list_reverse.ref
@@ -29,5 +29,6 @@
        let: "tmp1" := Fst ! "l" in
        let: "tmp2" := Snd ! "l" in
        "l" <- ("tmp1", acc);; rev "tmp2" (InjLV #())
-     end [{ v, Φ v }]
+     end
+  [{ v, Φ v }]
   
diff --git a/tests/one_shot.ref b/tests/one_shot.ref
index 94a3ddc05772f1ed1db1cd01a26a0c45d7698dfc..bd5c8d7fe9c61cad4f89779de7e89316e896e891 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,10 +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 4be43be0dc1b52d1098fb69503a0791d46ee5469..48311b6a3471067817bcdca838b45531d61dc411 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,10 +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 ac5e9cf57c10ad06210c29ba7a38745369ee3c2a..ce883c7eb98eb7a49acf25b11f63a43eaedf61d8 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 b0d84bf2c75c5d4b125f57031d216c7197c7210e..a1843eb617d3cd2e87e5d406ff301e1322776f80 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 d049912e274832e8df70839ebb36fa384e240c9a..4d3be4eaeba98ed4639adef6c6b491c9a0f6ff46 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