diff --git a/_CoqProject b/_CoqProject
index beae3548e47c677d13b0c28b1ff4e4153a3e3137..8ab07cf5218cb7253adbc62a75d39f38b5fd0753 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -6,6 +6,9 @@
 -arg -w -arg -redundant-canonical-projection
 # Warning seems incorrect, see https://gitlab.mpi-sws.org/iris/stdpp/-/issues/216
 -arg -w -arg -notation-incompatible-prefix
+# We can't do this migration yet until we require Coq 9.0
+-arg -w -arg -deprecated-from-Coq
+-arg -w -arg -deprecated-dirpath-Coq
 
 theories/logic/satisfiable.v
 theories/simulation/language.v
diff --git a/coq-simuliris.opam b/coq-simuliris.opam
index 06cc5342b4727bb02e75b034e62bc5d7a7bf996e..05fa0ef8a031497334e72f97dfb7aa2469de599c 100644
--- a/coq-simuliris.opam
+++ b/coq-simuliris.opam
@@ -9,7 +9,7 @@ synopsis: "Local Simulation proofs, the Iris style"
 
 depends: [
   "coq-iris" { (= "dev.2025-01-25.1.8a8f05fb") | (= "dev") }
-  "coq-equations" { (= "1.3+8.19") | (= "1.3.1+8.20") | (= "dev") }
+  "coq-equations" { (= "1.3+8.19") | (= "1.3.1+8.20") | (= "1.3.1+8.21") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]