From 7ad020afbda2442cf20972d3faf298b3b9ae0dc2 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

---
 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 5e6eced48824..23f721b6bb00 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".hash = "sha256-nAQAX35W9br7dgrT9FqGyHYSzwgMiMsuD1d7SztQDwY=";
     release."2.1.0".hash = "sha256-UoDxy2BKraDyRsO42GXRo26O74OF51biZQGkIMWLf8Y=";
     release."2.0.3".hash = "sha256-5lDq7IWlEW0EkNzYPu+dA6KOvRgy53W/alikpDr/Kd0=";
@@ -58,7 +60,6 @@ let
     release."1.0.3".hash = "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 5990fde8eb17..4a2b180e370c 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".hash = "sha256-7zfIddRH+Sl4nhEPtS/lMZwRUZI45AVFpcC/UC8Z0Yo=";
     "2.3.0".hash = "sha256-usIcxHOAuN+f/j3WjVbPrjz8Hl9ac8R6kYeAKi3CEts=";
     "2.2.0".hash = "sha256-Cie6paweITwPZy6ej9+qIvHFWknVR382uJPW927t/fo=";