compatibility with rocq (aka Coq) 9.0

_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

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}%"]