Commit 8d20d87c authored by Simon Friis Vindum's avatar Simon Friis Vindum
Browse files

Rename gmap_view_persist into gmap_view_frag_persist

parent d6881996
Pipeline #55818 failed with stage
in 5 minutes and 58 seconds
......@@ -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
......
......@@ -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] /=.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment