From 250a4b8bb1a2e6cac22e40630a2170fc48468380 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 8 Mar 2021 13:59:44 +0100
Subject: [PATCH] =?UTF-8?q?rename=20reservation=5Fmap=5Falloc=5Fupdate=20?=
 =?UTF-8?q?=E2=86=92=20reservation=5Fmap=5Falloc?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 iris/algebra/reservation_map.v | 4 ++--
 iris/base_logic/lib/gen_heap.v | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/iris/algebra/reservation_map.v b/iris/algebra/reservation_map.v
index c23cbd067..a8993d193 100644
--- a/iris/algebra/reservation_map.v
+++ b/iris/algebra/reservation_map.v
@@ -14,7 +14,7 @@ properties of this camera are:
 - The lemma [reservation_map_token_union] enables one to split [reservation_map_token]
   w.r.t. disjoint union. That is, if we have [E1 ## E2], then we get
   [reservation_map_token (E1 ∪ E2) = reservation_map_token E1 ⋅ reservation_map_token E2].
-- The lemma [reservation_map_alloc_update] provides a frame preserving update to
+- The lemma [reservation_map_alloc] provides a frame preserving update to
   associate data to a key: [reservation_map_token E ~~> reservation_map_data k a]
   provided [k ∈ E] and [✓ a].
 
@@ -254,7 +254,7 @@ Proof.
   - intros i. rewrite lookup_op lookup_empty. auto.
 Qed.
 
-Lemma reservation_map_alloc_update E k a :
+Lemma reservation_map_alloc E k a :
   k ∈ E → ✓ a → reservation_map_token E ~~> reservation_map_data k a.
 Proof.
   intros ??. apply cmra_total_update=> n [mf [Ef|]] //.
diff --git a/iris/base_logic/lib/gen_heap.v b/iris/base_logic/lib/gen_heap.v
index 7bd723137..a172b30ea 100644
--- a/iris/base_logic/lib/gen_heap.v
+++ b/iris/base_logic/lib/gen_heap.v
@@ -231,7 +231,7 @@ Section gen_heap.
     rewrite meta_token_eq meta_eq /meta_token_def /meta_def.
     iDestruct 1 as (γm) "[Hγm Hm]". iExists γm. iFrame "Hγm".
     iApply (own_update with "Hm").
-    apply reservation_map_alloc_update; last done.
+    apply reservation_map_alloc; last done.
     cut (positives_flatten N ∈@{coPset} ↑N); first by set_solver.
     rewrite nclose_eq. apply elem_coPset_suffixes.
     exists 1%positive. by rewrite left_id_L.
-- 
GitLab