diff --git a/pkgs/development/coq-modules/mathcomp-finmap/default.nix b/pkgs/development/coq-modules/mathcomp-finmap/default.nix
index 3aab002a5897..9c6b4b2bd49f 100644
--- a/pkgs/development/coq-modules/mathcomp-finmap/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-finmap/default.nix
@@ -6,64 +6,74 @@
   version ? null,
 }:
 
-mkCoqDerivation {
+let
+  derivation = mkCoqDerivation {
 
-  namePrefix = [
-    "coq"
-    "mathcomp"
-  ];
-  pname = "finmap";
-  owner = "math-comp";
-  inherit version;
-  defaultVersion =
-    let
-      case = coq: mc: out: {
-        cases = [
-          coq
-          mc
-        ];
-        inherit out;
-      };
-    in
-    with lib.versions;
-    lib.switch
-      [ coq.coq-version mathcomp-boot.version ]
-      [
-        (case (range "8.20" "9.1") (range "2.3" "2.5") "2.2.2")
-        (case (range "8.20" "9.1") (range "2.3" "2.4") "2.2.0")
-        (case (range "8.16" "9.0") (range "2.0" "2.3") "2.1.0")
-        (case (range "8.16" "8.18") (range "2.0" "2.1") "2.0.0")
-        (case (range "8.13" "8.20") (range "1.12" "1.19") "1.5.2")
-        (case (isGe "8.10") (range "1.11" "1.17") "1.5.1")
-        (case (range "8.7" "8.11") "1.11.0" "1.5.0")
-        (case (isEq "8.11") (range "1.8" "1.10") "1.4.0+coq-8.11")
-        (case (range "8.7" "8.11.0") (range "1.8" "1.10") "1.4.0")
-        (case (range "8.7" "8.11.0") (range "1.8" "1.10") "1.3.4")
-        (case (range "8.7" "8.9") "1.7.0" "1.1.0")
-        (case (range "8.6" "8.7") (range "1.6.1" "1.7") "1.0.0")
-      ]
-      null;
-  release = {
-    "2.2.2".sha256 = "sha256-G5fSdx4MhOXtQ2H8lpyK5FuIbWAZNc7vRL3hcYmGA2o=";
-    "2.2.0".sha256 = "sha256-oDQEZOutrJxmN8FvzovUIhqw0mwc8Ej7thrieJrW8BY=";
-    "2.1.0".sha256 = "sha256-gh0cnhdVDyo+D5zdtxLc10kGKQLQ3ITzHnMC45mCtpY=";
-    "2.0.0".sha256 = "sha256-0Wr1ZUYVuZH74vawO4EZlZ+K3kq+s1xEz/BfzyKj+wk=";
-    "1.5.2".sha256 = "sha256-0KmmSjc2AlUo6BKr9RZ4FjL9wlGISlTGU0X1Eu7l4sw=";
-    "1.5.1".sha256 = "0ryfml4pf1dfya16d8ma80favasmrygvspvb923n06kfw9v986j7";
-    "1.5.0".sha256 = "0vx9n1fi23592b3hv5p5ycy7mxc8qh1y5q05aksfwbzkk5zjkwnq";
-    "1.4.1".sha256 = "0kx4nx24dml1igk0w0qijmw221r5bgxhwhl5qicnxp7ab3c35s8p";
-    "1.4.0+coq-8.11".sha256 = "1fd00ihyx0kzq5fblh9vr8s5mr1kg7p6pk11c4gr8svl1n69ppmb";
-    "1.4.0".sha256 = "0mp82mcmrs424ff1vj3cvd8353r9vcap027h3p0iprr1vkkwjbzd";
-    "1.3.4".sha256 = "0f5a62ljhixy5d7gsnwd66gf054l26k3m79fb8nz40i2mgp6l9ii";
-    "1.2.1".sha256 = "0jryb5dq8js3imbmwrxignlk5zh8gwfb1wr4b1s7jbwz410vp7zf";
-    "1.1.0".sha256 = "05df59v3na8jhpsfp7hq3niam6asgcaipg2wngnzxzqnl86srp2a";
-    "1.0.0".sha256 = "0sah7k9qm8sw17cgd02f0x84hki8vj8kdz7h15i7rmz08rj0whpa";
+    namePrefix = [
+      "coq"
+      "mathcomp"
+    ];
+    pname = "finmap";
+    owner = "math-comp";
+    inherit version;
+    defaultVersion =
+      let
+        case = coq: mc: out: {
+          cases = [
+            coq
+            mc
+          ];
+          inherit out;
+        };
+      in
+      with lib.versions;
+      lib.switch
+        [ coq.coq-version mathcomp-boot.version ]
+        [
+          (case (range "8.20" "9.1") (range "2.3" "2.5") "2.2.2")
+          (case (range "8.20" "9.1") (range "2.3" "2.4") "2.2.0")
+          (case (range "8.16" "9.0") (range "2.0" "2.3") "2.1.0")
+          (case (range "8.16" "8.18") (range "2.0" "2.1") "2.0.0")
+          (case (range "8.13" "8.20") (range "1.12" "1.19") "1.5.2")
+          (case (isGe "8.10") (range "1.11" "1.17") "1.5.1")
+          (case (range "8.7" "8.11") "1.11.0" "1.5.0")
+          (case (isEq "8.11") (range "1.8" "1.10") "1.4.0+coq-8.11")
+          (case (range "8.7" "8.11.0") (range "1.8" "1.10") "1.4.0")
+          (case (range "8.7" "8.11.0") (range "1.8" "1.10") "1.3.4")
+          (case (range "8.7" "8.9") "1.7.0" "1.1.0")
+          (case (range "8.6" "8.7") (range "1.6.1" "1.7") "1.0.0")
+        ]
+        null;
+    release = {
+      "2.2.2".sha256 = "sha256-G5fSdx4MhOXtQ2H8lpyK5FuIbWAZNc7vRL3hcYmGA2o=";
+      "2.2.0".sha256 = "sha256-oDQEZOutrJxmN8FvzovUIhqw0mwc8Ej7thrieJrW8BY=";
+      "2.1.0".sha256 = "sha256-gh0cnhdVDyo+D5zdtxLc10kGKQLQ3ITzHnMC45mCtpY=";
+      "2.0.0".sha256 = "sha256-0Wr1ZUYVuZH74vawO4EZlZ+K3kq+s1xEz/BfzyKj+wk=";
+      "1.5.2".sha256 = "sha256-0KmmSjc2AlUo6BKr9RZ4FjL9wlGISlTGU0X1Eu7l4sw=";
+      "1.5.1".sha256 = "0ryfml4pf1dfya16d8ma80favasmrygvspvb923n06kfw9v986j7";
+      "1.5.0".sha256 = "0vx9n1fi23592b3hv5p5ycy7mxc8qh1y5q05aksfwbzkk5zjkwnq";
+      "1.4.1".sha256 = "0kx4nx24dml1igk0w0qijmw221r5bgxhwhl5qicnxp7ab3c35s8p";
+      "1.4.0+coq-8.11".sha256 = "1fd00ihyx0kzq5fblh9vr8s5mr1kg7p6pk11c4gr8svl1n69ppmb";
+      "1.4.0".sha256 = "0mp82mcmrs424ff1vj3cvd8353r9vcap027h3p0iprr1vkkwjbzd";
+      "1.3.4".sha256 = "0f5a62ljhixy5d7gsnwd66gf054l26k3m79fb8nz40i2mgp6l9ii";
+      "1.2.1".sha256 = "0jryb5dq8js3imbmwrxignlk5zh8gwfb1wr4b1s7jbwz410vp7zf";
+      "1.1.0".sha256 = "05df59v3na8jhpsfp7hq3niam6asgcaipg2wngnzxzqnl86srp2a";
+      "1.0.0".sha256 = "0sah7k9qm8sw17cgd02f0x84hki8vj8kdz7h15i7rmz08rj0whpa";
+    };
+
+    propagatedBuildInputs = [ mathcomp-boot ];
+
+    meta = {
+      description = "Finset and finmap library";
+      license = lib.licenses.cecill-b;
+    };
   };
-
-  propagatedBuildInputs = [ mathcomp-boot ];
-
-  meta = {
-    description = "Finset and finmap library";
-    license = lib.licenses.cecill-b;
-  };
-}
+in
+# this is just a wrapper for rocqPackages.mathcomp-finmap for Rocq >= 9.0
+if coq.rocqPackages ? mathcomp-finmap then
+  coq.rocqPackages.mathcomp-finmap.override {
+    inherit version mathcomp-boot;
+    inherit (coq.rocqPackages) rocq-core;
+  }
+else
+  derivation
diff --git a/pkgs/development/rocq-modules/mathcomp-finmap/default.nix b/pkgs/development/rocq-modules/mathcomp-finmap/default.nix
new file mode 100644
index 000000000000..5fd9b61f82e4
--- /dev/null
+++ b/pkgs/development/rocq-modules/mathcomp-finmap/default.nix
@@ -0,0 +1,45 @@
+{
+  rocq-core,
+  mkRocqDerivation,
+  mathcomp-boot,
+  lib,
+  version ? null,
+}:
+
+mkRocqDerivation {
+
+  namePrefix = [
+    "rocq-core"
+    "mathcomp"
+  ];
+  pname = "finmap";
+  owner = "math-comp";
+  inherit version;
+  defaultVersion =
+    let
+      case = rocq: mc: out: {
+        cases = [
+          rocq
+          mc
+        ];
+        inherit out;
+      };
+    in
+    with lib.versions;
+    lib.switch
+      [ rocq-core.rocq-version mathcomp-boot.version ]
+      [
+        (case (range "9.0" "9.1") (range "2.3" "2.5") "2.2.2")
+      ]
+      null;
+  release = {
+    "2.2.2".sha256 = "sha256-G5fSdx4MhOXtQ2H8lpyK5FuIbWAZNc7vRL3hcYmGA2o=";
+  };
+
+  propagatedBuildInputs = [ mathcomp-boot ];
+
+  meta = {
+    description = "Finset and finmap library";
+    license = lib.licenses.cecill-b;
+  };
+}
diff --git a/pkgs/top-level/rocq-packages.nix b/pkgs/top-level/rocq-packages.nix
index 9ce17a5314c1..53f5720c53d9 100644
--- a/pkgs/top-level/rocq-packages.nix
+++ b/pkgs/top-level/rocq-packages.nix
@@ -47,6 +47,7 @@ let
       mathcomp-field = self.mathcomp.field;
       mathcomp-character = self.mathcomp.character;
       mathcomp-bigenough = callPackage ../development/rocq-modules/mathcomp-bigenough { };
+      mathcomp-finmap = callPackage ../development/rocq-modules/mathcomp-finmap { };
       parseque = callPackage ../development/rocq-modules/parseque { };
       relation-algebra = callPackage ../development/rocq-modules/relation-algebra { };
       rocq-elpi = callPackage ../development/rocq-modules/rocq-elpi { };