Rename gmap_view_persist into gmap_view_frag_persist

CHANGELOG.md

@@ -160,6 +160,7 @@ s/\bgset_bij_auth_frac_(\w*)\b/gset_bij_auth_dfrac_\1/g
 s/\bgset_bij_auth_empty_frac_valid\b/gset_bij_auth_empty_dfrac_valid/g
 s/\bbij_both_frac_valid\b/bij_both_dfrac_valid/g
 s/\bgmap_view_(auth|both)_frac_(op_invN|op_inv|op_inv_L|valid|op_validN|op_valid|op_valid_L)\b/gmap_view_\1_dfrac_\2/g
+s/\bgmap_view_persist\b/gmap_view_frag_persist/g
 s/\bghost_map_elem_frac_ne\b/ghost_map_elem_dfrac_ne/g
 # big_sepM renames
 s/\bbig_sepM2_lookup_1\b/big_sepM2_lookup_l/g

iris/algebra/lib/gmap_view.v

@@ -407,7 +407,7 @@ Section lemmas.
     gmap_view_auth dq m ~~> gmap_view_auth DfracDiscarded m.
   Proof. apply view_update_auth_persist. Qed.
 
-  Lemma gmap_view_persist k dq v :
+  Lemma gmap_view_frag_persist k dq v :
     gmap_view_frag k dq v ~~> gmap_view_frag k DfracDiscarded v.
   Proof.
     apply view_update_frag=>m n bf Hrel j [df va] /=.

iris/base_logic/lib/ghost_map.v

@@ -114,7 +114,7 @@ Section lemmas.
     k1 ↪[γ] v1 -∗ k2 ↪[γ]{dq2} v2 -∗ ⌜k1 ≠ k2⌝.
   Proof. apply ghost_map_elem_dfrac_ne. apply: exclusive_l. Qed.
 
-  (** Make an element read-only. *)
+  (** Make a the authorative element read-only. *)
   Lemma ghost_map_auth_persist γ dq m :
     ghost_map_auth γ dq m ==∗ ghost_map_auth γ DfracDiscarded m.
   Proof. unseal. iApply own_update. apply gmap_view_auth_persist. Qed.
@@ -122,7 +122,7 @@ Section lemmas.
   (** Make an element read-only. *)
   Lemma ghost_map_elem_persist k γ dq v :
     k ↪[γ]{dq} v ==∗ k ↪[γ]□ v.
-  Proof. unseal. iApply own_update. apply gmap_view_persist. Qed.
+  Proof. unseal. iApply own_update. apply gmap_view_frag_persist. Qed.
 
   (** * Lemmas about [ghost_map_auth] *)
   Lemma ghost_map_alloc_strong P m :