diff --git a/coq-reloc.opam b/coq-reloc.opam
index 7cb4689f0a9bbbf0cb698caa209b39cd3152374f..b708dc830caa742c511fdf2733f3c6bdddc4e900 100644
--- a/coq-reloc.opam
+++ b/coq-reloc.opam
@@ -6,7 +6,7 @@ bug-reports: "https://gitlab.mpi-sws.org/dfrumin/reloc/issues"
 dev-repo: "git+https://gitlab.mpi-sws.org/dfrumin/reloc.git"
 
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2023-06-14.0.f0e415b6") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2023-08-29.5.af0a091b") | (= "dev") }
   "coq-autosubst" { = "dev" }
 ]
 
diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v
index 4d57628e47be2ddf2ea407d536182ee72fb8dbc9..c81377b0a6b9175f2c7ae3a62f3aeba0b42422dc 100644
--- a/theories/examples/ticket_lock.v
+++ b/theories/examples/ticket_lock.v
@@ -8,7 +8,8 @@ From iris.heap_lang.lib Require Export ticket_lock.
 (* A different `acquire` funciton to showcase the atomic rule for FG_increment *)
 Definition acquire : val := λ: "lk",
   let: "n" := FG_increment (Snd "lk") in
-  wait_loop "n" "lk".
+  (* breaking the ticket-lock abstraction... *)
+  ticket_lock.wait_loop "n" "lk".
 (* A different `release` function to showcase the rule for wkincr *)
 Definition release : val := λ: "lk", wkincr (Fst "lk").
 
@@ -128,7 +129,7 @@ Section refinement.
   Lemma wait_loop_refinement (lo ln : loc) γ lk (m : nat) :
     inv N (lockInv lo ln γ lk) -∗
     ticket γ m -∗
-    REL wait_loop #m (#lo, #ln)%V << reloc.lib.lock.acquire lk : ().
+    REL ticket_lock.wait_loop #m (#lo, #ln)%V << reloc.lib.lock.acquire lk : ().
   Proof.
     iIntros "#Hinv Hticket".
     rel_rec_l.
diff --git a/theories/experimental/hocap/ticket_lock.v b/theories/experimental/hocap/ticket_lock.v
index d0f33f98240358c25cd8e7128e1c4c5fb2f972e8..22f1f1abe0fd6f3df3083040cd7c2b58c191ca7c 100644
--- a/theories/experimental/hocap/ticket_lock.v
+++ b/theories/experimental/hocap/ticket_lock.v
@@ -37,7 +37,8 @@ Section refinement.
     Cnt (N.@"cnt1") cn γln -∗
     Cnt (N.@"cnt2") co γlo -∗
     ticket γ m -∗
-    REL wait_loop #m (co, cn)%V << spin_lock.acquire l' : ().
+    (* breaking the ticket_lock abstraction... *)
+    REL ticket_lock.wait_loop #m (co, cn)%V << spin_lock.acquire l' : ().
   Proof.
     iIntros "#Hinv #Hcntn #Hcnto Hticket".
     iLöb as "IH". rel_rec_l.