diff --git a/theories/heap_lang/lib/lock.v b/theories/heap_lang/lib/lock.v index 5796f1f917d042e881c67e3ecd5177eaa6a0dc99..720dcc19aa4af6c4696ed456ae0167c6f797ac7d 100644 --- a/theories/heap_lang/lib/lock.v +++ b/theories/heap_lang/lib/lock.v @@ -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 {_ _} _.