From 8912c3d2cc965f25e1f37f0c810264e8d5ffbab1 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 10 Oct 2020 09:41:39 +0200
Subject: [PATCH] API tweaks

---
 theories/algebra/lib/gmap_view.v   | 6 +++---
 theories/base_logic/lib/gen_heap.v | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/algebra/lib/gmap_view.v b/theories/algebra/lib/gmap_view.v
index 31b6f850a..a3a7b544f 100644
--- a/theories/algebra/lib/gmap_view.v
+++ b/theories/algebra/lib/gmap_view.v
@@ -164,7 +164,7 @@ Section lemmas.
   Lemma gmap_view_frag_op k dq1 dq2 v :
     gmap_view_frag k (dq1 ⋅ dq2) v ≡ gmap_view_frag k dq1 v ⋅ gmap_view_frag k dq2 v.
   Proof. rewrite -view_frag_op singleton_op -pair_op agree_idemp //. Qed.
-  Lemma gmap_view_frag_plus k q1 q2 v :
+  Lemma gmap_view_frag_add k q1 q2 v :
     gmap_view_frag k (DfracOwn (q1 + q2)) v ≡
       gmap_view_frag k (DfracOwn q1) v â‹… gmap_view_frag k (DfracOwn q2) v.
   Proof. rewrite -gmap_view_frag_op. done. Qed.
@@ -262,7 +262,7 @@ Section lemmas.
       rewrite lookup_insert_ne //.
   Qed.
 
-  Lemma gmap_view_freeze k q v :
+  Lemma gmap_view_persist k q v :
     gmap_view_frag k (DfracOwn q) v ~~> gmap_view_frag k DfracDiscarded v.
   Proof.
     apply view_update_frag; last first.
@@ -291,7 +291,7 @@ Section lemmas.
   Qed.
 
   (** Typeclass instances *)
-  Global Instance gmap_view_frag_core_id k v : CoreId (gmap_view_frag k DfracDiscarded v).
+  Global Instance gmap_view_frag_core_id k v : CoreId dq → CoreId (gmap_view_frag k dq v).
   Proof. apply _. Qed.
 
   Global Instance gmap_view_cmra_discrete : OfeDiscrete V → CmraDiscrete (gmap_viewR K V).
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index f12d9b6ad..d41b2f9d9 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -149,7 +149,7 @@ Section gen_heap.
   Proof. rewrite mapsto_eq /mapsto_def. apply _. Qed.
   Global Instance mapsto_fractional l v : Fractional (λ q, l ↦{q} v)%I.
   Proof.
-    intros p q. rewrite mapsto_eq /mapsto_def -own_op gmap_view_frag_plus //.
+    intros p q. rewrite mapsto_eq /mapsto_def -own_op gmap_view_frag_add //.
   Qed.
   Global Instance mapsto_as_fractional l q v :
     AsFractional (l ↦{q} v) (λ q, l ↦{q} v)%I q.
-- 
GitLab