diff --git a/pkgs/development/coq-modules/coqeal/default.nix b/pkgs/development/coq-modules/coqeal/default.nix
index 929728ce225b..c00d30ebbabb 100644
--- a/pkgs/development/coq-modules/coqeal/default.nix
+++ b/pkgs/development/coq-modules/coqeal/default.nix
@@ -30,8 +30,9 @@ let
       lib.switch
         [ coq.coq-version mathcomp.version ]
         [
-          (case (range "8.20" "9.1") (isGe "2.3.0") "2.1.1")
-          (case (range "8.20" "9.1") (isGe "2.3.0") "2.1.0")
+          (case (range "9.0" "9.2") (isGe "2.5.0") "2.1.2")
+          (case (range "8.20" "9.1") (range "2.3.0" "2.5.0") "2.1.1")
+          (case (range "8.20" "9.1") (range "2.3.0" "2.5.0") "2.1.0")
           (case (range "8.16" "8.20") (isGe "2.1.0") "2.0.3")
           (case (range "8.16" "8.20") (isGe "2.0.0") "2.0.1")
           (case (range "8.16" "8.17") (isGe "2.0.0") "2.0.0")
@@ -44,6 +45,7 @@ let
         ]
         null;
 
+    release."2.1.2".hash = "sha256-ktoejlxAtbPzWGdW+DXwLSAmxNHDzQTujkY1If4EM8E=";
     release."2.1.1".sha256 = "sha256-nAQAX35W9br7dgrT9FqGyHYSzwgMiMsuD1d7SztQDwY=";
     release."2.1.0".sha256 = "sha256-UoDxy2BKraDyRsO42GXRo26O74OF51biZQGkIMWLf8Y=";
     release."2.0.3".sha256 = "sha256-5lDq7IWlEW0EkNzYPu+dA6KOvRgy53W/alikpDr/Kd0=";
@@ -58,7 +60,6 @@ let
     release."1.0.3".sha256 = "0hc63ny7phzbihy8l7wxjvn3haxx8jfnhi91iw8hkq8n29i23v24";
 
     propagatedBuildInputs = [
-      mathcomp.ssreflect
       mathcomp.algebra
       bignums
       multinomials
@@ -74,10 +75,15 @@ let
       o.propagatedBuildInputs
       ++ lib.optional (lib.versions.isGe "1.1" o.version || o.version == "dev") mathcomp-real-closed;
   });
-  patched-derivation = patched-derivation1.overrideAttrs (o: {
+  patched-derivation2 = patched-derivation1.overrideAttrs (o: {
     propagatedBuildInputs =
       o.propagatedBuildInputs
       ++ lib.optional (lib.versions.isLe "2.0.3" o.version && o.version != "dev") paramcoq;
   });
+  patched-derivation3 = patched-derivation2.overrideAttrs (o: {
+    propagatedBuildInputs =
+      o.propagatedBuildInputs
+      ++ lib.optional (lib.versions.isLe "2.1.1" o.version && o.version != "dev") mathcomp.ssreflect;
+  });
 in
-patched-derivation
+patched-derivation3
diff --git a/pkgs/development/coq-modules/multinomials/default.nix b/pkgs/development/coq-modules/multinomials/default.nix
index 80ee8d4a46d2..c1edb9b8babf 100644
--- a/pkgs/development/coq-modules/multinomials/default.nix
+++ b/pkgs/development/coq-modules/multinomials/default.nix
@@ -33,6 +33,7 @@ mkCoqDerivation {
     lib.switch
       [ coq.coq-version mathcomp.version ]
       [
+        (case (range "9.0" "9.2") (range "2.6.0" "2.6.0") "2.5.0") # also works on MC 2.4 and 2.5 but breaks validsdp
         (case (range "8.18" "9.1") (range "2.1.0" "2.5.0") "2.4.0")
         (case (range "8.17" "9.0") (range "2.1.0" "2.3.0") "2.3.0")
         (case (range "8.17" "8.20") (isGe "2.1.0") "2.2.0")
@@ -49,6 +50,7 @@ mkCoqDerivation {
       ]
       null;
   release = {
+    "2.5.0".hash = "sha256-e1C1NfulQV1Ep2XxNjjcxIoY5FGzndiCuwIy3upwO78=";
     "2.4.0".sha256 = "sha256-7zfIddRH+Sl4nhEPtS/lMZwRUZI45AVFpcC/UC8Z0Yo=";
     "2.3.0".sha256 = "sha256-usIcxHOAuN+f/j3WjVbPrjz8Hl9ac8R6kYeAKi3CEts=";
     "2.2.0".sha256 = "sha256-Cie6paweITwPZy6ej9+qIvHFWknVR382uJPW927t/fo=";