Commit 15c2d1ce authored by Joshua Yanovski's avatar Joshua Yanovski

Update lock.v

parent 87637946
Pipeline #4361 failed with stage
......@@ -26,8 +26,6 @@ Structure lock Σ `{!heapG Σ} := Lock {
{{{ is_lock N γ lk R locked γ R }}} release lk {{{ RET #(); True }}}
}.
Arguments newlock {_ _} _.
Arguments acquire {_ _} _.
Arguments release {_ _} _.
......
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