From ff96901dbd04d4f70f3e5ef52b24a8f0c9227529 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= <theo.zimmermann@inria.fr>
Date: Tue, 17 Aug 2021 10:25:41 +0200
Subject: [PATCH] coqPackages.hydra-battles: 0.3 -> 0.4

---
 .../coq-modules/hydra-battles/default.nix     | 24 +++++++++++--------
 1 file changed, 14 insertions(+), 10 deletions(-)

diff --git a/pkgs/development/coq-modules/hydra-battles/default.nix b/pkgs/development/coq-modules/hydra-battles/default.nix
index a74eec4b64fc..6c3c9d88e0cb 100644
--- a/pkgs/development/coq-modules/hydra-battles/default.nix
+++ b/pkgs/development/coq-modules/hydra-battles/default.nix
@@ -1,28 +1,32 @@
-{ lib, mkCoqDerivation, coq, mathcomp, equations, paramcoq, version ? null }:
+{ lib, mkCoqDerivation, coq, equations, version ? null }:
 with lib;
 
 mkCoqDerivation {
   pname = "hydra-battles";
   owner = "coq-community";
 
-  release."0.3".rev    = "v0.3";
-  release."0.3".sha256 = "sha256-rXP/vJqVEg2tN/I9LWV13YQ1+C7M6lzGu3oI+7pSZzg=";
+  release."0.4".sha256 = "sha256:1f7pc4w3kir4c9p0fjx5l77401bx12y72nmqxrqs3qqd3iynvqlp";
+  releaseRev = (v: "v${v}");
 
   inherit version;
   defaultVersion = with versions; switch coq.coq-version [
-    { case = isGe "8.11"; out = "0.3"; }
+    { case = isGe "8.11"; out = "0.4"; }
   ] null;
 
-  propagatedBuildInputs = [ mathcomp equations paramcoq ];
+  propagatedBuildInputs = [ equations ];
+
+  useDune2 = true;
 
   meta = {
-    description = "Variations on Kirby & Paris' hydra battles and other entertaining math in Coq";
+    description = "Exploration of some properties of Kirby and Paris' hydra battles, with the help of Coq";
     longDescription = ''
-       Variations on Kirby & Paris' hydra battles and other
-       entertaining math in Coq (collaborative, documented, includes
-       exercises)
+      An exploration of some properties of Kirby and Paris' hydra
+      battles, with the help of the Coq Proof assistant. This
+      development includes the study of several representations of
+      ordinal numbers, and a part of the so-called Ketonen and Solovay
+      machinery (combinatorial properties of epsilon0).
     '';
-    maintainers = with maintainers; [ siraben ];
+    maintainers = with maintainers; [ siraben Zimmi48 ];
     license = licenses.mit;
     platforms = platforms.unix;
   };