From 6d120ab859c59b3d8796e7efad28fce110d47a41 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= <theo.zimmermann@telecom-paris.fr>
Date: Fri, 30 Jan 2026 15:34:29 +0100
Subject: [PATCH] coqPackages_9_0.mtac2: init at 1.4-coq9.0

---
 pkgs/development/coq-modules/mtac2/default.nix | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/pkgs/development/coq-modules/mtac2/default.nix b/pkgs/development/coq-modules/mtac2/default.nix
index d7fd6f4a36d8..ef06e17f2d7f 100644
--- a/pkgs/development/coq-modules/mtac2/default.nix
+++ b/pkgs/development/coq-modules/mtac2/default.nix
@@ -2,6 +2,7 @@
   lib,
   mkCoqDerivation,
   coq,
+  stdlib,
   unicoq,
   version ? null,
 }:
@@ -14,14 +15,19 @@ mkCoqDerivation {
     with lib.versions;
     lib.switch coq.version [
       {
-        case = range "8.19" "8.19";
+        case = range "8.19" "9.0";
         out = "1.4-coq${coq.coq-version}";
       }
     ] null;
+  release."1.4-coq9.0".sha256 = "sha256-pAPBRCW7M46UZPJ+v/0xAT8mpQURN8czMmlrfYz/MVU=";
+  release."1.4-coq8.20".sha256 = "sha256-3nu/8zDvdnl6WzGtw46mVcdqgkRgc6Xy8/I+lUOrSIY=";
   release."1.4-coq8.19".sha256 = "sha256-G9eK0eLyECdT20/yf8yyz7M8Xq2WnHHaHpxVGP0yTtU=";
   releaseRev = v: "v${v}";
   mlPlugin = true;
-  propagatedBuildInputs = [ unicoq ];
+  propagatedBuildInputs = [
+    stdlib
+    unicoq
+  ];
   meta = {
     description = "Typed tactic language for Coq";
     license = lib.licenses.mit;