diff --git a/coq-reloc.opam b/coq-reloc.opam
index 4ad07266222373f540c42a9858ef6df79dd0abe9..f06d4d12b08c0e76e67cf4750ab75bd7a5cbe9dc 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-03-09.0.f91e8eab") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2023-03-17.1.a7a250e6") | (= "dev") }
   "coq-autosubst" { = "dev" }
 ]
 
diff --git a/theories/logic/spec_rules.v b/theories/logic/spec_rules.v
index 3834f8a4f1284660f93e9362e9bf8bf5e6fa6444..2bfb0ff9508a23c727a256ecf900db82b03dcdc3 100644
--- a/theories/logic/spec_rules.v
+++ b/theories/logic/spec_rules.v
@@ -154,7 +154,7 @@ Section rules.
     rewrite to_heap_insert to_tpool_insert'; last eauto. iFrame. iPureIntro.
     eapply rtc_r, step_insert_no_fork; eauto.
     rewrite -state_init_heap_singleton. eapply AllocNS; first by lia.
-    intros. assert (i = 0) as -> by lia. by rewrite loc_add_0.
+    intros. assert (i = 0) as -> by lia. by rewrite Loc.add_0.
   Qed.
 
   Lemma step_load E j K l q v: