diff --git a/iris/proofmode/notation.v b/iris/proofmode/notation.v
index 0dfb1c1e5ff3decaf2f4e1ccc3d628cf0a191122..da7af97dff01813d335e5a22778389a7c9a6b771 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 532b1a1366e993cbcc9fdb19a513d70b0439f853..c69ac5b38b5ff81298c5fd8880571b216aedbf55 100644
--- a/tests/atomic.ref
+++ b/tests/atomic.ref
@@ -12,7 +12,6 @@
   AACC << ∀ (v0 : val) (q : dfrac), l ↦{q} v0, ABORT l ↦ v >>
        @ ⊤ ∖ ∅, ∅ 
        << l ↦{q} v0, COMM Q -∗ Q >>
-  
 "non_laterable"
      : string
 1 goal
@@ -28,7 +27,6 @@
   AACC << ∀ (v : val) (q : dfrac), l ↦{q} v, ABORT ▷ P >>
        @ ⊤ ∖ ∅, ∅ 
        << l ↦{q} v, COMM True >>
-  
 1 goal
   
   Σ : gFunctors
@@ -42,7 +40,6 @@
   AACC << ∀ (v : val) (q : dfrac), l ↦{q} v, ABORT ▷ P >>
        @ ⊤ ∖ ∅, ∅ 
        << l ↦{q} v, COMM True >>
-  
 "printing"
      : string
 1 goal
@@ -62,7 +59,6 @@
   "AU" : AU << ∀ x : val, P x >> @ ⊤ ∖ ∅, ∅ << ∃ y : val, P y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
-  
 1 goal
   
   Σ : gFunctors
@@ -78,7 +74,6 @@
            << ∃ y : val, P y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
-  
 1 goal
   
   Σ : gFunctors
@@ -96,7 +91,6 @@
   "AU" : AU << ∀ x : val, l ↦ x >> @ ⊤ ∖ ∅, ∅ << l ↦ x, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
-  
 1 goal
   
   Σ : gFunctors
@@ -112,7 +106,6 @@
            << l ↦ x, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
-  
 1 goal
   
   Σ : gFunctors
@@ -130,7 +123,6 @@
   "AU" : AU << l ↦ #() >> @ ⊤ ∖ ∅, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
-  
 1 goal
   
   Σ : gFunctors
@@ -146,7 +138,6 @@
            << ∃ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
-  
 1 goal
   
   Σ : gFunctors
@@ -164,7 +155,6 @@
   "AU" : AU << l ↦ #() >> @ ⊤ ∖ ∅, ∅ << l ↦ #(), COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
-  
 1 goal
   
   Σ : gFunctors
@@ -178,7 +168,6 @@
            << l ↦ #(), COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
-  
 "Now come the long pre/post tests"
      : string
 1 goal
@@ -202,7 +191,6 @@
             << ∃ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
-  
 1 goal
   
   Σ : gFunctors
@@ -224,7 +212,6 @@
             << ∃ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
-  
 1 goal
   
   Σ : gFunctors
@@ -248,7 +235,6 @@
             l ↦ xx, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
-  
 1 goal
   
   Σ : gFunctors
@@ -270,7 +256,6 @@
             << l ↦ x, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
-  
 1 goal
   
   Σ : gFunctors
@@ -294,7 +279,6 @@
             << ∃ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
-  
 1 goal
   
   Σ : gFunctors
@@ -318,7 +302,6 @@
             << l ↦ #(), COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
-  
 1 goal
   
   Σ : gFunctors
@@ -342,7 +325,6 @@
             << l ↦ yyyy, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
-  
 1 goal
   
   Σ : gFunctors
@@ -368,7 +350,6 @@
                l ↦ xx, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
-  
 "Prettification"
      : string
 1 goal
