diff --git a/.github/workflows/deploy-docs-gh-pages.yml b/.github/workflows/deploy-docs-gh-pages.yml
index c80063a5dd..80a3437aac 100644
--- a/.github/workflows/deploy-docs-gh-pages.yml
+++ b/.github/workflows/deploy-docs-gh-pages.yml
@@ -24,8 +24,9 @@ jobs:
         with:
           ocaml-compiler: 4.14
           opam-repositories: |
-            coq-released: https://coq.inria.fr/opam/released
             default: https://github.com/ocaml/opam-repository.git
+            rocq-released: https://rocq-prover.org/opam/released
+            rocq-extra-dev: https://rocq-prover.org/opam/extra-dev
 
       - name: Build Mathcomp Analysis
         run: opam install -y --deps-only . --with-doc && opam exec -- make -j 4
diff --git a/.github/workflows/generate_docs.yml b/.github/workflows/generate_docs.yml
index 2de2827d05..ee1e2e3faf 100644
--- a/.github/workflows/generate_docs.yml
+++ b/.github/workflows/generate_docs.yml
@@ -1,3 +1,5 @@
+name: Generate HTML doc using Rocqnavi
+
 on:
   push:
     branches-ignore: ["gh-pages"]
@@ -31,8 +33,9 @@ jobs:
         with:
           ocaml-compiler: 4.14
           opam-repositories: |
-            coq-released: https://coq.inria.fr/opam/released
             default: https://github.com/ocaml/opam-repository.git
+            rocq-released: https://rocq-prover.org/opam/released
+            rocq-extra-dev: https://rocq-prover.org/opam/extra-dev
 
       - name: Build Mathcomp Analysis
         run: opam install -y --deps-only . --with-doc && opam exec -- make -j 4
diff --git a/rocq-mathcomp-classical.opam b/rocq-mathcomp-classical.opam
index 550a6f32e6..1d0be4b011 100644
--- a/rocq-mathcomp-classical.opam
+++ b/rocq-mathcomp-classical.opam
@@ -16,10 +16,10 @@ build: [make "-C" "classical" "-j%{jobs}%"]
 install: [make "-C" "classical" "install"]
 depends: [
   "rocq-core" { (>= "9.0" & < "9.2~") | (= "dev") }
-  "rocq-mathcomp-ssreflect" { (>= "2.5.0" & < "2.6~") | (= "dev") }
+  "rocq-mathcomp-ssreflect" { (= "dev") }
   "rocq-mathcomp-fingroup"
   "rocq-mathcomp-algebra"
-  "rocq-mathcomp-finmap" { (>= "2.1.0") }
+  "rocq-mathcomp-finmap" { (= "dev") }
   "rocq-hierarchy-builder" { (>= "1.8.0") }
 ]