diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 08a8a4a3f2a3b79f49fa53d5e04ccf398ade3d8d..31da8a1513c6cd0f2b396d6666db8a82c56751e3 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -47,11 +47,11 @@ build-coq.dev:
   variables:
     OPAM_PINS: "coq version dev"
 
-build-coq.8.15.0:
+build-coq.8.17.0:
   <<: *template
   variables:
     OCAML: "ocaml-variants.4.14.0+options ocaml-option-flambda"
-    OPAM_PINS: "coq version 8.15.0"
+    OPAM_PINS: "coq version 8.17.0"
     DENY_WARNINGS: "1"
     MANGLE_NAMES: "1"
     # Coq bench needs an opam package
@@ -60,11 +60,11 @@ build-coq.8.15.0:
   - fp-timing
 
 # Separate MR job that does not run on fp-timing.
-build-coq.8.15.0-mr:
+build-coq.8.17.0-mr:
   <<: *template
   <<: *only_mr
   variables:
-    OPAM_PINS: "coq version 8.15.0"
+    OPAM_PINS: "coq version 8.17.0"
     MANGLE_NAMES: "1"
     DENY_WARNINGS: "1"
 
@@ -72,7 +72,7 @@ trigger-iris.timing:
   <<: *template
   variables:
     OCAML: "ocaml-variants.4.14.0+options ocaml-option-flambda"
-    OPAM_PINS: "coq version 8.15.0   git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
+    OPAM_PINS: "coq version 8.17.0   git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
   tags:
   - fp-timing
   only:
diff --git a/README.md b/README.md
index a9cbc3e6a1393472e8426572ddc4c08b850a9f24..fbcf84848116b447b704440da231626e876ac67b 100644
--- a/README.md
+++ b/README.md
@@ -6,7 +6,7 @@ Some example verification demonstrating the use of Iris.
 
 This version is known to compile with:
 
- - Coq 8.15.0
+ - Coq 8.17.0
  - A development version of [Iris](https://gitlab.mpi-sws.org/iris/iris)
  - A development version of [Autosubst](https://github.com/coq-community/autosubst)
 
diff --git a/_CoqProject b/_CoqProject
index a5316e76dc2151fca37eb29249a85f8d349f00b3..2d5f7bce973af6d7d38ce5c595fcfd646f980738 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -4,6 +4,8 @@
 # Cannot use non-canonical projections as it causes massive unification failures
 # (https://github.com/coq/coq/issues/6294).
 -arg -w -arg -redundant-canonical-projection
+# Fixing this one requires Coq 8.17
+-arg -w -arg -future-coercion-class-field
 
 theories/barrier/proof.v
 theories/barrier/specification.v
diff --git a/coq-iris-examples.opam b/coq-iris-examples.opam
index 5f2b5988391736e5332445f97c1612157e6a080f..a8a9b31727c01816dd6e2b0f45ef19b27edd4ebb 100644
--- a/coq-iris-examples.opam
+++ b/coq-iris-examples.opam
@@ -8,7 +8,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/examples.git"
 synopsis: "A collection of case studies for Iris -- not meant to be used as a dependency of anything"
 
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2023-04-12.0.958aad09") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2023-05-02.4.943e9b74") | (= "dev") }
   "coq-autosubst" { = "dev" }
 ]