From d105a30b8c597a1a4725a08ffbf96dd1a24c8a2f Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Tue, 31 Mar 2026 16:54:16 +0200
Subject: [PATCH 1/4] coqPackages.aac-tactics: enable for Coq > 9.0

---
 pkgs/development/coq-modules/aac-tactics/default.nix | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pkgs/development/coq-modules/aac-tactics/default.nix b/pkgs/development/coq-modules/aac-tactics/default.nix
index 46e8948abab1..3eef4aefd59c 100644
--- a/pkgs/development/coq-modules/aac-tactics/default.nix
+++ b/pkgs/development/coq-modules/aac-tactics/default.nix
@@ -36,7 +36,7 @@ mkCoqDerivation {
 
     lib.switch coq.coq-version [
       {
-        case = "9.0";
+        case = lib.versions.isGe "9.0";
         out = "9.0.0";
       }
       {

From 2ceb79316e98ddc6ba345e8cf93a00048f578e44 Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Tue, 31 Mar 2026 16:54:26 +0200
Subject: [PATCH 2/4] coqPackages.rewriter: enable for Coq > 9.0

---
 pkgs/development/coq-modules/rewriter/default.nix | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pkgs/development/coq-modules/rewriter/default.nix b/pkgs/development/coq-modules/rewriter/default.nix
index 42cc8f777125..3e3e05cd516e 100644
--- a/pkgs/development/coq-modules/rewriter/default.nix
+++ b/pkgs/development/coq-modules/rewriter/default.nix
@@ -16,7 +16,7 @@ mkCoqDerivation {
     in
     lib.switch coq.coq-version [
       {
-        case = range "8.17" "9.0";
+        case = range "8.17" "9.2";
         out = "0.0.15";
       }
     ] null;

From c041078e3b68bf1c06a33c5c6fa74b11cd91951f Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Tue, 31 Mar 2026 17:06:53 +0200
Subject: [PATCH 3/4] =?UTF-8?q?coqPackages.unicoq:=20enable=20for=20Coq=20?=
 =?UTF-8?q?=E2=89=A5=209.1?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 pkgs/development/coq-modules/unicoq/default.nix | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/pkgs/development/coq-modules/unicoq/default.nix b/pkgs/development/coq-modules/unicoq/default.nix
index 401015b89dec..744a6d24bb4a 100644
--- a/pkgs/development/coq-modules/unicoq/default.nix
+++ b/pkgs/development/coq-modules/unicoq/default.nix
@@ -12,6 +12,10 @@ mkCoqDerivation {
   defaultVersion =
     with lib.versions;
     lib.switch coq.version [
+      {
+        case = isGe "9.1";
+        out = "1.6-9.1";
+      }
       {
         case = range "8.20" "9.0";
         out = "1.6-8.20";
@@ -21,6 +25,8 @@ mkCoqDerivation {
         out = "1.6-8.19";
       }
     ] null;
+  release."1.6-9.1".rev = "0cf37ef7e638bfaad6e804e17bd80e7bb0e1b717";
+  release."1.6-9.1".hash = "sha256-1EKDkj33pg3AsEpckZYqWppPUZV2OkxM2xLq2zvZGMQ=";
   release."1.6-8.20".sha256 = "sha256-zne9LB0lGdqUfrBe8cDK8fwuxfBDFU4PqNlt9nl7rNI=";
   release."1.6-8.19".sha256 = "sha256-fDk60B8AzJwiemxHGgWjNu6PTu6NcJoI9uK7Ww2AT14=";
   releaseRev = v: "v${v}";

From b8d1c0987ec116743c863777dbcd00988a74cf29 Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Tue, 31 Mar 2026 17:07:08 +0200
Subject: [PATCH 4/4] coqPackages.mtac2: enable for Coq 9.1

---
 pkgs/development/coq-modules/mtac2/default.nix | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/pkgs/development/coq-modules/mtac2/default.nix b/pkgs/development/coq-modules/mtac2/default.nix
index ef06e17f2d7f..75ad9aec33a7 100644
--- a/pkgs/development/coq-modules/mtac2/default.nix
+++ b/pkgs/development/coq-modules/mtac2/default.nix
@@ -14,11 +14,16 @@ mkCoqDerivation {
   defaultVersion =
     with lib.versions;
     lib.switch coq.version [
+      {
+        case = isEq "9.1";
+        out = "1.4-rocq${coq.coq-version}";
+      }
       {
         case = range "8.19" "9.0";
         out = "1.4-coq${coq.coq-version}";
       }
     ] null;
+  release."1.4-rocq9.1".hash = "sha256-A+ac84ZfDMW2NhS/NrGIfdairXmzXxZIYGNmJIz0ReM=";
   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=";