diff --git a/coq-actris.opam b/coq-actris.opam
index bf97f2aa735a05d1808542fc4b597f64ed2f4d51..99cd19fb637b747791d17047674d6a40d0f2354d 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.2022-08-03.2.75c9df64") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2022-08-12.4.9245c4c0") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/utils/llist.v b/theories/utils/llist.v
index 28c7ac18a720c9ac39be0084c12b3e7692cdf2c7..1e1920e377c9b161f5d04eeedcd8bc3667a9b6c8 100644
--- a/theories/utils/llist.v
+++ b/theories/utils/llist.v
@@ -253,7 +253,7 @@ Lemma lsplit_spec l xs :
 Proof.
   iIntros (Φ) "Hl HΦ". wp_lam.
   wp_smart_apply (llength_spec with "Hl"); iIntros "Hl". wp_pures.
-  rewrite Z.quot_div_nonneg; [|lia..]. rewrite -(Nat2Z_inj_div _ 2).
+  rewrite Z.quot_div_nonneg; [|lia..]. rewrite -(Nat2Z.inj_div _ 2).
   wp_smart_apply (lsplit_at_spec with "Hl"); iIntros (k) "[Hl Hk]".
   iApply "HΦ". iFrame. by rewrite take_drop.
 Qed.