compatibility with rocq (aka Coq) 9.0

basically everything still works. cc @jung

_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

[Ralf Jung]

These would still be good to have in preparation for when we add 9.0 to CI. Do they fix all the warnings or are there more?