Commit 351aadec authored by Ralf Jung's avatar Ralf Jung

val-unboxed-compatible list and mset

parent 5574a80a
......@@ -323,9 +323,6 @@ Section properties.
Global Instance cloc_to_val_inj : Inj (=) (=) cloc_to_val.
Proof. intros cl1 cl2 Hcl. apply (inj Some). by rewrite -!cloc_of_to_val Hcl. Qed.
Lemma cloc_to_val_for_compare cl :
val_for_compare (cloc_to_val cl) = cloc_to_val cl.
Proof. rewrite /cloc_to_val. unlock. done. Qed.
Lemma to_locking_heap_insert σ cl lv v :
to_locking_heap (<[cl:=(lv,v)]> σ) = <[cl:=(1%Qp, lv, to_agree v)]>(to_locking_heap σ).
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