Commit 335c29dd authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

`Free` is atomic.

parent 8f97d906
......@@ -123,6 +123,8 @@ Proof. solve_atomic. Qed.
Instance alloc_atomic s v w : Atomic s (AllocN (Val v) (Val w)).
Proof. solve_atomic. Qed.
Instance free_atomic s v : Atomic s (Free (Val v)).
Proof. solve_atomic. Qed.
Instance load_atomic s v : Atomic s (Load (Val v)).
Proof. solve_atomic. Qed.
Instance store_atomic s v1 v2 : Atomic s (Store (Val v1) (Val v2)).
......
Supports Markdown
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