@@ -386,4 +367,3 @@
            ∧ (∀ x0 : val, P x0 ={∅,⊤}=∗ Φ #())
   --------------------------------------∗
   WP ! #0 @ ∅ {{ v, |={∅,⊤}=> Φ v }}
-  
diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index ecab7bdd6a9a190f402ca6ecec3c33c3ace5c769..67af46d8f2fc6584105128398bff68f383069fe5 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -8,7 +8,6 @@
   ============================
   --------------------------------------∗
   WP let: "x" := ref #1 in "x" <- ! "x" + #1;; ! "x" @ E {{ v, ⌜v = #2⌝ }}
-  
 1 goal
   
   Σ : gFunctors
@@ -19,7 +18,6 @@
   _ : l ↦ #1
   --------------------------------------∗
   WP #l <- #1 + #1;; ! #l @ E {{ v, ⌜v = #2⌝ }}
-  
 "heap_e2_spec"
      : string
 1 goal
@@ -34,7 +32,6 @@
   WP let: "x" := #l in let: "y" := ref #1 in "x" <- ! "x" + #1;; ! "x"
   @ E
   [{ v, ⌜v = #2⌝ }]
-  
 1 goal
   
   Σ : gFunctors
@@ -46,7 +43,6 @@
   _ : l' ↦ #1
   --------------------------------------∗
   WP #l <- #1 + #1;; ! #l @ E [{ v, ⌜v = #2⌝ }]
-  
 "heap_e7_spec"
      : string
 1 goal
@@ -58,7 +54,6 @@
   _ : ▷ l ↦ #0
   --------------------------------------∗
   WP CmpXchg #l #0 #1 {{ _, l ↦ #1 }}
-  
 1 goal
   
   Σ : gFunctors
@@ -68,7 +63,6 @@
   _ : l ↦ #1
   --------------------------------------∗
   |={⊤}=> l ↦ #1
-  
 "wp_load_fail"
      : string
 The command has indeed failed with message:
@@ -105,7 +99,6 @@ Tactic failure: wp_bind: cannot find (! ?e)%E in (Val #()).
   "Hl2" : l ↦{#1 / 2} #0
   --------------------------------------∗
   |={⊤}=> True
-  
 1 goal
   
   Σ : gFunctors
@@ -114,7 +107,6 @@ Tactic failure: wp_bind: cannot find (! ?e)%E in (Val #()).
   ============================
   --------------------------------------∗
   |={⊤}=> True
-  
 "wp_nonclosed_value"
      : string
 The command has indeed failed with message:
@@ -127,7 +119,6 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   ============================
   --------------------------------------∗
   WP "x" {{ _, True }}
-  
 1 goal
   
   Σ : gFunctors
@@ -141,7 +132,6 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   _ : l ↦∗ replicate (Z.to_nat n) #0
   --------------------------------------∗
   |={⊤}=> Φ #l
-  
 "test_array_fraction_destruct"
      : string
 1 goal
@@ -155,7 +145,6 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   "Hl2" : l ↦∗{#1 / 2} vs
   --------------------------------------∗
   l ↦∗{#1 / 2} vs ∗ l ↦∗{#1 / 2} vs
-  
 "test_wp_finish_fupd"
      : string
 1 goal
@@ -166,7 +155,6 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   ============================
   --------------------------------------∗
   |={⊤}=> True
-  
 "test_twp_finish_fupd"
      : string
 1 goal
@@ -177,7 +165,6 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   ============================
   --------------------------------------∗
   |={⊤}=> True
-  
 1 goal
   
   Σ : gFunctors
@@ -191,7 +178,6 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   "HΦ" : ▷ (True -∗ Φ v)
   --------------------------------------∗
   WP ! #l {{ v, Φ v }}
-  
 1 goal
   
   Σ : gFunctors
@@ -205,7 +191,6 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   "HΦ" : True -∗ Φ v
   --------------------------------------∗
   WP ! #l [{ v, Φ v }]
-  
 1 goal
   
   Σ : gFunctors
@@ -228,9 +213,8 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
 
 goal 2 is:
  "H" : P
---------------------------------------∗
-WP #() #() @ E2 {{ _, |={E2,E1}=> True }}
-
+ --------------------------------------∗
+ WP #() #() @ E2 {{ _, |={E2,E1}=> True }}
 "wp_iInv_atomic"
      : string
 2 goals
@@ -246,10 +230,9 @@ WP #() #() @ E2 {{ _, |={E2,E1}=> True }}
 
 goal 2 is:
  "H" : â–· P
-"Hclose" : ▷ P ={E ∖ ↑N,E}=∗ emp
---------------------------------------∗
-WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N,E}=> True }}
-
+ "Hclose" : ▷ P ={E ∖ ↑N,E}=∗ emp
+ --------------------------------------∗
+ WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N,E}=> True }}
 "wp_iInv_atomic_acc"
      : string
 2 goals
@@ -265,9 +248,8 @@ WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N,E}=> True }}
 
 goal 2 is:
  "H" : â–· P
---------------------------------------∗
-WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N}=> ▷ P ∗ True }}
-
+ --------------------------------------∗
+ WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N}=> ▷ P ∗ True }}
 "not_cmpxchg"
      : string
 The command has indeed failed with message:
diff --git a/tests/heap_lang_printing.ref b/tests/heap_lang_printing.ref
index 596127e1b1c41dbabc2e90fe9cdd7e3b64889f88..a589b0dcddb4f3c8d3fb1c9be35d3fcd454a8b2b 100644
--- a/tests/heap_lang_printing.ref
+++ b/tests/heap_lang_printing.ref
@@ -5,7 +5,6 @@
   ============================
   --------------------------------------∗
   WP let: "f" := λ: "x", "x" in ref ("f" #10) {{ _, True }}
-  
 1 goal
   
   Σ : gFunctors
@@ -17,7 +16,6 @@
      let: "val2" := fun2 "val1" in
      let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
   {{ _, True }}
-  
 1 goal
   
   Σ : gFunctors
@@ -32,7 +30,6 @@
         let: "val3" := fun3 "val2" in
         if: "val1" = "val2" then "val" else "val3"
      {{ _, True }} }}
