From 2c0d03d407c314d1ee61471bf1bb1526e08b2bd5 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Tue, 29 Aug 2023 10:25:46 +0200 Subject: [PATCH] forgot to make this one Local --- iris_heap_lang/lib/spin_lock.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/iris_heap_lang/lib/spin_lock.v b/iris_heap_lang/lib/spin_lock.v index 193785389..8686e3e03 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. *) -- GitLab