diff --git a/coq-reloc.opam b/coq-reloc.opam
index f1cbb1d4a07efa70ccee39d51a84105f0b4a7c88..303c91722036b20804d2cf75c77d2b4a3c8a6a99 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.2024-02-16.1.06f499e0") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2024-08-16.3.8890e30a") | (= "dev") }
   "coq-autosubst" { = "dev" }
 ]
 
diff --git a/theories/examples/folly_queue/refinement.v b/theories/examples/folly_queue/refinement.v
index 1f0315848abb6d53fa7600ff9e7cfa181d599d0c..fd8e56476b6feee2e4f9b7ae89fb7461eaeb708a 100644
--- a/theories/examples/folly_queue/refinement.v
+++ b/theories/examples/folly_queue/refinement.v
@@ -68,12 +68,12 @@ Section queue_refinement.
     list_idx_to_map (xs ++ [x]) = <[length xs := x]>(list_idx_to_map xs).
   Proof.
     rewrite /list_idx_to_map.
-    rewrite app_length /= Nat.add_1_r.
+    rewrite length_app /= Nat.add_1_r.
     rewrite seq_S /=.
     rewrite zip_with_app /=.
-    2: { by rewrite seq_length. }
+    2: { by rewrite length_seq. }
     rewrite list_to_map_snoc; first done.
-    rewrite fst_zip. 2: { rewrite seq_length. done. }
+    rewrite fst_zip. 2: { rewrite length_seq. done. }
     intros [i Hl]%elem_of_list_lookup_1.
     apply lookup_seq in Hl as Hlm.
     simpl in Hlm.
@@ -116,7 +116,7 @@ Section queue_refinement.
     rewrite /list_idx_to_map.
     rewrite lookup_fmap.
     rewrite not_elem_of_list_to_map_1; first done.
-    rewrite fst_zip. 2: { rewrite seq_length. done. }
+    rewrite fst_zip. 2: { rewrite length_seq. done. }
     rewrite elem_of_list_In.
     rewrite in_seq. lia.
   Qed.
@@ -139,7 +139,7 @@ Section queue_refinement.
     rewrite dom_singleton_L in Hincl.
     rewrite dom_make_map in Hincl.
     rewrite dom_list_to_map in Hincl.
-    rewrite fst_zip in Hincl. 2: { rewrite seq_length. done. }
+    rewrite fst_zip in Hincl. 2: { rewrite length_seq. done. }
     rewrite list_to_set_seq in Hincl.
     iPureIntro. set_solver.
   Qed.
@@ -159,7 +159,7 @@ Section queue_refinement.
     rewrite lookup_fmap.
     erewrite elem_of_list_to_map_1.
     - simpl. reflexivity.
-    - rewrite fst_zip. 2: { rewrite seq_length. done. }
+    - rewrite fst_zip. 2: { rewrite length_seq. done. }
       apply NoDup_seq.
     - apply elem_of_lookup_zip_with.
       exists i, i, x.
@@ -729,7 +729,7 @@ Section queue_refinement.
         iFrame. simpl.
         rewrite big_sepS_empty.
         iPureIntro. split; last done. split.
-        { rewrite app_length. simpl. lia. }
+        { rewrite length_app. simpl. lia. }
         rewrite drop_app_le; last lia.
         rewrite Hlisteq. done. }
       rel_pures_l.
@@ -782,8 +782,8 @@ Section queue_refinement.
         assert (popTicket `max` (pushTicket + 1) = popTicket `max` pushTicket) as -> by lia.
         simpl. iFrame.
         iPureIntro. split.
-        - rewrite app_length. simpl. lia.
-        - apply drop_ge. rewrite app_length. simpl. lia. }
+        - rewrite length_app. simpl. lia.
+        - apply drop_ge. rewrite length_app. simpl. lia. }
 
       rel_pures_l.
       rel_bind_l (! _)%E.
diff --git a/theories/examples/symbol.v b/theories/examples/symbol.v
index 46b2b068d69a2c5816e6b45bea281a78a77eee54..335ff1c7b146fbd5c1bafa03eb3f8680de2ea542 100644
--- a/theories/examples/symbol.v
+++ b/theories/examples/symbol.v
@@ -273,7 +273,7 @@ Section proof.
       rel_store_l_atomic.
       iClear "Hls".
       iInv sizeN as (m ls) "(Ha & >Hs1 & >Hs2 & >Htbl1 & >Htbl2 & #Hls)" "Hcl".
-      iDestruct (gen_heap.pointsto_agree with "Htbl1 Htbl1'") as %->.
+      iDestruct (pointsto_agree with "Htbl1 Htbl1'") as %->.
       iCombine "Htbl1 Htbl1'" as "Htbl1".
       iModIntro. iExists _. iFrame. iNext. iIntros "[Htbl1 Htbl1']".
       repeat rel_pure_l. repeat rel_pure_r. rel_load_r.
diff --git a/theories/logic/spec_ra.v b/theories/logic/spec_ra.v
index 0ead2bdf03fbb9dd70f08aaac132bf2bfb6208f6..76f1a818cae3b7142c867b5823159e93051742ca 100644
--- a/theories/logic/spec_ra.v
+++ b/theories/logic/spec_ra.v
@@ -109,7 +109,7 @@ Section conversions.
     - rewrite lookup_insert_ne; last lia. by rewrite !tpool_lookup lookup_app_l.
     - by rewrite lookup_insert tpool_lookup lookup_app_r // Nat.sub_diag.
     - rewrite lookup_insert_ne; last lia.
-      rewrite !tpool_lookup ?lookup_ge_None_2 ?app_length //=;
+      rewrite !tpool_lookup ?lookup_ge_None_2 ?length_app //=;
          change (ofe_car exprO) with expr; lia.
   Qed.
 
diff --git a/theories/logic/spec_rules.v b/theories/logic/spec_rules.v
index da703eb0148ae1bd76dc3e02055ba38cdbf30ad0..837480fb3dcaf2b12172825bd4f946c38457110a 100644
--- a/theories/logic/spec_rules.v
+++ b/theories/logic/spec_rules.v
@@ -29,7 +29,7 @@ Section rules.
     erased_step (tp, σ) (<[j:=fill K e']> tp ++ efs, σ').
   Proof.
     intros. rewrite -(take_drop_middle tp j (fill K e)) //.
-    rewrite insert_app_r_alt take_length_le ?Nat.sub_diag /=;
+    rewrite insert_app_r_alt length_take_le ?Nat.sub_diag /=;
       eauto using lookup_lt_Some, Nat.lt_le_incl.
     rewrite -(assoc_L (++)) /=. eexists.
     eapply step_atomic; eauto. by apply: Ectx_step'.
@@ -359,7 +359,7 @@ Section rules.
       by rewrite lookup_ge_None_2. }
     iExists (length tp). iFrame "Hj Hfork". iApply "Hclose". iNext.
     iExists (<[j:=fill K #()]> tp ++ [e]), σ.
-    rewrite to_tpool_snoc insert_length to_tpool_insert //. iFrame. iPureIntro.
+    rewrite to_tpool_snoc length_insert to_tpool_insert //. iFrame. iPureIntro.
     eapply rtc_r, step_insert; eauto. econstructor; eauto.
   Qed.