From 055d78335d86af40cf1a3553eb11b9678cb5ddc6 Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Mon, 17 Jul 2023 07:48:54 +0200
Subject: [PATCH] =?UTF-8?q?coqPackages.bignums:=208.17.0=20=E2=86=92=209.0?=
 =?UTF-8?q?.0+coq8.17?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 pkgs/development/coq-modules/bignums/default.nix | 14 ++++++++++----
 pkgs/top-level/coq-packages.nix                  | 12 ++++++++++--
 2 files changed, 20 insertions(+), 6 deletions(-)

diff --git a/pkgs/development/coq-modules/bignums/default.nix b/pkgs/development/coq-modules/bignums/default.nix
index c62e20a5a2e..c459ef2ea5c 100644
--- a/pkgs/development/coq-modules/bignums/default.nix
+++ b/pkgs/development/coq-modules/bignums/default.nix
@@ -3,11 +3,17 @@
 mkCoqDerivation {
   pname = "bignums";
   owner = "coq";
-  displayVersion = { bignums = ""; };
   inherit version;
-  defaultVersion = if lib.versions.isGe "8.6" coq.coq-version
-    then "${coq.coq-version}.0" else null;
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
+    { case = range "8.13" "8.17"; out = "9.0.0+coq${coq.coq-version}"; }
+    { case = range "8.6" "8.17"; out = "${coq.coq-version}.0"; }
+  ] null;
 
+  release."9.0.0+coq8.17".sha256 = "sha256-Mn85LqxJKPDIfpxRef9Uh5POwOKlTQ7jsMVz1wnQwuY=";
+  release."9.0.0+coq8.16".sha256 = "sha256-pwFTl4Unr2ZIirAB3HTtfhL2YN7G/Pg88RX9AhKWXbE=";
+  release."9.0.0+coq8.15".sha256 = "sha256-2oGOANn3XULHNIlyqjZ5ppQTQa2QF1zzf3YjHAd/pjo=";
+  release."9.0.0+coq8.14".sha256 = "sha256-qTU152Dz34W6nFZ0pPbja9ouUm/714ZrLQ/Z4N/HIC4=";
+  release."9.0.0+coq8.13".sha256 = "sha256-zvAqV3VAB7cN+nlMhjSXzxuDkdd387ju2VSb2EUthI0=";
   release."8.17.0".sha256 = "sha256-MXYjqN86+3O4hT2ql62U83T5H03E/8ysH8erpvC/oyw=";
   release."8.16.0".sha256 = "sha256-DH3iWwatPlhhCVYVlgL2WLkvneSVzSXUiKo2e0+1zR4=";
   release."8.15.0".sha256 = "093klwlhclgyrba1iv18dyz1qp5f0lwiaa7y0qwvgmai8rll5fns";
@@ -21,7 +27,7 @@ mkCoqDerivation {
   release."8.7.0".sha256  = "11c4sdmpd3l6jjl4v6k213z9fhrmmm1xnly3zmzam1wrrdif4ghl";
   release."8.6.0".rev     = "v8.6.0";
   release."8.6.0".sha256  = "0553pcsy21cyhmns6k9qggzb67az8kl31d0lwlnz08bsqswigzrj";
-  releaseRev = v: "V${v}";
+  releaseRev = v: "${if lib.versions.isGe "9.0" v then "v" else "V"}${v}";
 
   mlPlugin = true;
 
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index e83f18786f1..c3685280430 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -26,7 +26,11 @@ let
       category-theory = callPackage ../development/coq-modules/category-theory { };
       ceres = callPackage ../development/coq-modules/ceres {};
       Cheerios = callPackage ../development/coq-modules/Cheerios {};
-      CoLoR = callPackage ../development/coq-modules/CoLoR {};
+      CoLoR = callPackage ../development/coq-modules/CoLoR (
+        (lib.optionalAttrs (lib.versions.isEq self.coq.coq-version "8.13") {
+          bignums = self.bignums.override { version = "8.13.0"; };
+        })
+      );
       compcert = callPackage ../development/coq-modules/compcert {
         inherit fetchpatch makeWrapper coq2html lib stdenv;
       };
@@ -36,7 +40,11 @@ let
       coq-haskell = callPackage ../development/coq-modules/coq-haskell { };
       coq-lsp = callPackage ../development/coq-modules/coq-lsp {};
       coq-record-update = callPackage ../development/coq-modules/coq-record-update { };
-      coqeal = callPackage ../development/coq-modules/coqeal {};
+      coqeal = callPackage ../development/coq-modules/coqeal (
+        (lib.optionalAttrs (lib.versions.range "8.13" "8.14" self.coq.coq-version) {
+          bignums = self.bignums.override { version = "${self.coq.coq-version}.0"; };
+        })
+      );
       coqhammer = callPackage ../development/coq-modules/coqhammer {};
       coqide = callPackage ../development/coq-modules/coqide {};
       coqprime = callPackage ../development/coq-modules/coqprime {};