diff --git a/_CoqProject b/_CoqProject
index 198cf2a91544ca0b088c43b9b197aa01e681f6cf..98c2f076b3cca826aea30b599b26ed47dc77dc9e 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -17,6 +17,9 @@
 -arg -w -arg -redundant-canonical-projection
 # Fixing this one requires Coq 8.15.
 -arg -w -arg -deprecated-typeclasses-transparency-without-locality
+# Disabling warnings about future coercion syntax that requires Coq 8.17
+# (https://github.com/coq/coq/pull/16230)
+-arg -w -arg -future-coercion-class-field
 
 iris/prelude/options.v
 iris/prelude/prelude.v
diff --git a/coq-iris.opam b/coq-iris.opam
index 3880f2dfa13b73a4e125fe6ce5f48eb1f52731dd..285ff423bb55cc44d3e0d0899e5ecac44d5dcfa7 100644
--- a/coq-iris.opam
+++ b/coq-iris.opam
@@ -27,7 +27,7 @@ tags: [
 ]
 
 depends: [
-  "coq" { (>= "8.13" & < "8.17~") | (= "dev") }
+  "coq" { (>= "8.13" & < "8.18~") | (= "dev") }
   "coq-stdpp" { (= "dev.2023-03-24.1.504d165a") | (= "dev") }
 ]