Skip to content
Snippets Groups Projects
Commit ebe7b443 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Use auth_update_no_frame in boxes.

parent 8b6f2178
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 2 deletions
program_logic/boxes.v
+ 1
− 2
View file @ ebe7b443
......@@ -70,8 +70,7 @@ Proof.
rewrite /box_own_prop -!own_op own_valid_l prod_validI; iIntros "[[Hb _] Hγ]".
iDestruct "Hb" as % [[[] [= ->]%leibniz_equiv] ?]%auth_valid_discrete.
iApply (@own_update with "Hγ"); apply prod_update; simpl; last reflexivity.
rewrite -{1}(right_id ∅ _ (Excl' b2)) -{1}(right_id ∅ _ (Excl' b3)).
by apply auth_update, option_local_update, exclusive_local_update.
by apply auth_update_no_frame, option_local_update, exclusive_local_update.
Qed.
Lemma box_own_agree γ Q1 Q2 :
......
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