diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index 25e9898..2fffbe1 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -21,6 +21,8 @@ jobs:
           - 'coqorg/coq:8.19'
           - 'coqorg/coq:8.18'
           - 'rocq/rocq-prover:dev'
+          - 'rocq/rocq-prover:9.2'
+          - 'rocq/rocq-prover:9.1'
           - 'rocq/rocq-prover:9.0'
       fail-fast: false
     steps:
diff --git a/coq-math-classes.opam b/coq-math-classes.opam
index 2dfd230..45d1310 100644
--- a/coq-math-classes.opam
+++ b/coq-math-classes.opam
@@ -30,8 +30,9 @@ build: [
 ]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.18" & < "9.1~") | (= "dev")}
-  "coq-bignums" 
+  ("coq" {>= "8.18" & < "8.21~"}
+  | "rocq-core" {(>= "9.0" & < "9.4~") | (= "dev")})
+  "coq-bignums"
 ]
 
 tags: [
diff --git a/meta.yml b/meta.yml
index c14301c..572fa6a 100644
--- a/meta.yml
+++ b/meta.yml
@@ -51,11 +51,16 @@ license:
   identifier: MIT
 
 supported_coq_versions:
-  text: Coq/Rocq 8.18 or later (use releases for other Coq/Rocq versions)
-  opam: '{(>= "8.18" & < "9.1~") | (= "dev")}'
+  text: Coq 8.18 to 8.20 or Rocq 9.0 to 9.3 (use releases for other Coq/Rocq versions)
+  # The coq-core/rocq-core split (Rocq 9.2 drops the `coq` compatibility
+  # package) means the compiler dependency must be hand-written as a
+  # disjunction in coq-math-classes.opam; this field is kept for reference.
+  opam: '{>= "8.18" & < "8.21~"} | "rocq-core" {(>= "9.0" & < "9.4~") | (= "dev")}'
 
 tested_rocq_opam_versions:
 - version: dev
+- version: "9.2"
+- version: "9.1"
 - version: "9.0"
 
 tested_coq_opam_versions: