diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 0a20cfd6c0b2bdb1721985269828dc59d4653c09..d62a732451a9673130ed42898e147529cefa6f87 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -659,14 +659,14 @@ Tactic failure: iLöb: no 'BiLöb' instance found.
 1 subgoal
   
   PROP : bi
-  P1 : PROP
-  P2, P3 : Prop
-  Himpl : P2 → P3
-  HP2 : P2
+  P : PROP
+  φ1, φ2 : Prop
+  Himpl : φ1 → φ2
+  HP2 : φ1
   ============================
-  "HP" : P1
+  "HP" : P
   --------------------------------------∗
-  P1 ∗ ⌜P3⌝
+  P ∗ ⌜φ2⌝
   
 "test_not_fresh"
      : string
diff --git a/tests/proofmode.v b/tests/proofmode.v
index fb17541b694ece2405c436bf7017d058ea369025..901ac767ece923854da73e679a568509dba42ab4 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1245,8 +1245,8 @@ Ltac ltac_tactics.string_to_ident_hook ::=
                                         end).
 
 Check "test_pure_name".
-Lemma test_pure_name P1 (P2 P3: Prop) (Himpl: P2 -> P3) :
-  P1 ∗ ⌜P2⌝ -∗ P1 ∗ ⌜P3⌝.
+Lemma test_pure_name P (φ1 φ2 : Prop) (Himpl : φ1 → φ2) :
+  P ∗ ⌜φ1⌝ -∗ P ∗ ⌜φ2⌝.
 Proof.
   iIntros "[HP %HP2]".
   Show.
@@ -1260,8 +1260,8 @@ Lemma test_iIntros_forall_pure_named (Ψ: nat → PROP) :
 Proof. iIntros "HP". iIntros "%y". iApply ("HP" $! y). Qed.
 
 Check "test_not_fresh".
-Lemma test_not_fresh P1 (P2: Prop) (H:P2) :
-  P1 ∗ ⌜P2⌝ -∗ P1 ∗ ⌜P2⌝.
+Lemma test_not_fresh P (φ : Prop) (H : φ) :
+  P ∗ ⌜ φ ⌝ -∗ P ∗ ⌜ φ ⌝.
 Proof.
   Fail iIntros "[H %H]".
 Abort.