diff --git a/pkgs/development/coq-modules/mathcomp-bigenough/default.nix b/pkgs/development/coq-modules/mathcomp-bigenough/default.nix
deleted file mode 100644
index 3ba007d9dd0a..000000000000
--- a/pkgs/development/coq-modules/mathcomp-bigenough/default.nix
+++ /dev/null
@@ -1,52 +0,0 @@
-{
-  coq,
-  mkCoqDerivation,
-  mathcomp-boot,
-  lib,
-  version ? null,
-}:
-
-let
-  derivation = mkCoqDerivation {
-
-    namePrefix = [
-      "coq"
-      "mathcomp"
-    ];
-    pname = "bigenough";
-    owner = "math-comp";
-
-    release = {
-      "1.0.0".hash = "sha256:10g0gp3hk7wri7lijkrqna263346wwf6a3hbd4qr9gn8hmsx70wg";
-      "1.0.1".hash = "sha256:02f4dv4rz72liciwxb2k7acwx6lgqz4381mqyq5854p3nbyn06aw";
-      "1.0.2".hash = "sha256-fJ/5xr91VtvpIoaFwb3PlnKl6UHG6GEeBRVGZrVLMU0=";
-      "1.0.3".hash = "sha256-9ObUoaavnninL72r5iqkLz7lJBpcKXXi8LXKGhgx/N4=";
-    };
-    inherit version;
-    defaultVersion =
-      let
-        case = case: out: { inherit case out; };
-      in
-      with lib.versions;
-      lib.switch coq.coq-version [
-        (case (range "8.10" "9.1") "1.0.3")
-        (case (range "8.10" "9.1") "1.0.2")
-        (case (range "8.5" "8.14") "1.0.0")
-      ] null;
-
-    propagatedBuildInputs = [ mathcomp-boot ];
-
-    meta = {
-      description = "Small library to do epsilon - N reasonning";
-      license = lib.licenses.cecill-b;
-    };
-  };
-in
-# this is just a wrapper for rocqPackages.mathcomp-bigenough for Rocq >= 9.0
-if coq.rocqPackages ? mathcomp-bigenough then
-  coq.rocqPackages.mathcomp-bigenough.override {
-    inherit version mathcomp-boot;
-    inherit (coq.rocqPackages) rocq-core;
-  }
-else
-  derivation
diff --git a/pkgs/development/rocq-modules/mathcomp-bigenough/default.nix b/pkgs/development/rocq-modules/mathcomp-bigenough/default.nix
index 0f6c1ce50129..924585a14513 100644
--- a/pkgs/development/rocq-modules/mathcomp-bigenough/default.nix
+++ b/pkgs/development/rocq-modules/mathcomp-bigenough/default.nix
@@ -6,32 +6,44 @@
   version ? null,
 }:
 
-mkRocqDerivation {
+let
+  derivation = mkRocqDerivation {
 
-  namePrefix = [
-    "rocq"
-    "mathcomp"
-  ];
-  pname = "bigenough";
-  owner = "math-comp";
+    namePrefix = [
+      "rocq"
+      "mathcomp"
+    ];
+    pname = "bigenough";
+    owner = "math-comp";
 
-  release = {
-    "1.0.4".sha256 = "sha256-cwfDCEFSXWnqV5aIrhTviUti0CXNwmFe6zVbqlD2iZw=";
+    release = {
+      "1.0.0".hash = "sha256:10g0gp3hk7wri7lijkrqna263346wwf6a3hbd4qr9gn8hmsx70wg";
+      "1.0.1".hash = "sha256:02f4dv4rz72liciwxb2k7acwx6lgqz4381mqyq5854p3nbyn06aw";
+      "1.0.2".hash = "sha256-fJ/5xr91VtvpIoaFwb3PlnKl6UHG6GEeBRVGZrVLMU0=";
+      "1.0.3".hash = "sha256-9ObUoaavnninL72r5iqkLz7lJBpcKXXi8LXKGhgx/N4=";
+      "1.0.4".sha256 = "sha256-cwfDCEFSXWnqV5aIrhTviUti0CXNwmFe6zVbqlD2iZw=";
+    };
+    inherit version;
+    defaultVersion =
+      let
+        case = case: out: { inherit case out; };
+      in
+      with lib.versions;
+      lib.switch rocq-core.rocq-version [
+        (case (range "9.0" "9.3") "1.0.4")
+        (case (range "8.10" "9.1") "1.0.3")
+        (case (range "8.10" "9.1") "1.0.2")
+        (case (range "8.5" "8.14") "1.0.0")
+      ] null;
+
+    propagatedBuildInputs = [ mathcomp-boot ];
+
+    useCoqifVersion = v: v != null && v != "dev" && lib.versions.isLe "1.0.3" v;
+
+    meta = {
+      description = "Small library to do epsilon - N reasonning";
+      license = lib.licenses.cecill-b;
+    };
   };
-  inherit version;
-  defaultVersion =
-    let
-      case = case: out: { inherit case out; };
-    in
-    with lib.versions;
-    lib.switch rocq-core.rocq-version [
-      (case (range "9.0" "9.3") "1.0.4")
-    ] null;
-
-  propagatedBuildInputs = [ mathcomp-boot ];
-
-  meta = {
-    description = "Small library to do epsilon - N reasonning";
-    license = lib.licenses.cecill-b;
-  };
-}
+in
+derivation
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index b5af3ce604ee..97b4a68b3aba 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -171,7 +171,7 @@ let
       mathcomp-analysis = callPackage ../development/rocq-modules/mathcomp-analysis { };
       mathcomp-analysis-stdlib = self.mathcomp-analysis.analysis-stdlib;
       mathcomp-apery = callPackage ../development/coq-modules/mathcomp-apery { };
-      mathcomp-bigenough = callPackage ../development/coq-modules/mathcomp-bigenough { };
+      mathcomp-bigenough = callPackage ../development/rocq-modules/mathcomp-bigenough { };
       mathcomp-classical = self.mathcomp-analysis.classical;
       mathcomp-experimental-reals = self.mathcomp-analysis.experimental-reals;
       mathcomp-finmap = callPackage ../development/coq-modules/mathcomp-finmap { };