From b76c352cb71152231ec5a60b7e307299f201dc8d Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi <pi8027@gmail.com>
Date: Thu, 14 Nov 2024 14:13:29 +0100
Subject: [PATCH] coqPackages.lemma-overloading: init at 8.12

---
 .../coq-modules/lemma-overloading/default.nix | 32 +++++++++++++++++++
 pkgs/top-level/coq-packages.nix               |  1 +
 2 files changed, 33 insertions(+)
 create mode 100644 pkgs/development/coq-modules/lemma-overloading/default.nix

diff --git a/pkgs/development/coq-modules/lemma-overloading/default.nix b/pkgs/development/coq-modules/lemma-overloading/default.nix
new file mode 100644
index 000000000000..8f4f12b02ba4
--- /dev/null
+++ b/pkgs/development/coq-modules/lemma-overloading/default.nix
@@ -0,0 +1,32 @@
+{ lib, mkCoqDerivation, coq, mathcomp-ssreflect, version ? null }:
+
+mkCoqDerivation rec {
+  pname = "lemma-overloading";
+  inherit version;
+
+  defaultVersion = with lib.versions;
+     lib.switch [ coq.coq-version mathcomp-ssreflect.version ] [
+       { cases = [ (range "8.10" "8.12") (range "1.7" "1.11") ]; out = "8.12.0"; }
+       { cases = [ (range "8.10" "8.11") (range "1.7" "1.11") ]; out = "8.11.0"; }
+       { cases = [ (range "8.8" "8.11") (range "1.7" "1.10") ]; out = "8.10.0"; }
+       { cases = [ (range "8.8" "8.9") (range "1.7" "1.8") ]; out = "8.9.0"; }
+       { cases = [ (isEq "8.8") (range "1.6.2" "1.7") ]; out = "8.8.0"; }
+     ] null;
+
+  release = {
+    "8.12.0".sha256 = "sha256-ul1IhxFwhLTy3+rmo3gvjHI3Z8A8avN0Rzq0YDy2bjs=";
+    "8.11.0".sha256 = "sha256-RI3KdSEYxUbjfZWKO7atGdEqDU8WmLJSFeF6TLlgUFc=";
+    "8.10.0".sha256 = "sha256-qpHh/iz2fFtGwUedjJ6fuOh8uq1mlL4ETxc9zDJ6800=";
+    "8.9.0".sha256 = "sha256-dE9O94DvcF93TUTU7ky9pvGZgTtPZWz6826b6Js/nHc=";
+    "8.8.0".sha256 = "sha256-Iq3KfESMnZF8hhGKuvZHx+hAMEaoCP7MhhQEI6xfoO8=";
+  };
+  releaseRev = v: "v${v}";
+
+  propagatedBuildInputs = [ mathcomp-ssreflect ];
+
+  meta = with lib; {
+    description = "Libraries demonstrating design patterns for programming and proving with canonical structures in Coq";
+    maintainers = with lib.maintainers; [ cohencyril ];
+    license = licenses.gpl3Plus;
+  };
+}
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index dbee4637a848..e757116796ab 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -87,6 +87,7 @@ let
       ITree = callPackage ../development/coq-modules/ITree { };
       itree-io = callPackage ../development/coq-modules/itree-io { };
       json = callPackage ../development/coq-modules/json {};
+      lemma-overloading = callPackage ../development/coq-modules/lemma-overloading {};
       LibHyps = callPackage ../development/coq-modules/LibHyps {};
       ltac2 = callPackage ../development/coq-modules/ltac2 {};
       math-classes = callPackage ../development/coq-modules/math-classes { };