diff --git a/pkgs/development/coq-modules/mathcomp-analysis/default.nix b/pkgs/development/coq-modules/mathcomp-analysis/default.nix
index be83ed4778a9..0df390b8a9ee 100644
--- a/pkgs/development/coq-modules/mathcomp-analysis/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-analysis/default.nix
@@ -4,7 +4,6 @@
   mathcomp,
   mathcomp-finmap,
   mathcomp-bigenough,
-  mathcomp-real-closed,
   hierarchy-builder,
   stdlib,
   single ? false,
@@ -105,7 +104,6 @@ let
       analysis-deps = [
         mathcomp.field
         mathcomp-bigenough
-        mathcomp-real-closed
       ];
       intra-deps = lib.optionals (package != "single") (map mathcomp_ packages.${package});
       pkgpath = lib.switch package [
diff --git a/pkgs/development/rocq-modules/mathcomp-analysis/default.nix b/pkgs/development/rocq-modules/mathcomp-analysis/default.nix
index 1a77e673e4f7..c40340feeb35 100644
--- a/pkgs/development/rocq-modules/mathcomp-analysis/default.nix
+++ b/pkgs/development/rocq-modules/mathcomp-analysis/default.nix
@@ -4,6 +4,7 @@
   mathcomp,
   mathcomp-finmap,
   mathcomp-bigenough,
+  mathcomp-real-closed,
   stdlib,
   single ? false,
   rocq-core,
@@ -58,6 +59,7 @@ let
       analysis-deps = [
         mathcomp.field
         mathcomp-bigenough
+        mathcomp-real-closed
       ];
       intra-deps = lib.optionals (package != "single") (map mathcomp_ packages.${package});
       pkgpath =