diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index bc5b6d18..105a5508 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -18,6 +18,8 @@ jobs:
       matrix:
         image:
           - 'rocq/rocq-prover:dev'
+          - 'rocq/rocq-prover:9.2'
+          - 'rocq/rocq-prover:9.1'
           - 'rocq/rocq-prover:9.0'
           - 'coqorg/coq:8.20'
           - 'coqorg/coq:8.19'
diff --git a/coq-corn.opam b/coq-corn.opam
index 790b1065..277d2b6c 100644
--- a/coq-corn.opam
+++ b/coq-corn.opam
@@ -46,10 +46,11 @@ build: [
 ]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.19" & < "9.1~") | (= "dev")}
-  "coq-math-classes" {(>= "8.8.1") | (= "dev")}
-  "coq-elpi" {(>= "1.18.0") | (= "dev")}
-  "coq-bignums" 
+  ("coq" {>= "8.19" & < "8.21~"}
+  | "rocq-core" {(>= "9.0" & < "9.3~") | (= "dev")})
+  ("coq-math-classes" {>= "8.8.1"} | "rocq-math-classes")
+  ("coq-elpi" {>= "1.18.0"} | "rocq-elpi")
+  "coq-bignums"
 ]
 
 tags: [
diff --git a/meta.yml b/meta.yml
index 388bd450..738cce0e 100644
--- a/meta.yml
+++ b/meta.yml
@@ -81,11 +81,20 @@ license:
   identifier: GPL-2.0
 
 supported_coq_versions:
-  text: Coq 8.19 or greater
-  opam: '{(>= "8.19" & < "8.20~") | (= "dev")}'
+  text: Coq 8.19 to 8.20 or Rocq 9.0 to 9.2
+  # Rocq 9.2 drops the `coq` compatibility opam package, so the compiler and
+  # elpi dependencies are hand-written as disjunctions (coq/rocq-core,
+  # coq-elpi/rocq-elpi) in coq-corn.opam; this field is kept for reference.
+  opam: '{>= "8.19" & < "8.21~"} | "rocq-core" {(>= "9.0" & < "9.3~") | (= "dev")}'
 
-tested_coq_opam_versions:
+tested_rocq_opam_versions:
 - version: dev
+- version: "9.2"
+- version: "9.1"
+- version: "9.0"
+
+tested_coq_opam_versions:
+- version: "8.20"
 - version: "8.19"
 
 dependencies: