diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index bc516583777a44832c6981234a3ae9faab51e3b5..f225a57a6e5d40a648942c46a16cfc5de706da24 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -19,6 +19,46 @@
   --------------------------------------â–¡
   Q ∨ P
   
+1 subgoal
+  
+  PROP : sbi
+  P : PROP
+  ============================
+  "HP" : (P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P)
+         ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P
+  --------------------------------------∗
+  P
+  
+1 subgoal
+  
+  PROP : sbi
+  P : PROP
+  ============================
+  _ : (P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P)
+      ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P
+  --------------------------------------∗
+  P
+  
+1 subgoal
+  
+  PROP : sbi
+  P : PROP
+  ============================
+  "HP" : TESTNOTATION {{ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P | 
+         P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P }}
+  --------------------------------------∗
+  P
+  
+1 subgoal
+  
+  PROP : sbi
+  P : PROP
+  ============================
+  _ : TESTNOTATION {{ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P | 
+      P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P }}
+  --------------------------------------∗
+  P
+  
 1 subgoal
   
   PROP : sbi
diff --git a/tests/proofmode.v b/tests/proofmode.v
index be7245aedd0cf24f87a8d14012044921c9b51870..84d2c922917167ac0cc1e1117c96ee2297b7160a 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -37,6 +37,39 @@ Lemma demo_3 P1 P2 P3 :
   P1 ∗ P2 ∗ P3 -∗ P1 ∗ ▷ (P2 ∗ ∃ x, (P3 ∧ ⌜x = 0⌝) ∨ P3).
 Proof. iIntros "($ & $ & $)". iNext. by iExists 0. Qed.
 
+(* Test line breaking of long assumptions. *)
+Section linebreaks.
+Lemma print_long_line P :
+  (P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P) ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P
+  -∗ P.
+Proof.
+  iIntros "HP". Show.
+Abort.
+Lemma print_long_line_anon P :
+  (P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P) ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P
+  -∗ P.
+Proof.
+  iIntros "?". Show.
+Abort.
+
+(* This is specifically crafted such that not having the `hv` in
+   the proofmode notation breaks the output. *)
+Local Notation "'TESTNOTATION' '{{' P '|' Q '}' '}'" := (P ∧ Q)%I
+  (format "'TESTNOTATION'  '{{'  P  '|'  Q  '}' '}'") : bi_scope.
+Lemma print_long_line P :
+  TESTNOTATION {{ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P | P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P }}
+  -∗ P.
+Proof.
+  iIntros "HP". Show.
+Abort.
+Lemma print_long_line_anon P :
+  TESTNOTATION {{ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P | P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P }}
+  -∗ P.
+Proof.
+  iIntros "?". Show.
+Abort.
+End linebreaks.
+
 Definition foo (P : PROP) := (P -∗ P)%I.
 Definition bar : PROP := (∀ P, foo P)%I.
 
diff --git a/tests/proofmode_iris.ref b/tests/proofmode_iris.ref
index 30f4ac3d4defa422577b34d0d6b6a8d41b9304e7..735cba70fecd266f25fee04d0bd183d4f37afa25 100644
--- a/tests/proofmode_iris.ref
+++ b/tests/proofmode_iris.ref
@@ -103,8 +103,7 @@
   --------------------------------------â–¡
   "Hown1" : na_own t E1
   "Hown2" : na_own t (E2 ∖ ↑N)
-  "Hclose" : ▷ <pers> P ∗ na_own t (E2 ∖ ↑N) ={⊤}=∗ 
-  id (na_own t E2)
+  "Hclose" : ▷ <pers> P ∗ na_own t (E2 ∖ ↑N) ={⊤}=∗ id (na_own t E2)
   --------------------------------------∗
   |={⊤}=> na_own t E1 ∗ na_own t E2 ∗ ▷ P
   
diff --git a/theories/proofmode/notation.v b/theories/proofmode/notation.v
index 37bce07be123dbec55aa9b1253e42443d8e20731..7f273eb8eaf81cc6e38dc172bea0a4615667e9ed 100644
--- a/theories/proofmode/notation.v
+++ b/theories/proofmode/notation.v
@@ -10,10 +10,10 @@ Arguments Esnoc {_} _%proof_scope _%string _%I.
 Notation "" := Enil (only printing) : proof_scope.
 Notation "Γ H : P" := (Esnoc Γ (INamed H) P)
   (at level 1, P at level 200,
-   left associativity, format "Γ H  :  P '//'", only printing) : proof_scope.
+   left associativity, format "Γ H  :  '[hv' P ']' '//'", only printing) : proof_scope.
 Notation "Γ '_' : P" := (Esnoc Γ (IAnon _) P)
   (at level 1, P at level 200,
-   left associativity, format "Γ '_'  :  P '//'", only printing) : proof_scope.
+   left associativity, format "Γ '_'  :  '[hv' P ']' '//'", only printing) : proof_scope.
 
 Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ∗ Q" :=
   (envs_entails (Envs Γ Δ _) Q%I)