diff --git a/pkgs/development/coq-modules/QuickChick/default.nix b/pkgs/development/coq-modules/QuickChick/default.nix
index a18acb3120e3..bb85278f28cc 100644
--- a/pkgs/development/coq-modules/QuickChick/default.nix
+++ b/pkgs/development/coq-modules/QuickChick/default.nix
@@ -2,7 +2,7 @@
   lib,
   mkCoqDerivation,
   coq,
-  ssreflect,
+  mathcomp-boot,
   ExtLib,
   simple-io,
   version ? null,
@@ -17,7 +17,7 @@ in
   inherit version;
   defaultVersion =
     lib.switch
-      [ coq.coq-version ssreflect.version ]
+      [ coq.coq-version mathcomp-boot.version ]
       [
         {
           cases = [
@@ -127,7 +127,7 @@ in
   mlPlugin = true;
   nativeBuildInputs = lib.optional recent coq.ocamlPackages.ocamlbuild;
   propagatedBuildInputs =
-    [ ssreflect ]
+    [ mathcomp-boot ]
     ++ lib.optionals recent [
       ExtLib
       simple-io
diff --git a/pkgs/development/coq-modules/autosubst/default.nix b/pkgs/development/coq-modules/autosubst/default.nix
index 037ccdebe7f8..440eadea3bff 100644
--- a/pkgs/development/coq-modules/autosubst/default.nix
+++ b/pkgs/development/coq-modules/autosubst/default.nix
@@ -2,7 +2,7 @@
   lib,
   mkCoqDerivation,
   coq,
-  mathcomp-ssreflect,
+  mathcomp-boot,
   stdlib,
   version ? null,
 }:
@@ -35,7 +35,7 @@ mkCoqDerivation {
     ] null;
 
   propagatedBuildInputs = [
-    mathcomp-ssreflect
+    mathcomp-boot
     stdlib
   ];
 
diff --git a/pkgs/development/coq-modules/coquelicot/default.nix b/pkgs/development/coq-modules/coquelicot/default.nix
index fa6687c73a54..8832ddcec24c 100644
--- a/pkgs/development/coq-modules/coquelicot/default.nix
+++ b/pkgs/development/coq-modules/coquelicot/default.nix
@@ -4,7 +4,7 @@
   autoconf,
   coq,
   stdlib,
-  ssreflect,
+  mathcomp-boot,
   version ? null,
 }:
 
@@ -59,7 +59,7 @@ mkCoqDerivation {
   nativeBuildInputs = [ autoconf ];
   propagatedBuildInputs = [
     stdlib
-    ssreflect
+    mathcomp-boot
   ];
   useMelquiondRemake.logpath = "Coquelicot";
 
diff --git a/pkgs/development/coq-modules/extructures/default.nix b/pkgs/development/coq-modules/extructures/default.nix
index aca5a9ad8dc1..270c6146fe3e 100644
--- a/pkgs/development/coq-modules/extructures/default.nix
+++ b/pkgs/development/coq-modules/extructures/default.nix
@@ -3,7 +3,7 @@
   mkCoqDerivation,
   coq,
   version ? null,
-  ssreflect,
+  mathcomp-boot,
   deriving,
 }:
 
@@ -15,7 +15,7 @@
   defaultVersion =
     with lib.versions;
     lib.switch
-      [ coq.coq-version ssreflect.version ]
+      [ coq.coq-version mathcomp-boot.version ]
       [
         {
           cases = [
@@ -63,7 +63,7 @@
   release."0.3.0".sha256 = "sha256:14rm0726f1732ldds495qavg26gsn30w6dfdn36xb12g5kzavp38";
   release."0.2.2".sha256 = "sha256:1clzza73gccy6p6l95n6gs0adkqd3h4wgl4qg5l0qm4q140grvm7";
 
-  propagatedBuildInputs = [ ssreflect ];
+  propagatedBuildInputs = [ mathcomp-boot ];
 
   meta = with lib; {
     description = "Finite data structures with extensional reasoning";
diff --git a/pkgs/development/coq-modules/fourcolor/default.nix b/pkgs/development/coq-modules/fourcolor/default.nix
index 39f6b75135eb..3768db213bd8 100644
--- a/pkgs/development/coq-modules/fourcolor/default.nix
+++ b/pkgs/development/coq-modules/fourcolor/default.nix
@@ -64,9 +64,9 @@ mkCoqDerivation {
       null;
 
   propagatedBuildInputs = [
-    mathcomp.algebra
-    mathcomp.ssreflect
+    mathcomp.boot
     mathcomp.fingroup
+    mathcomp.algebra
   ];
 
   meta = with lib; {
diff --git a/pkgs/development/coq-modules/gaia/default.nix b/pkgs/development/coq-modules/gaia/default.nix
index 6110407c94e7..c10aab6198d8 100644
--- a/pkgs/development/coq-modules/gaia/default.nix
+++ b/pkgs/development/coq-modules/gaia/default.nix
@@ -50,9 +50,9 @@ mkCoqDerivation {
       null;
 
   propagatedBuildInputs = [
-    mathcomp.ssreflect
-    mathcomp.algebra
+    mathcomp.boot
     mathcomp.fingroup
+    mathcomp.algebra
     stdlib
   ];
 
diff --git a/pkgs/development/coq-modules/interval/default.nix b/pkgs/development/coq-modules/interval/default.nix
index 2317d04a398b..eacc9e91774d 100644
--- a/pkgs/development/coq-modules/interval/default.nix
+++ b/pkgs/development/coq-modules/interval/default.nix
@@ -5,7 +5,7 @@
   coq,
   coquelicot,
   flocq,
-  mathcomp-ssreflect,
+  mathcomp-boot,
   mathcomp-fingroup,
   bignums ? null,
   gnuplot_qt,
@@ -82,7 +82,7 @@ mkCoqDerivation rec {
     ++ [
       coquelicot
       flocq
-      mathcomp-ssreflect
+      mathcomp-boot
       mathcomp-fingroup
     ]
     ++ lib.optionals (lib.versions.isGe "4.2.0" defaultVersion) [ gnuplot_qt ];
diff --git a/pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix b/pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix
index 212d1cb03568..3ea3a67f390b 100644
--- a/pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix
@@ -2,6 +2,7 @@
   lib,
   mkCoqDerivation,
   coq,
+  mathcomp-ssreflect,
   mathcomp-algebra,
   coq-elpi,
   mathcomp-zify,
@@ -60,6 +61,7 @@ mkCoqDerivation {
   release."1.2.4".sha256 = "sha256-BRxt0LGPz2u3kJRjcderaZqCfs8M8qKAAwNSWmIck7Q=";
 
   propagatedBuildInputs = [
+    mathcomp-ssreflect
     mathcomp-algebra
     coq-elpi
     mathcomp-zify
diff --git a/pkgs/development/coq-modules/mathcomp-bigenough/default.nix b/pkgs/development/coq-modules/mathcomp-bigenough/default.nix
index 86516fd9082d..45399fa5ce63 100644
--- a/pkgs/development/coq-modules/mathcomp-bigenough/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-bigenough/default.nix
@@ -1,7 +1,7 @@
 {
   coq,
   mkCoqDerivation,
-  mathcomp,
+  mathcomp-boot,
   lib,
   version ? null,
 }:
@@ -34,7 +34,7 @@ mkCoqDerivation {
       }
     ] null;
 
-  propagatedBuildInputs = [ mathcomp.ssreflect ];
+  propagatedBuildInputs = [ mathcomp-boot ];
 
   meta = {
     description = "Small library to do epsilon - N reasonning";
diff --git a/pkgs/development/coq-modules/mathcomp-finmap/default.nix b/pkgs/development/coq-modules/mathcomp-finmap/default.nix
index fe408966797b..8e3245c619a1 100644
--- a/pkgs/development/coq-modules/mathcomp-finmap/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-finmap/default.nix
@@ -1,7 +1,7 @@
 {
   coq,
   mkCoqDerivation,
-  mathcomp,
+  mathcomp-boot,
   lib,
   version ? null,
 }:
@@ -18,7 +18,7 @@ mkCoqDerivation {
   defaultVersion =
     with lib.versions;
     lib.switch
-      [ coq.version mathcomp.version ]
+      [ coq.version mathcomp-boot.version ]
       [
         {
           cases = [
@@ -107,7 +107,7 @@ mkCoqDerivation {
     "1.0.0".sha256 = "0sah7k9qm8sw17cgd02f0x84hki8vj8kdz7h15i7rmz08rj0whpa";
   };
 
-  propagatedBuildInputs = [ mathcomp.ssreflect ];
+  propagatedBuildInputs = [ mathcomp-boot ];
 
   meta = {
     description = "Finset and finmap library";
diff --git a/pkgs/development/coq-modules/mathcomp-zify/default.nix b/pkgs/development/coq-modules/mathcomp-zify/default.nix
index ffad0bc8b0b8..3a6dd0c1b97d 100644
--- a/pkgs/development/coq-modules/mathcomp-zify/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-zify/default.nix
@@ -2,9 +2,9 @@
   lib,
   mkCoqDerivation,
   coq,
-  mathcomp-algebra,
-  mathcomp-ssreflect,
+  mathcomp-boot,
   mathcomp-fingroup,
+  mathcomp-algebra,
   stdlib,
   version ? null,
 }:
@@ -54,8 +54,8 @@ mkCoqDerivation {
   release."1.5.0+2.0+8.16".sha256 = "sha256-boBYGvXdGFc6aPnjgSZYSoW4kmN5khtNrSV3DUv9DqM=";
 
   propagatedBuildInputs = [
+    mathcomp-boot
     mathcomp-algebra
-    mathcomp-ssreflect
     mathcomp-fingroup
     stdlib
   ];
diff --git a/pkgs/development/coq-modules/multinomials/default.nix b/pkgs/development/coq-modules/multinomials/default.nix
index e20117d8393a..1817d4011199 100644
--- a/pkgs/development/coq-modules/multinomials/default.nix
+++ b/pkgs/development/coq-modules/multinomials/default.nix
@@ -138,7 +138,7 @@ mkCoqDerivation {
   '';
 
   propagatedBuildInputs = [
-    mathcomp.ssreflect
+    mathcomp.boot
     mathcomp.algebra
     mathcomp-finmap
     mathcomp.fingroup
diff --git a/pkgs/development/coq-modules/odd-order/default.nix b/pkgs/development/coq-modules/odd-order/default.nix
index 1e4e044ae558..26688b4cba6c 100644
--- a/pkgs/development/coq-modules/odd-order/default.nix
+++ b/pkgs/development/coq-modules/odd-order/default.nix
@@ -39,7 +39,7 @@ mkCoqDerivation {
 
   propagatedBuildInputs = [
     mathcomp.character
-    mathcomp.ssreflect
+    mathcomp.boot
     mathcomp.fingroup
     mathcomp.algebra
     mathcomp.solvable
diff --git a/pkgs/development/coq-modules/relation-algebra/default.nix b/pkgs/development/coq-modules/relation-algebra/default.nix
index 571360d9926f..40ffbb30c7d9 100644
--- a/pkgs/development/coq-modules/relation-algebra/default.nix
+++ b/pkgs/development/coq-modules/relation-algebra/default.nix
@@ -3,7 +3,7 @@
   mkCoqDerivation,
   coq,
   aac-tactics,
-  mathcomp,
+  mathcomp-boot,
   version ? null,
 }:
 
@@ -79,7 +79,7 @@ mkCoqDerivation {
 
   propagatedBuildInputs = [
     aac-tactics
-    mathcomp.ssreflect
+    mathcomp-boot
   ];
 
   meta = with lib; {
diff --git a/pkgs/development/coq-modules/ssprove/default.nix b/pkgs/development/coq-modules/ssprove/default.nix
index ca181478fedb..c3db4a8be0e5 100644
--- a/pkgs/development/coq-modules/ssprove/default.nix
+++ b/pkgs/development/coq-modules/ssprove/default.nix
@@ -4,7 +4,7 @@
   coq,
   version ? null,
   equations,
-  mathcomp-ssreflect,
+  mathcomp-boot,
   mathcomp-analysis,
   mathcomp-experimental-reals,
   extructures,
@@ -19,7 +19,7 @@
   defaultVersion =
     with lib.versions;
     lib.switch
-      [ coq.coq-version mathcomp-ssreflect.version ]
+      [ coq.coq-version mathcomp-boot.version ]
       [
         {
           cases = [
@@ -62,7 +62,7 @@
 
   propagatedBuildInputs = [
     equations
-    mathcomp-ssreflect
+    mathcomp-boot
     mathcomp-analysis
     mathcomp-experimental-reals
     extructures