diff --git a/coq-actris.opam b/coq-actris.opam
index 6a4adc2394169adc6146a472da304df39427cdbf..ddd01dbbc24993b62152d1fa4861056615ce507b 100644
--- a/coq-actris.opam
+++ b/coq-actris.opam
@@ -8,7 +8,7 @@ bug-reports: "https://gitlab.mpi-sws.org/iris/actris/issues"
 dev-repo: "git+https://gitlab.mpi-sws.org/iris/actris.git"
 
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2023-08-03.5.fe2b6d61") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2023-08-29.5.af0a091b") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 86d2ce9e566a9f1da3f7a34742109593b96ef2df..e17e6b73d09169711527e23a225451719e19a715 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -28,6 +28,8 @@ From actris.channel Require Export proto.
 From actris.utils Require Import llist skip.
 Set Default Proof Using "Type".
 
+Local Existing Instance spin_lock.
+
 (** * The definition of the message-passing connectives *)
 Definition new_chan : val :=
   λ: <>,
@@ -69,7 +71,7 @@ Class chanG Σ := {
   chanG_lockG :: lockG Σ;
   chanG_protoG :: protoG Σ val;
 }.
-Definition chanΣ : gFunctors := #[ lockΣ; protoΣ val ].
+Definition chanΣ : gFunctors := #[ spin_lockΣ; protoΣ val ].
 Global Instance subG_chanΣ {Σ} : subG chanΣ Σ → chanG Σ.
 Proof. solve_inG. Qed.
 
diff --git a/theories/examples/basics.v b/theories/examples/basics.v
index 29b7e326a4a69506402d2be370cb3c39196dcad4..ba010b6b865495ee65f51052b664d93375171ee4 100644
--- a/theories/examples/basics.v
+++ b/theories/examples/basics.v
@@ -4,6 +4,8 @@ From actris.channel Require Import proofmode.
 From iris.heap_lang Require Import lib.spin_lock.
 From actris.utils Require Import contribution.
 
+Local Existing Instance spin_lock.
+
 (** Basic *)
 Definition prog : val := λ: <>,
   let: "c" := start_chan (λ: "c'", send "c'" #42) in
diff --git a/theories/examples/par_map.v b/theories/examples/par_map.v
index cd84a106329a3165c896b254013c1643b97d56c9..525e0e922e0db3d44160cb0977a9428707613cfb 100644
--- a/theories/examples/par_map.v
+++ b/theories/examples/par_map.v
@@ -5,6 +5,8 @@ From iris.heap_lang Require Import lib.spin_lock.
 From actris.utils Require Import llist contribution.
 From iris.algebra Require Import gmultiset.
 
+Local Existing Instance spin_lock.
+
 (** * Distributed version (aka the implementation) *)
 Definition par_map_worker : val :=
   rec: "go" "map" "l" "c" :=
diff --git a/theories/examples/pizza.v b/theories/examples/pizza.v
index 6180e2296754a2ea7637ef089a8da6a84a31a010..b5674883171d4e9738fa22a3f5fedc976e1fe6ac 100644
--- a/theories/examples/pizza.v
+++ b/theories/examples/pizza.v
@@ -3,6 +3,8 @@ From actris.utils Require Import llist.
 From actris.channel Require Import proofmode.
 From stdpp Require Import list.
 
+Local Existing Instance spin_lock.
+
 Inductive pizza :=
   | Margherita
   | Calzone.
diff --git a/theories/logrel/examples/compute_client_list.v b/theories/logrel/examples/compute_client_list.v
index 6f9494b14f1ac0d822ec650f1d40fcb8fc848801..47d04d92a1407d91fb61393a4545fbdf7de819a2 100644
--- a/theories/logrel/examples/compute_client_list.v
+++ b/theories/logrel/examples/compute_client_list.v
@@ -22,6 +22,8 @@ From actris.logrel Require Import session_typing_rules napp.
 From actris.logrel.lib Require Import list par_start.
 From actris.logrel.examples Require Import compute_service.
 
+Local Existing Instance spin_lock.
+
 Definition send_all_par : val :=
   rec: "go" "c" "xs" "lk" "counter" :=
     if: lisnil "xs" then
@@ -56,7 +58,7 @@ Definition compute_client : val :=
     recv_all_par "c" "ys" "n" "lk" "counter");; "ys".
 
 Section compute_example.
