From d025df3435b18e6c405ccfa5173da76b137d57b1 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Wed, 22 Jul 2026 16:14:30 +0200
Subject: [PATCH] coqPackages.multinomials: 2.4.0 -> 2.5.0

(cherry picked from commit 7ad020afbda2442cf20972d3faf298b3b9ae0dc2)
---
 pkgs/development/coq-modules/coqeal/default.nix  | 16 +++++++++++-----
 .../coq-modules/multinomials/default.nix         |  2 ++
 2 files changed, 13 insertions(+), 5 deletions(-)

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=";