diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index c7260dac..7b188ee8 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -21,7 +21,7 @@ jobs:
         opam_file:
           - 'coq-wasm.opam'
         coq_version:
-          - '8.20'
+          - '9.0'
       fail-fast: true
 
     steps:
diff --git a/coq-wasm.opam b/coq-wasm.opam
index 9408da4c..eec85a23 100644
--- a/coq-wasm.opam
+++ b/coq-wasm.opam
@@ -1,6 +1,6 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-version: "2.2.0"
+version: "2.2.1"
 synopsis: "Wasm formalisation in Coq"
 description:
   "Wasm formalisation in Coq, following the AFP formalisation of Conrad Watt"
@@ -13,11 +13,11 @@ homepage: "https://github.com/WasmCert/WasmCert-Coq"
 bug-reports: "https://github.com/WasmCert/WasmCert-Coq/issues"
 depends: [
   "dune" {>= "3.11"}
-  "coq" {>= "8.20" & < "8.21~"}
+  "coq" {>= "9.0" & < "9.2~"}
   "coq-compcert" {>= "3.14"}
   "coq-ext-lib" {>= "0.11.8"}
   "coq-mathcomp-ssreflect" {>= "2.4.0" & <= "2.5~"}
-  "coq-parseque" {>= "0.2.0"}
+  "rocq-parseque" {>= "0.2.0"}
   "cmdliner" {>= "1.1.0"}
   "linenoise" {>= "1.4.0"}
   "mdx" {>= "1.9.0"}
diff --git a/dune-project b/dune-project
index f73c878b..0f8bdbfe 100644
--- a/dune-project
+++ b/dune-project
@@ -2,7 +2,7 @@
 (using coq 0.2)
 (using mdx 0.2)
 (name coq-wasm)
-(version 2.2.0)
+(version 2.2.1)
 
 (generate_opam_files true)
 (license MIT)
@@ -15,11 +15,11 @@
   (synopsis "Wasm formalisation in Coq")
   (description "Wasm formalisation in Coq, following the AFP formalisation of Conrad Watt")
   (depends
-    (coq (and (>= 8.20) (< 8.21~)))
+    (coq (and (>= 9.0) (< 9.2~)))
     (coq-compcert (>= 3.14))
     (coq-ext-lib (>= 0.11.8))
     (coq-mathcomp-ssreflect (and (>= 2.4.0) (<= 2.5~)))
-    (coq-parseque (>= 0.2.0))
+    (rocq-parseque (>= 0.2.0))
     (cmdliner (>= 1.1.0))
     (linenoise (>= 1.4.0))
     (mdx (>= 1.9.0))