From 5d74ded95068dea995dade900b698c0d830954a0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 15 Nov 2017 17:21:08 +0100
Subject: [PATCH] =?UTF-8?q?Use=20`=CE=A6`=20and=20`=CE=A8`=20for=20predica?=
 =?UTF-8?q?tes=20in=20saved=5Fprop=20as=20we=20do=20everywhere.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/base_logic/lib/saved_prop.v | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index c07150d1f..73a957514 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -81,23 +81,23 @@ Qed.
 Notation savedPredG Σ A := (savedAnythingG Σ (constCF A -n> ▶ ∙)).
 Notation savedPredΣ A := (savedAnythingΣ (constCF A -n> ▶ ∙)).
 
-Definition saved_pred_own `{savedPredG Σ A} (γ : gname) (f: A -n> iProp Σ) :=
-  saved_anything_own (F := A -n> ▶ ∙) γ (CofeMor Next ◎ f).
+Definition saved_pred_own `{savedPredG Σ A} (γ : gname) (Φ : A -n> iProp Σ) :=
+  saved_anything_own (F := A -n> ▶ ∙) γ (CofeMor Next ◎ Φ).
 
-Lemma saved_pred_alloc_strong `{savedPredG Σ A} (G : gset gname) (f: A -n> iProp Σ) :
-  (|==> ∃ γ, ⌜γ ∉ G⌝ ∧ saved_pred_own γ f)%I.
+Lemma saved_pred_alloc_strong `{savedPredG Σ A} (G : gset gname) (Φ : A -n> iProp Σ) :
+  (|==> ∃ γ, ⌜γ ∉ G⌝ ∧ saved_pred_own γ Φ)%I.
 Proof. iApply saved_anything_alloc_strong. Qed.
 
-Lemma saved_pred_alloc `{savedPredG Σ A} (f: A -n> iProp Σ) :
-  (|==> ∃ γ, saved_pred_own γ f)%I.
+Lemma saved_pred_alloc `{savedPredG Σ A} (Φ : A -n> iProp Σ) :
+  (|==> ∃ γ, saved_pred_own γ Φ)%I.
 Proof. iApply saved_anything_alloc. Qed.
 
 (* We put the `x` on the outside to make this lemma easier to apply. *)
-Lemma saved_pred_agree `{savedPredG Σ A} γ f g x :
-  saved_pred_own γ f -∗ saved_pred_own γ g -∗ ▷ (f x ≡ g x).
+Lemma saved_pred_agree `{savedPredG Σ A} γ Φ Ψ x :
+  saved_pred_own γ Φ -∗ saved_pred_own γ Ψ -∗ ▷ (Φ x ≡ Ψ x).
 Proof.
-  iIntros "Hx Hy". unfold saved_pred_own. iApply later_equivI.
-  iDestruct (ofe_morC_equivI (CofeMor Next â—Ž f) (CofeMor Next â—Ž g)) as "[FE _]".
+  iIntros "HΦ HΨ". unfold saved_pred_own. iApply later_equivI.
+  iDestruct (ofe_morC_equivI (CofeMor Next ◎ Φ) (CofeMor Next ◎ Ψ)) as "[FE _]".
   simpl. iApply ("FE" with "[-]").
-  iApply (saved_anything_agree with "Hx Hy").
+  iApply (saved_anything_agree with "HΦ HΨ").
 Qed.
-- 
GitLab