diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 52fe1233201f11fa0f01e6c8877a708d6135f461..9c89c7202cfdb8422af3f862ecd38d819c73ec2f 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -29,11 +29,11 @@ variables:
 
 ## Build jobs
 
-# build against known-working Coq 8.18.0
-build-coq.8.18.0:
+# build against known-working Coq 8.19.2
+build-coq.8.19.2:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.18.0"
+    OPAM_PINS: "coq version 8.19.2"
     #DENY_WARNINGS: "1"
     #MANGLE_NAMES: "1"
     #OPAM_PKG: "1"
@@ -44,7 +44,7 @@ build-iris.dev:
   variables:
     STDPP_REPO: "iris/stdpp"
     IRIS_REPO: "iris/iris"
-    OPAM_PINS: "coq version 8.18.dev   git+https://gitlab.mpi-sws.org/$STDPP_REPO#$STDPP_REV   git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
+    OPAM_PINS: "coq version 8.19.dev   git+https://gitlab.mpi-sws.org/$STDPP_REPO#$STDPP_REV   git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
   except:
   only:
   - triggers
diff --git a/semantics.opam b/semantics.opam
index 41493c33f2a3c926067840b37cc9ae1286c61157..5649e4c3a29733f0c596e1e49ac6992a1cbefcd5 100644
--- a/semantics.opam
+++ b/semantics.opam
@@ -9,10 +9,10 @@ bug-reports: "https://gitlab.mpi-sws.org/FP/semantics-course/issues"
 version: "dev"
 
 depends: [
-  "coq" { (>= "8.18" & < "8.19~") | (= "dev") }
-  "coq-iris-heap-lang" { (= "dev.2024-06-10.0.84ed8993") | (= "dev") }
-  "coq-equations" { (= "1.3+8.18") }
-  "coq-autosubst" { (= "1.8") | (= "dev")  }
+  "coq" { (>= "8.18" & < "8.20~") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2024-08-20.0.657b34ad") | (= "dev") }
+  "coq-equations" { (= "1.3+8.18") | = "1.3+8.19" }
+  "coq-autosubst" { (= "1.8") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/program_logics/heap_lang/derived_laws.v b/theories/program_logics/heap_lang/derived_laws.v
index e43905d49d470a2a6a8afcdd1d375db5cd44764c..2586fc67293a2a77d3d0e28f295a68f86d9c16a6 100644
--- a/theories/program_logics/heap_lang/derived_laws.v
+++ b/theories/program_logics/heap_lang/derived_laws.v
@@ -85,13 +85,13 @@ Proof.
   iDestruct (array_app with "Hl") as "[Hl1 Hl]".
   iDestruct (array_cons with "Hl") as "[Hl2 Hl3]".
   assert (off < length vs) as H by (apply lookup_lt_is_Some; by eexists).
-  rewrite take_length min_l; last by lia. iFrame "Hl2".
+  rewrite length_take min_l; last by lia. iFrame "Hl2".
   iIntros (w) "Hl2".
   clear Hlookup. assert (<[off:=w]> vs !! off = Some w) as Hlookup.
   { apply list_lookup_insert. lia. }
   rewrite -[in (l ↦∗{_} <[off:=w]> vs)%I](take_drop_middle (<[off:=w]> vs) off w Hlookup).
   iApply array_app. rewrite take_insert; last by lia. iFrame.
-  iApply array_cons. rewrite take_length min_l; last by lia. iFrame.
+  iApply array_cons. rewrite length_take min_l; last by lia. iFrame.
   rewrite drop_insert_gt; last by lia. done.
 Qed.
 
diff --git a/theories/program_logics/heap_lang/primitive_laws.v b/theories/program_logics/heap_lang/primitive_laws.v
index 5d766c664c2538d1dbac41f4e06442410c729ea1..194a07d4472ee3f9f53717b32d6a29d08e5545a1 100644
--- a/theories/program_logics/heap_lang/primitive_laws.v
+++ b/theories/program_logics/heap_lang/primitive_laws.v
@@ -118,7 +118,7 @@ Proof.
   iMod (gen_heap_alloc_big _ (heap_array _ (replicate (Z.to_nat n) v)) with "Hσ")
     as "(Hσ & Hl & Hm)".
   { apply heap_array_map_disjoint.
-    rewrite replicate_length Z2Nat.id; auto with lia. }
+    rewrite length_replicate Z2Nat.id; auto with lia. }
   iApply step_fupd_intro; first done.
   iModIntro. iFrame "Hσ". do 2 (iSplit; first done).
   iApply wp_value_fupd. iApply "HΦ".