From 116780733496d126eeaa031be1f303e9a19db507 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 21 Jul 2020 13:08:53 +0200
Subject: [PATCH] Tweak some names in test file.

---
 tests/proofmode.ref | 12 ++++++------
 tests/proofmode.v   |  8 ++++----
 2 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 0a20cfd6c..d62a73245 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 fb17541b6..901ac767e 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.
-- 
GitLab