-  
 1 goal
   
   Σ : gFunctors
@@ -46,7 +43,6 @@
      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
@@ -62,7 +58,6 @@
         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
@@ -82,7 +77,6 @@
   @ E_long
   {{ _, long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗
      long_post ∗ long_post }}
-  
 1 goal
   
   Σ : gFunctors
@@ -105,7 +99,6 @@
      @ E_long
      {{ _, long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗
         long_post ∗ long_post }} }}
-  
 1 goal
   
   Σ : gFunctors
@@ -128,7 +121,6 @@
        @ E_long
        {{ _, long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗
           long_post ∗ long_post }} }}
-  
 1 goal
   
   Σ : gFunctors
diff --git a/tests/heap_lang_printing2.ref b/tests/heap_lang_printing2.ref
index 1c677e63f410219d4b8a5dc654cfb13f0e4dfd42..d5c8ffbf748a9030e4937561f0e61f43806c1b79 100644
--- a/tests/heap_lang_printing2.ref
+++ b/tests/heap_lang_printing2.ref
@@ -16,7 +16,6 @@
      let: "val2" := fun2 "val1" in
      let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
   {{ _, True }}
-  
 1 goal
   
   Σ : gFunctors
diff --git a/tests/ipm_paper.ref b/tests/ipm_paper.ref
index ffb9ec7401e0669317d36ddfd8ae57d7c7505a14..7ca6491cc009e4d3eff6faf151881b66edf08859 100644
--- a/tests/ipm_paper.ref
+++ b/tests/ipm_paper.ref
@@ -13,7 +13,6 @@
   "HR" : R
   --------------------------------------∗
   Ψ x ∗ P
-  
 1 goal
   
   M : ucmra
@@ -25,7 +24,6 @@
   "HΨ" : Ψ x
   --------------------------------------∗
   Ψ x
-  
 1 goal
   
   M : ucmra
@@ -38,7 +36,6 @@
   "HR" : R
   --------------------------------------∗
   P
-  
 "sep_exist_short"
      : string
 1 goal
@@ -53,7 +50,6 @@
   "HR" : R
   --------------------------------------∗
   ∃ a : A, Ψ a ∗ P
-  
 "read_spec"
      : string
 1 goal
@@ -71,7 +67,6 @@
   "Hγf" : own γ (Frag n)
   --------------------------------------∗
   WP ! #l {{ v, ∃ m : nat, ⌜v = #m ∧ n ≤ m⌝ ∧ C l m }}
-  
 1 goal
   
   Σ : gFunctors
