diff --git a/iris_heap_lang/lib/spin_lock.v b/iris_heap_lang/lib/spin_lock.v index 1937853890831fcd26bd041c398e8a8c9bba1977..8686e3e03de742d8dc0fc86ffbaf1f4e323bf2fe 100644 --- a/iris_heap_lang/lib/spin_lock.v +++ b/iris_heap_lang/lib/spin_lock.v @@ -10,7 +10,7 @@ Local Definition newlock : val := λ: <>, ref #false. Local Definition try_acquire : val := λ: "l", CAS "l" #false #true. Local Definition acquire : val := rec: "acquire" "l" := if: try_acquire "l" then #() else "acquire" "l". -Definition release : val := λ: "l", "l" <- #false. +Local Definition release : val := λ: "l", "l" <- #false. (** The CMRA we need. *) (* Not bundling heapGS, as it may be shared with other users. *)