From bf1e063be350c611022c1430f3a7f1f42005de7f Mon Sep 17 00:00:00 2001
From: Jean-Pierre De Jesus DIAZ <jean@foundation.xyz>
Date: Mon, 17 Jun 2024 14:25:35 +0200
Subject: [PATCH] gnu: coq-autosubst: Fix Coq 8.19 compatibility.

* gnu/packages/patches/coq-autosubst-1.8-remove-deprecated-files.patch:
New patch.
* gnu/local.mk (dist_patch_DATA): Register patch.
* gnu/packages/coq.scm (coq-autosubst)<source>: Use Coq 8.19
compatibility patch.

Change-Id: Ib705c92b5605c6b679224f471ff12c018842c006
Signed-off-by: Andreas Enge <andreas@enge.fr>
---
 gnu/local.mk                                  |  1 +
 gnu/packages/coq.scm                          |  4 +-
 ...utosubst-1.8-remove-deprecated-files.patch | 43 +++++++++++++++++++
 3 files changed, 47 insertions(+), 1 deletion(-)
 create mode 100644 gnu/packages/patches/coq-autosubst-1.8-remove-deprecated-files.patch

diff --git a/gnu/local.mk b/gnu/local.mk
index f9a6c3fa22..f96807616f 100644
--- a/gnu/local.mk
+++ b/gnu/local.mk
@@ -1081,6 +1081,7 @@ dist_patch_DATA =						\
   %D%/packages/patches/converseen-hide-updates-checks.patch	\
   %D%/packages/patches/converseen-hide-non-free-pointers.patch	\
   %D%/packages/patches/cool-retro-term-wctype.patch		\
+  %D%/packages/patches/coq-autosubst-1.8-remove-deprecated-files.patch		\
   %D%/packages/patches/coreutils-gnulib-tests.patch		\
   %D%/packages/patches/cppcheck-disable-char-signedness-test.patch	\
   %D%/packages/patches/cppdap-add-CPPDAP_USE_EXTERNAL_GTEST_PACKAGE.patch\
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index f0c09bdef9..7a8a49208a 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -528,7 +528,9 @@ Coq proof assistant.")
                     (commit (string-append "v" version))))
               (file-name (git-file-name name version))
               (sha256
-               (base32 "0qk72r6cqxwhqqkl2kmryhw365w3l2016qii1q1sk3md7zq46jcz"))))
+               (base32 "0qk72r6cqxwhqqkl2kmryhw365w3l2016qii1q1sk3md7zq46jcz"))
+              (patches
+               (search-patches "coq-autosubst-1.8-remove-deprecated-files.patch"))))
     (build-system gnu-build-system)
     (arguments
      `(#:tests? #f
diff --git a/gnu/packages/patches/coq-autosubst-1.8-remove-deprecated-files.patch b/gnu/packages/patches/coq-autosubst-1.8-remove-deprecated-files.patch
new file mode 100644
index 0000000000..cc76672798
--- /dev/null
+++ b/gnu/packages/patches/coq-autosubst-1.8-remove-deprecated-files.patch
@@ -0,0 +1,43 @@
+This patch compatibility problems with Coq 8.19.
+
+It was taken from the master branch of coq-autosubst as there is only
+this change since version 1.8 of autosubst and they haven't released a
+newer version yet.
+
+To recreate this patch:
+
+wget https://github.com/coq-community/autosubst/commit/97eea491813b691c6187d53d92ae6020874a82a3.patch \
+     -O coq-autosubst-1.8-remove-deprecated-files.patch
+
+From 97eea491813b691c6187d53d92ae6020874a82a3 Mon Sep 17 00:00:00 2001
+From: Pierre Rousselin <rousselin@math.univ-paris13.fr>
+Date: Sun, 15 Oct 2023 14:34:31 +0200
+Subject: [PATCH] Remove deprecated files in Coq.Arith
+
+This is necessary for Coq/Coq:#18164
+---
+ theories/Autosubst_Basics.v | 4 ++--
+ 1 file changed, 2 insertions(+), 2 deletions(-)
+
+diff --git a/theories/Autosubst_Basics.v b/theories/Autosubst_Basics.v
+index 477c87c..1940c3b 100644
+--- a/theories/Autosubst_Basics.v
++++ b/theories/Autosubst_Basics.v
+@@ -5,7 +5,7 @@
+ *)
+ 
+ Require Import Coq.Program.Tactics.
+-Require Import Coq.Arith.Plus List FunctionalExtensionality.
++Require Import Coq.Arith.PeanoNat List FunctionalExtensionality.
+ 
+ (** Annotate "a" with additional information. *)
+ Definition annot {A B} (a : A) (b : B) : A := a.
+@@ -240,7 +240,7 @@ Lemma plusSn n m : S n + m = S (n + m). reflexivity. Qed.
+ Lemma plusnS n m : n + S m = S (n + m). symmetry. apply plus_n_Sm. Qed.
+ Lemma plusOn n : O + n = n. reflexivity. Qed.
+ Lemma plusnO n : n + O = n. symmetry. apply plus_n_O. Qed.
+-Lemma plusA n m k : n + (m + k) = (n + m) + k. apply plus_assoc. Qed.
++Lemma plusA n m k : n + (m + k) = (n + m) + k. apply Nat.add_assoc. Qed.
+ 
+ Lemma scons_eta f n : f n .: (+S n) >>> f = (+n) >>> f.
+ Proof.