@@ -90,4 +85,3 @@
   "Hγ" : own γ (Auth c)
   --------------------------------------∗
   |={⊤ ∖ ↑N}=> ▷ I γ l ∗ (∃ m : nat, ⌜#c = #m ∧ n ≤ m⌝ ∧ C l m)
-  
diff --git a/tests/list_reverse.ref b/tests/list_reverse.ref
index f673d83d48d901ecd528dbb5b0fe60093d725090..cbb1beabd6795ace7ff86080fe750c79001ad7dc 100644
--- a/tests/list_reverse.ref
+++ b/tests/list_reverse.ref
@@ -11,7 +11,6 @@
   "HΦ" : ∀ w : val, is_list w (reverse xs ++ ys) -∗ Φ w
   --------------------------------------∗
   WP rev hd acc [{ v, Φ v }]
-  
 1 goal
   
   Σ : gFunctors
@@ -31,4 +30,3 @@
        "l" <- ("tmp1", acc);; rev "tmp2" (InjLV #())
      end
   [{ v, Φ v }]
-  
diff --git a/tests/mosel_paper.ref b/tests/mosel_paper.ref
index 0369dfe162820419ade5167b99d35330ae1bb269..f7bc683c9a64b21ea7e2f30825dace429eb9470a 100644
--- a/tests/mosel_paper.ref
+++ b/tests/mosel_paper.ref
@@ -9,7 +9,6 @@
   "H" : ∃ a : A, Φ a ∨ Ψ a
   --------------------------------------∗
   ∃ a : A, P ∗ Φ a ∨ P ∗ Ψ a
-  
 1 goal
   
   PROP : bi
@@ -22,7 +21,6 @@
   "H1" : Φ x
   --------------------------------------∗
   ∃ a : A, P ∗ Φ a ∨ P ∗ Ψ a
-  
 1 goal
   
   PROP : bi
@@ -35,7 +33,6 @@
   "H2" : Ψ x
   --------------------------------------∗
   ∃ a : A, P ∗ Φ a ∨ P ∗ Ψ a
-  
 1 goal
   
   PROP : bi
@@ -47,7 +44,6 @@
   "H" : ∃ a : A, Φ a ∨ Ψ a
   --------------------------------------∗
   ∃ a : A, P ∗ Φ a ∨ P ∗ Ψ a
-  
 1 goal
   
   PROP : bi
@@ -58,7 +54,6 @@
   "H" : ∃ a : A, Φ a ∨ Ψ a
   --------------------------------------∗
   ∃ x : A, Φ x ∨ Ψ x
-  
 1 goal
   
   PROP : bi
@@ -71,7 +66,6 @@
   "H1" : Φ x
   --------------------------------------∗
   Φ x
-  
 1 goal
   
   PROP : bi
@@ -84,7 +78,6 @@
   "H2" : Ψ x
   --------------------------------------∗
   P ∗ Ψ x
-  
 1 goal
   
   PROP : bi
@@ -97,7 +90,6 @@
   "H" : ∃ a : A, Φ a ∨ Ψ a
   --------------------------------------∗
   ∃ a : A, Φ a ∨ P ∗ P ∗ Ψ a
-  
 1 goal
   
   PROP : bi
@@ -111,7 +103,6 @@
   "H2" : Ψ x
   --------------------------------------∗
   P ∗ P ∗ Ψ x
-  
 1 goal
   
   PROP : bi
@@ -122,7 +113,6 @@
   "HQ" : Q
   --------------------------------------â–¡
   □ (P ∗ Q)
-  
 1 goal
   
   I : biIndex
@@ -133,7 +123,6 @@
   "H2" : Φ -∗ Ψ
   --------------------------------------∗
   Ψ
-  
 1 goal
   
   I : biIndex
@@ -142,7 +131,6 @@
   ============================
   --------------------------------------∗
   ∀ i : I, Φ i ∗ (Φ -∗ Ψ) i -∗ Ψ i
-  
 1 goal
   
   I : biIndex
@@ -156,7 +144,6 @@
   "H3" : <affine> Φ
   --------------------------------------∗
   ⎡ P ∗ Q ⎤
-  
 1 goal
   
   I : biIndex
@@ -170,4 +157,3 @@
   "H3" : <affine> Φ
   --------------------------------------∗
   ⎡ Q ⎤
-  
diff --git a/tests/one_shot.ref b/tests/one_shot.ref
index bd5c8d7fe9c61cad4f89779de7e89316e896e891..7ae888dae419bdaade976aef3754b05fee020242 100644
--- a/tests/one_shot.ref
+++ b/tests/one_shot.ref
@@ -16,7 +16,6 @@
   one_shot_inv γ l ∗
   (⌜InjLV #() = InjLV #()⌝
    ∨ (∃ n : Z, ⌜InjLV #() = InjRV #n⌝ ∗ own γ (Shot n)))
-  
 1 goal
   
   Σ : gFunctors
@@ -40,5 +39,4 @@
        | 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 48311b6a3471067817bcdca838b45531d61dc411..6f721994e5b705a36820d319966995ce1d757e66 100644
--- a/tests/one_shot_once.ref
+++ b/tests/one_shot_once.ref
@@ -16,7 +16,6 @@
   one_shot_inv γ l ∗
   (⌜InjLV #() = InjLV #()⌝
    ∨ (∃ n : Z, ⌜InjLV #() = InjRV #n⌝ ∗ own γ (Shot n)))
-  
 1 goal
   
   Σ : gFunctors
@@ -41,4 +40,3 @@
        | InjR <> => assert: InjRV #m = "y'"
        end
     {{ _, True }}
-  
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index ce883c7eb98eb7a49acf25b11f63a43eaedf61d8..78d3fc66c2ace0804bcff092b6293d81fdc9cd0e 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -10,7 +10,6 @@
   "H" : □ (P ∨ Q)
   --------------------------------------∗
   Q ∨ P
-  
 1 goal
   
   PROP : bi
@@ -20,7 +19,6 @@
   _ : P
   --------------------------------------â–¡
   Q ∨ P
-  
 "test_iStopProof"
      : string
 1 goal
@@ -33,7 +31,6 @@
   "H2" : Q
   --------------------------------------∗
   Q
-  
 1 goal
   
   PROP : bi
@@ -53,7 +50,6 @@
   _ : Q
   --------------------------------------â–¡
   <affine> (P ∗ Q)
-  
 "test_iDestruct_spatial"
      : string
 1 goal
@@ -64,7 +60,6 @@
   "HQ" : <affine> Q
   --------------------------------------∗
   Q
-  
 "test_iDestruct_spatial_affine"
      : string
 1 goal
@@ -76,7 +71,6 @@
   "HQ" : Q
   --------------------------------------∗
   Q
-  
 "test_iDestruct_exists_not_exists"
      : string
 The command has indeed failed with message:
@@ -93,7 +87,6 @@ Tactic failure: iExistDestruct: cannot destruct P.
   "H" : Φ y ∧ P
   --------------------------------------â–¡
   P
-  
 "test_iDestruct_exists_anonymous"
      : string
 1 goal
@@ -106,7 +99,6 @@ Tactic failure: iExistDestruct: cannot destruct P.
   "HΦ" : ∃ x : nat, Φ x
   --------------------------------------∗
   ∃ x : nat, Φ x
-  
 "test_iIntros_forall_pure"
      : string
 1 goal
@@ -117,7 +109,6 @@ Tactic failure: iExistDestruct: cannot destruct P.
   ============================
   --------------------------------------∗
   Ψ x → Ψ x
-  
 "test_iIntros_pure_names"
      : string
 1 goal
@@ -130,7 +121,6 @@ Tactic failure: iExistDestruct: cannot destruct P.
   ============================
   --------------------------------------∗
   P -∗ P
-  
 The command has indeed failed with message:
 No applicable tactic.
 The command has indeed failed with message:
@@ -170,7 +160,6 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
   ============================
   --------------------------------------∗
   â–·^(S n + S m) emp
-  
 "test_specialize_nested_intuitionistic"
      : string
 1 goal
@@ -186,7 +175,6 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
   "HR" : R2
   --------------------------------------∗
   R2
-  
 "test_iSimpl_in"
      : string
 1 goal
@@ -197,7 +185,6 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
   "H" : ⌜S (S (S x)) = y⌝
   --------------------------------------∗
   ⌜S (S (S x)) = y⌝
-  
 1 goal
   
   PROP : bi
@@ -207,7 +194,6 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
   "H2" : ⌜S y = z⌝
   --------------------------------------∗
   ⌜S (S (S x)) = y⌝
-  
 1 goal
   
   PROP : bi
@@ -218,7 +204,6 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
   "H2" : ⌜(1 + y)%nat = z⌝
   --------------------------------------∗
   ⌜S (S (S x)) = y⌝
-  
 "test_iSimpl_in4"
      : string
 The command has indeed failed with message:
@@ -232,7 +217,6 @@ Tactic failure: iEval: %: unsupported selection pattern.
   ============================
   --------------------------------------∗
   â–· emp
-  
 "test_iFrame_later_2"
      : string
 1 goal
@@ -242,7 +226,6 @@ Tactic failure: iEval: %: unsupported selection pattern.
   ============================
   --------------------------------------∗
   â–· emp
-  
 The command has indeed failed with message:
 Tactic failure: iFrame: cannot frame Q.
 "test_and_sep_affine_bi"
@@ -257,7 +240,6 @@ Tactic failure: iFrame: cannot frame Q.
   _ : Q
   --------------------------------------∗
   â–¡ P
-  
 "test_big_sepL_simpl"
      : string
 1 goal
@@ -272,7 +254,6 @@ Tactic failure: iFrame: cannot frame Q.
   _ : [∗ list] y ∈ (x :: l), <affine> ⌜y = y⌝
   --------------------------------------∗
   P
-  
 1 goal
   
   PROP : bi
@@ -285,7 +266,6 @@ Tactic failure: iFrame: cannot frame Q.
   _ : <affine> ⌜x = x⌝ ∗ ([∗ list] y ∈ l, <affine> ⌜y = y⌝)
   --------------------------------------∗
   P
-  
 "test_big_sepL2_simpl"
      : string
 1 goal
@@ -300,7 +280,6 @@ Tactic failure: iFrame: cannot frame Q.
   _ : [∗ list] y1;y2 ∈ (x1 :: l1);((x2 :: l2) ++ l2), <affine> ⌜y1 = y2⌝
   --------------------------------------∗
   P ∨ ([∗ list] _;_ ∈ (x1 :: l1);(x2 :: l2), True)
-  
 1 goal
   
   PROP : bi
@@ -314,7 +293,6 @@ Tactic failure: iFrame: cannot frame Q.
       ([∗ list] y1;y2 ∈ l1;(l2 ++ l2), <affine> ⌜y1 = y2⌝)
   --------------------------------------∗
   P ∨ True ∗ ([∗ list] _;_ ∈ l1;l2, True)
-  
 "test_big_sepL2_iDestruct"
      : string
 1 goal
@@ -328,7 +306,6 @@ Tactic failure: iFrame: cannot frame Q.
   _ : [∗ list] y1;y2 ∈ l1;l2, Φ y1 y2
   --------------------------------------∗
   <absorb> Φ x1 x2
-  
 "test_reducing_after_iDestruct"
      : string
 1 goal
@@ -338,7 +315,6 @@ Tactic failure: iFrame: cannot frame Q.
   "H" : â–¡ True
   --------------------------------------∗
   True
-  
 "test_reducing_after_iApply"
      : string
 1 goal
@@ -348,7 +324,6 @@ Tactic failure: iFrame: cannot frame Q.
   "H" : emp
   --------------------------------------â–¡
   â–¡ emp
-  
 "test_reducing_after_iApply_late_evar"
      : string
 1 goal
@@ -358,7 +333,6 @@ Tactic failure: iFrame: cannot frame Q.
   "H" : emp
   --------------------------------------â–¡
   â–¡ emp
-  
 "test_wandM"
      : string
 1 goal
@@ -372,7 +346,6 @@ Tactic failure: iFrame: cannot frame Q.
   "HP" : default emp mP
   --------------------------------------∗
   R
-  
 1 goal
   
   PROP : bi
@@ -382,7 +355,6 @@ Tactic failure: iFrame: cannot frame Q.
   "HP" : default emp mP
   --------------------------------------∗
   default emp mP
-  
 1 goal
   
   PROP : bi
@@ -394,7 +366,6 @@ Tactic failure: iFrame: cannot frame Q.
   "HQ" : Q
   --------------------------------------∗
   ▷ P ∗ Q
-  
 "elim_mod_accessor"
      : string
 1 goal
@@ -409,7 +380,6 @@ Tactic failure: iFrame: cannot frame Q.
   "Hacc" : ∃ x : X, α x ∗ (β x ={E2,E1}=∗ default emp (γ x))
   --------------------------------------∗
   |={E2,E1}=> True
-  
 "print_long_line_1"
      : string
 1 goal
@@ -422,7 +392,6 @@ Tactic failure: iFrame: cannot frame Q.
          P_P_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
-  
 1 goal
   
   PROP : bi
@@ -433,7 +402,6 @@ Tactic failure: iFrame: cannot frame Q.
       P_P_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
-  
 "print_long_line_2"
      : string
 1 goal
@@ -446,7 +414,6 @@ Tactic failure: iFrame: cannot frame Q.
          P_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
-  
 1 goal
   
   PROP : bi
@@ -457,7 +424,6 @@ Tactic failure: iFrame: cannot frame Q.
       P_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
-  
 "long_impl"
      : string
 1 goal
@@ -469,7 +435,6 @@ Tactic failure: iFrame: cannot frame Q.
   --------------------------------------∗
   PPPPPPPPPPPPPPPPP → QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗
   QQQQQQQQQQQQQQQQQQ
-  
 "long_impl_nested"
      : string
 1 goal
@@ -482,7 +447,6 @@ Tactic failure: iFrame: cannot frame Q.
   PPPPPPPPPPPPPPPPP
   → QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
     → QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
-  
 "long_wand"
      : string
 1 goal
@@ -494,7 +458,6 @@ Tactic failure: iFrame: cannot frame Q.
   --------------------------------------∗
   PPPPPPPPPPPPPPPPP -∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗
   QQQQQQQQQQQQQQQQQQ
-  
 "long_wand_nested"
      : string
 1 goal
@@ -507,7 +470,6 @@ Tactic failure: iFrame: cannot frame Q.
   PPPPPPPPPPPPPPPPP -∗
   QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ -∗
   QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
-  
 "long_fupd"
      : string
 1 goal
@@ -520,7 +482,6 @@ Tactic failure: iFrame: cannot frame Q.
   --------------------------------------∗
   PPPPPPPPPPPPPPPPP ={E}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗
   QQQQQQQQQQQQQQQQQQ
-  
 "long_fupd_nested"
      : string
 1 goal
@@ -534,7 +495,6 @@ Tactic failure: iFrame: cannot frame Q.
   PPPPPPPPPPPPPPPPP ={E1,E2}=∗
   QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ={E1,E2}=∗
   QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
-  
 "iStopProof_not_proofmode"
      : string
 The command has indeed failed with message:
@@ -764,7 +724,6 @@ but has unexpected type nat.
   "HP" : P
   --------------------------------------∗
   P ∗ ⌜φ2⌝
-  
 "test_not_fresh"
      : string
 The command has indeed failed with message:
diff --git a/tests/proofmode_ascii.ref b/tests/proofmode_ascii.ref
index a1843eb617d3cd2e87e5d406ff301e1322776f80..5db0de8ae8ce60a59390d6b2544f32df7b9f11ac 100644
--- a/tests/proofmode_ascii.ref
+++ b/tests/proofmode_ascii.ref
@@ -11,7 +11,6 @@
   "H2" : â–· <pers> P
   --------------------------------------â–¡
   |={⊤ ∖ ↑N}=> ▷ <pers> P ∗ (|={⊤}=> ▷ P)
-  
 1 goal
   
   Σ : gFunctors
@@ -27,7 +26,6 @@
   "Hclose" : ▷ <pers> P ={⊤ ∖ ↑N,⊤}=∗ emp
   --------------------------------------∗
   |={⊤ ∖ ↑N,⊤}=> ▷ P
-  
 1 goal
   
   Σ : gFunctors
@@ -45,7 +43,6 @@
   "Hown" : cinv_own γ p
   --------------------------------------∗
   |={⊤ ∖ ↑N}=> ▷ <pers> P ∗ (|={⊤}=> cinv_own γ p ∗ ▷ P)
-  
 1 goal
   
   Σ : gFunctors
@@ -64,7 +61,6 @@
   "Hclose" : ▷ <pers> P ={⊤ ∖ ↑N,⊤}=∗ emp
   --------------------------------------∗
   |={⊤ ∖ ↑N,⊤}=> cinv_own γ p ∗ ▷ P
-  
 1 goal
   
   Σ : gFunctors
@@ -85,7 +81,6 @@
   --------------------------------------∗
   |={⊤}=> (▷ <pers> P ∗ na_own t (E2 ∖ ↑N)) ∗
     (na_own t E2 ={⊤}=∗ na_own t E1 ∗ na_own t E2 ∗ ▷ P)
-  
 1 goal
   
   Σ : gFunctors
@@ -106,7 +101,6 @@
   "Hclose" : ▷ <pers> P ∗ na_own t (E2 ∖ ↑N) ={⊤}=∗ na_own t E2
   --------------------------------------∗
   |={⊤}=> na_own t E1 ∗ na_own t E2 ∗ ▷ P
-  
 "test_iInv_12"
      : string
 The command has indeed failed with message:
@@ -130,7 +124,6 @@ Tactic failure: iInv: invariant "H2" not found.
   "HP" : ⎡ ▷ 𝓟 ⎤
   --------------------------------------∗
   |={E ∖ ↑N}=> ⎡ ▷ 𝓟 ⎤ ∗ (|={E}=> emp)
-  
 "test_iInv_with_close"
      : string
 1 goal
@@ -147,7 +140,6 @@ Tactic failure: iInv: invariant "H2" not found.
   "Hclose" : ⎡ ▷ 𝓟 ={E ∖ ↑N,E}=∗ emp ⎤
   --------------------------------------∗
   |={E ∖ ↑N,E}=> emp
-  
 "p1"
      : string
 1 goal
diff --git a/tests/proofmode_iris.ref b/tests/proofmode_iris.ref
index 4d3be4eaeba98ed4639adef6c6b491c9a0f6ff46..f0895eca28b9fbd23262e76467788199d8d4b480 100644
--- a/tests/proofmode_iris.ref
+++ b/tests/proofmode_iris.ref
@@ -11,7 +11,6 @@
   "H2" : â–· <pers> P
   --------------------------------------â–¡
   |={⊤ ∖ ↑N}=> ▷ <pers> P ∗ (|={⊤}=> ▷ P)
-  
 1 goal
   
   Σ : gFunctors
@@ -27,7 +26,6 @@
   "Hclose" : ▷ <pers> P ={⊤ ∖ ↑N,⊤}=∗ emp
   --------------------------------------∗
   |={⊤ ∖ ↑N,⊤}=> ▷ P
-  
 1 goal
   
   Σ : gFunctors
@@ -57,7 +55,6 @@
   "Hown" : cinv_own γ p
   --------------------------------------∗
   |={⊤ ∖ ↑N}=> ▷ <pers> P ∗ (|={⊤}=> cinv_own γ p ∗ ▷ P)
-  
 1 goal
   
   Σ : gFunctors
@@ -76,7 +73,6 @@
   "Hclose" : ▷ <pers> P ={⊤ ∖ ↑N,⊤}=∗ emp
   --------------------------------------∗
   |={⊤ ∖ ↑N,⊤}=> cinv_own γ p ∗ ▷ P
-  
 1 goal
   
   Σ : gFunctors
@@ -97,7 +93,6 @@
   --------------------------------------∗
   |={⊤}=> (▷ <pers> P ∗ na_own t (E2 ∖ ↑N)) ∗
     (na_own t E2 ={⊤}=∗ na_own t E1 ∗ na_own t E2 ∗ ▷ P)
-  
 1 goal
   
   Σ : gFunctors
@@ -132,7 +127,6 @@
   "Hclose" : ▷ <pers> P ∗ na_own t (E2 ∖ ↑N) ={⊤}=∗ na_own t E2
   --------------------------------------∗
   |={⊤}=> na_own t E1 ∗ na_own t E2 ∗ ▷ P
-  
 "test_iInv_12"
      : string
 The command has indeed failed with message:
@@ -156,7 +150,6 @@ Tactic failure: iInv: invariant "H2" not found.
   "H2" : own γ (1 / 2)%Qp
   --------------------------------------∗
   own γ 1%Qp
-  
 1 goal
   
   Σ : gFunctors
@@ -169,7 +162,6 @@ Tactic failure: iInv: invariant "H2" not found.
   "H" : own γ 1%Qp
   --------------------------------------∗
   own γ 1%Qp
-  
 "test_iInv"
      : string
 1 goal
@@ -185,7 +177,6 @@ Tactic failure: iInv: invariant "H2" not found.
   "HP" : ⎡ ▷ 𝓟 ⎤
   --------------------------------------∗
   |={E ∖ ↑N}=> ⎡ ▷ 𝓟 ⎤ ∗ (|={E}=> emp)
-  
 "test_iInv_with_close"
      : string
 1 goal
@@ -202,4 +193,3 @@ Tactic failure: iInv: invariant "H2" not found.
   "Hclose" : ⎡ ▷ 𝓟 ={E ∖ ↑N,E}=∗ emp ⎤
   --------------------------------------∗
   |={E ∖ ↑N,E}=> emp
-  
diff --git a/tests/proofmode_monpred.ref b/tests/proofmode_monpred.ref
index 4d1d96175d23bf8ca564feaab67ade0c4dde7c9a..37fde33a6b980db77a5656a3982692601d2a531b 100644
--- a/tests/proofmode_monpred.ref
+++ b/tests/proofmode_monpred.ref
@@ -8,7 +8,6 @@
   "HW" : (P -∗ Q) i
   --------------------------------------∗
   (P -∗ Q) i
-  
 1 goal
   
   I : biIndex
@@ -20,7 +19,6 @@
   "HP" : P j
   --------------------------------------∗
   Q j
-  
 1 goal
   
   I : biIndex
@@ -34,7 +32,6 @@
   "H4" : 𝓠
   --------------------------------------∗
   ∀ i, 𝓟 ∗ 𝓠 ∗ Q i
-  
 1 goal
   
   I : biIndex
@@ -45,7 +42,6 @@
   ============================
   --------------------------------------∗
   (Q -∗ emp) i
-  
 1 goal
   
   I : biIndex
@@ -56,7 +52,6 @@
   ============================
   --------------------------------------∗
   ∀ _ : (), ∃ _ : (), emp
-  
 The command has indeed failed with message:
 Tactic failure: iFrame: cannot frame (P i).
 1 goal
@@ -71,7 +66,6 @@ Tactic failure: iFrame: cannot frame (P i).
   "H2" : ⎡ ▷ <pers> 𝓟 ⎤
   --------------------------------------â–¡
   |={⊤ ∖ ↑N}=> ⎡ ▷ <pers> 𝓟 ⎤ ∗ (|={⊤}=> ⎡ ▷ 𝓟 ⎤)
-  
 1 goal
   
   I : biIndex
@@ -86,4 +80,3 @@ Tactic failure: iFrame: cannot frame (P i).
   "Hclose" : ⎡ ▷ <pers> 𝓟 ={⊤ ∖ ↑N,⊤}=∗ emp ⎤
   --------------------------------------∗
   |={⊤ ∖ ↑N,⊤}=> ⎡ ▷ 𝓟 ⎤
-  
diff --git a/tests/telescopes.ref b/tests/telescopes.ref
index 2743ec03a2202e03bd0d449c8c306818eae58398..5ffac672a96f4d0744032ad992218e7c25167e8b 100644
--- a/tests/telescopes.ref
+++ b/tests/telescopes.ref
@@ -12,7 +12,6 @@
   "Hclose" : β x' ={E2,E1}=∗ γ1 x'
   --------------------------------------∗
   |={E2}=> ∃.. x : X, α x ∗ (β x ={E2,E1}=∗ γ2 x)
-  
 1 goal
   
   PROP : bi
@@ -34,7 +33,6 @@
   "Hγ1" : γ1 x
   --------------------------------------∗
   (λ.. x0 : X, γ1 x0 ∨ γ2 x0) x
-  
 1 goal
   
   PROP : bi
@@ -47,7 +45,6 @@
   "Hγ1" : γ1 x
   --------------------------------------∗
   γ1 x ∨ γ2 x
-  
 1 goal
   
   PROP : bi
@@ -57,7 +54,6 @@
   "H" : ∃ x x0 : nat, <affine> ⌜x = x0⌝ ∗ (True ={E2,E1}=∗ <affine> ⌜x ≠ x0⌝)
   --------------------------------------∗
   |={E2,E1}=> False
-  
 "test1_test"
      : string
 1 goal
@@ -68,7 +64,6 @@
   "H" : ∃ x0 : nat, <affine> ⌜x = x0⌝
   --------------------------------------∗
   â–· False
-  
 1 goal
   
   PROP : bi
@@ -77,7 +72,6 @@
   "H" : ∃ x0 : nat, <affine> ⌜x = x0⌝
   --------------------------------------∗
   â–· False
-  
 "test2_test"
      : string
 1 goal
@@ -87,7 +81,6 @@
   "H" : ∃ x x0 : nat, <affine> ⌜x = x0⌝
   --------------------------------------∗
   False
-  
 1 goal
   
   PROP : bi
@@ -96,7 +89,6 @@
   "H" : ∃ x0 : nat, <affine> ⌜x = x0⌝
   --------------------------------------∗
   False
-  
 1 goal
   
   PROP : bi
@@ -105,7 +97,6 @@
   "H" : ▷ (∃ x0 : nat, <affine> ⌜x = x0⌝)
   --------------------------------------∗
   â–· False
-  
 "test3_test"
      : string
 1 goal
@@ -116,7 +107,6 @@
   "H" : ∃ x0 : nat, <affine> ⌜x = x0⌝
   --------------------------------------∗
   â–· False
-  
 1 goal
   
   PROP : bi
@@ -125,4 +115,3 @@
   "H" : ◇ (∃ x0 : nat, <affine> ⌜x = x0⌝)
   --------------------------------------∗
   â–· False
-