From 45b41b926e7d7756d82b3f5c16dfef9d83ef5be3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 6 Oct 2020 20:05:43 +0200
Subject: [PATCH] Rename `auth_update_core_id` into `auth_update_frac_alloc`.

Also rename the recently added `view_update_alloc_frac` into
`view_update_frac_alloc` to be consistent with other lemmas about the
placement of `_frac`.
---
 theories/algebra/auth.v | 4 ++--
 theories/algebra/view.v | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 320f987aa..c53598628 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -278,10 +278,10 @@ Section auth.
     exact: cmra_update_op_l.
   Qed.
 
-  Lemma auth_update_core_id q a b `{!CoreId b} :
+  Lemma auth_update_frac_alloc q a b `{!CoreId b} :
     b ≼ a → ●{q} a ~~> ●{q} a ⋅ ◯ b.
   Proof.
-    intros Ha%(core_id_extract _ _). apply view_update_alloc_frac=> n bf [??].
+    intros Ha%(core_id_extract _ _). apply view_update_frac_alloc=> n bf [??].
     split; [|done]. rewrite Ha (comm _ a). by apply cmra_monoN_l.
   Qed.
 
diff --git a/theories/algebra/view.v b/theories/algebra/view.v
index e0411c7fe..94fe19030 100644
--- a/theories/algebra/view.v
+++ b/theories/algebra/view.v
@@ -525,7 +525,7 @@ Section cmra.
     rewrite !cmra_total_update view_validN_eq=> ?? n [[[q ag]|] bf]; naive_solver.
   Qed.
 
-  Lemma view_update_alloc_frac q a b :
+  Lemma view_update_frac_alloc q a b :
     (∀ n bf, rel n a bf → rel n a (b ⋅ bf)) →
     ●V{q} a ~~> ●V{q} a ⋅ ◯V b.
   Proof.
-- 
GitLab