From 0412acb43fb362c39f5a97300f14a7342f00ea90 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 7 Nov 2019 16:27:01 +0100
Subject: [PATCH] Consistent variable names in `tests/proofmode_monpred.v`.

---
 tests/proofmode_monpred.ref | 18 +++++++++---------
 tests/proofmode_monpred.v   | 11 ++++++-----
 2 files changed, 15 insertions(+), 14 deletions(-)

diff --git a/tests/proofmode_monpred.ref b/tests/proofmode_monpred.ref
index 5b018493c..72d54d672 100644
--- a/tests/proofmode_monpred.ref
+++ b/tests/proofmode_monpred.ref
@@ -68,12 +68,12 @@ Tactic failure: iFrame: cannot frame (P i).
   Σ : gFunctors
   invG0 : invG Σ
   N : namespace
-  P : iProp Σ
+  𝓟 : iProp Σ
   ============================
-  "H" : ⎡ inv N (<pers> P) ⎤
-  "H2" : ⎡ ▷ <pers> P ⎤
+  "H" : ⎡ inv N (<pers> 𝓟) ⎤
+  "H2" : ⎡ ▷ <pers> 𝓟 ⎤
   --------------------------------------□
-  |={⊤ ∖ ↑N}=> ⎡ ▷ <pers> P ⎤ ∗ (|={⊤}=> ⎡ ▷ P ⎤)
+  |={⊤ ∖ ↑N}=> ⎡ ▷ <pers> 𝓟 ⎤ ∗ (|={⊤}=> ⎡ ▷ 𝓟 ⎤)
   
 1 subgoal
   
@@ -81,12 +81,12 @@ Tactic failure: iFrame: cannot frame (P i).
   Σ : gFunctors
   invG0 : invG Σ
   N : namespace
-  P : iProp Σ
+  𝓟 : iProp Σ
   ============================
-  "H" : ⎡ inv N (<pers> P) ⎤
-  "H2" : ⎡ ▷ <pers> P ⎤
+  "H" : ⎡ inv N (<pers> 𝓟) ⎤
+  "H2" : ⎡ ▷ <pers> 𝓟 ⎤
   --------------------------------------□
-  "Hclose" : ⎡ ▷ <pers> P ={⊤ ∖ ↑N,⊤}=∗ emp ⎤
+  "Hclose" : ⎡ ▷ <pers> 𝓟 ={⊤ ∖ ↑N,⊤}=∗ emp ⎤
   --------------------------------------∗
-  |={⊤ ∖ ↑N,⊤}=> ⎡ ▷ P ⎤
+  |={⊤ ∖ ↑N,⊤}=> ⎡ ▷ 𝓟 ⎤
   
diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index 41c98a140..013a1e199 100644
--- a/tests/proofmode_monpred.v
+++ b/tests/proofmode_monpred.v
@@ -174,18 +174,19 @@ Section tests_iprop.
   Context {I : biIndex} `{!invG Σ}.
 
   Local Notation monPred := (monPred I (iPropI Σ)).
-  Implicit Types P : iProp Σ.
+  Implicit Types P Q R : monPred.
+  Implicit Types 𝓟 𝓠 𝓡 : iProp Σ.
 
-  Lemma test_iInv_0 N P:
-    embed (B:=monPred) (inv N (<pers> P)) ={⊤}=∗  ⎡▷ P⎤.
+  Lemma test_iInv_0 N 𝓟 :
+    embed (B:=monPred) (inv N (<pers> 𝓟)) ={⊤}=∗ ⎡▷ 𝓟⎤.
   Proof.
     iIntros "#H".
     iInv N as "#H2". Show.
     iModIntro. iSplit=>//. iModIntro. iModIntro; auto.
   Qed.
 
-  Lemma test_iInv_0_with_close N P:
-    embed (B:=monPred) (inv N (<pers> P)) ={⊤}=∗ ⎡▷ P⎤.
+  Lemma test_iInv_0_with_close N 𝓟 :
+    embed (B:=monPred) (inv N (<pers> 𝓟)) ={⊤}=∗ ⎡▷ 𝓟⎤.
   Proof.
     iIntros "#H".
     iInv N as "#H2" "Hclose". Show.
-- 
GitLab