Commit 226181b6 authored by Ralf Jung's avatar Ralf Jung

fix build

parent c34a636b
......@@ -27,7 +27,7 @@ Section proof.
Proof.
iIntros "Hp1 Hp2".
rewrite /bagPart -gmultiset_op_union -frac_op'.
rewrite frag_auth_op own_op. iFrame.
rewrite frac_auth_frag_op own_op. iFrame.
Qed.
Lemma bagPart_decompose (γ: gname) (q: Qp) (X Y : gmultiset val) :
bagPart γ q (X Y) - bagPart γ (q/2) X bagPart γ (q/2) Y.
......@@ -36,7 +36,7 @@ Section proof.
assert (q = (q/2)+(q/2))%Qp as Hq by (by rewrite Qp_div_2).
rewrite /bagPart {1}Hq.
rewrite -gmultiset_op_union -frac_op'.
rewrite frag_auth_op own_op. iFrame.
rewrite frac_auth_frag_op own_op. iFrame.
Qed.
Global Instance bagM_persistent γb γ x : Persistent (bagM γb γ x).
......
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