diff --git a/iris_heap_lang/lib/spin_lock.v b/iris_heap_lang/lib/spin_lock.v
index c449f45c6f4484e7e7d8f32a5b49bc66764b4c82..1937853890831fcd26bd041c398e8a8c9bba1977 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.