From cc54c166e227ffb8f5a308e20e1c0cf602a021b7 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 29 Aug 2023 10:13:58 +0200
Subject: [PATCH] export lock from spin_lock

---
 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 c449f45c6..193785389 100644
--- a/iris_heap_lang/lib/spin_lock.v
+++ b/iris_heap_lang/lib/spin_lock.v
@@ -3,7 +3,7 @@ From iris.proofmode Require Import proofmode.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
-From iris.heap_lang.lib Require Import lock.
+From iris.heap_lang.lib Require Export lock.
 From iris.prelude Require Import options.
 
 Local Definition newlock : val := λ: <>, ref #false.
-- 
GitLab