-  Context `{heapGS Σ, chanG Σ, lockG Σ, spawnG Σ}.
+  Context `{heapGS Σ, chanG Σ, spin_lockG Σ, spawnG Σ}.
   Context `{!inG Σ fracR}.
 
   Definition compute_type_client_aux (rec : lsty Σ) : lsty Σ :=
diff --git a/theories/logrel/examples/par_recv.v b/theories/logrel/examples/par_recv.v
index 5b72a103391211ed4eec597388f6f7e44d4c2091..446ea7cb04159a7ed3b10d2e27f40ec090f995c1 100755
--- a/theories/logrel/examples/par_recv.v
+++ b/theories/logrel/examples/par_recv.v
@@ -18,6 +18,8 @@ From iris.heap_lang.lib Require Export par spin_lock.
 From actris.channel Require Import proofmode.
 From actris.logrel Require Export term_typing_judgment session_types.
 
+Local Existing Instance spin_lock.
+
 Definition prog : val := λ: "c",
   let: "lock" := newlock #() in
   (
diff --git a/theories/logrel/lib/mutex.v b/theories/logrel/lib/mutex.v
index eb5ca71642bcc2e57923ca403e7fd2ed1630c0cf..73df8f13674afa2f2cc1c9d792d7e08ca8e8a706 100644
--- a/theories/logrel/lib/mutex.v
+++ b/theories/logrel/lib/mutex.v
@@ -24,11 +24,13 @@ This type former is strongly inspired by the [Mutex] type in the standard
 library of Rust, which has also been semantically modelled in the LambdaRust
 project.
 *)
-From iris.heap_lang.lib Require Export spin_lock.
+From iris.heap_lang.lib Require Import spin_lock.
 From iris.heap_lang Require Import metatheory.
 From actris.channel Require Import proofmode.
 From actris.logrel Require Export term_types term_typing_judgment subtyping.
 
+Local Existing Instance spin_lock.
+
 (** Mutex functions *)
 Definition mutex_alloc : val := λ: "x", (newlock #(), ref "x").
 Definition mutex_acquire : val := λ: "x", acquire (Fst "x");; ! (Snd "x").
@@ -37,15 +39,15 @@ Definition mutex_release : val :=
 
 (** Semantic types *)
 Definition lty_mutex `{heapGS Σ, lockG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w,
-  ∃ (γ : gname) (l : loc) (lk : val),
+  ∃ (γ : lock_name) (l : loc) (lk : val),
     ⌜ w = (lk,#l)%V ⌝ ∗
     is_lock γ lk (∃ v_inner, l ↦ v_inner ∗ ltty_car A v_inner))%I.
 
 Definition lty_mutex_guard `{heapGS Σ, lockG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w,
-  ∃ (γ : gname) (l : loc) (lk : val) (v : val),
+  ∃ (γ : lock_name) (l : loc) (lk : val) (v : val),
     ⌜ w = (lk,#l)%V ⌝ ∗
     is_lock γ lk (∃ v_inner, l ↦ v_inner ∗ ltty_car A v_inner) ∗
-    spin_lock.locked γ ∗ l ↦ v)%I.
+    lock.locked γ ∗ l ↦ v)%I.
 
 Global Instance: Params (@lty_mutex) 3 := {}.
 Global Instance: Params (@lty_mutex_guard) 3 := {}.
@@ -73,7 +75,7 @@ Section properties.
   Proof.
     iIntros "#[Hle1 Hle2]" (v) "!>". iDestruct 1 as (γ l lk ->) "Hinv".
     iExists γ, l, lk. iSplit; first done.
-    iApply (spin_lock.is_lock_iff with "Hinv").
+    iApply (is_lock_iff with "Hinv").
     iIntros "!> !>". iSplit.
     - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl". by iApply "Hle1".
     - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl". by iApply "Hle2".
@@ -90,7 +92,7 @@ Section properties.
     iIntros "#[Hle1 Hle2]" (v) "!>".
     iDestruct 1 as (γ l lk w ->) "[Hinv [Hlock Hinner]]".
     iExists γ, l, lk, w. iSplit; first done.
-    iFrame "Hlock Hinner". iApply (spin_lock.is_lock_iff with "Hinv").
+    iFrame "Hlock Hinner". iApply (is_lock_iff with "Hinv").
     iIntros "!> !>". iSplit.
     - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl". by iApply "Hle1".
     - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl". by iApply "Hle2".
@@ -98,7 +100,7 @@ Section properties.
 End properties.
 
 Section rules.
-  Context `{heapGS Σ, lockG Σ}.
+  Context `{heapGS Σ, spin_lockG Σ}.
 
   (** Mutex properties *)
   Lemma ltyped_mutex_alloc Γ A :