diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index f225a57a6e5d40a648942c46a16cfc5de706da24..28c05666197c1895e01afaaa8459f2948700110e 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -22,42 +22,42 @@
 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_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
+  "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
   --------------------------------------∗
-  P
+  True
   
 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_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
+  True
   
 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_P_P_P_P_P : PROP
   ============================
-  "HP" : TESTNOTATION {{ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P | 
-         P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P }}
+  "HP" : TESTNOTATION {{ P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P |
+         P_P_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 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_P_P_P_P_P : PROP
   ============================
-  _ : TESTNOTATION {{ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P | 
-      P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P }}
+  _ : TESTNOTATION {{ P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P |
+      P_P_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 subgoal
   
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 84d2c922917167ac0cc1e1117c96ee2297b7160a..63a7dd9f73279eed6998a2278eb98b9ff87b37e2 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -39,15 +39,17 @@ 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.
+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_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
+  -∗ True.
 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.
+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_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
+  -∗ True.
 Proof.
   iIntros "?". Show.
 Abort.
@@ -55,16 +57,16 @@ 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.
+  (format "'TESTNOTATION'  '{{'  P  '|'  '/' Q  '}' '}'") : bi_scope.
+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_P_P_P_P : PROP) :
+  TESTNOTATION {{ P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P | P_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.
 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.
+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_P_P_P_P : PROP) :
+  TESTNOTATION {{ P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P | P_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.
 Proof.
   iIntros "?". Show.
 Abort.