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.
3a0e785d'/><select name='qt'>
<option value='grep'>log msg</option>
<option value='author'>author</option>
<option value='committer'>committer</option>
<option value='range'>range</option>
</select>
<input class='txt' type='search' size='10' name='q' value=''/>
<input type='submit' value='search'/>
</form>
</td></tr></table>
<div class='path'>path: <a href='/guix/log/?id=318581c5fc8f7716ad65d670eb7654a03a0e785d'>root</a>/<a href='/guix/log/gnu?id=318581c5fc8f7716ad65d670eb7654a03a0e785d'>gnu</a>/<a href='/guix/log/gnu/build?id=318581c5fc8f7716ad65d670eb7654a03a0e785d'>build</a>/<a href='/guix/log/gnu/build/linux-initrd.scm?id=318581c5fc8f7716ad65d670eb7654a03a0e785d'>linux-initrd.scm</a></div><div class='content'><table class='list nowrap'><tr class='nohover'><th class='left'>Age</th><th class='left'>Commit message (<a href='/guix/log/gnu/build/linux-initrd.scm?id=318581c5fc8f7716ad65d670eb7654a03a0e785d&amp;showmsg=1'>Expand</a>)</th><th class='left'>Author</th></tr>
<tr><td><span title='2020-12-15 17:32:10 +0100'>2020-12-15</span></td><td><a href='/guix/commit/gnu/build/linux-initrd.scm?id=6a060ff27ff68384d7c90076baa36c349fff689d'>store-copy: 'populate-store' can optionally deduplicate files.</a><span class='msg-avail'>...<span class='msg-tooltip'>Until now deduplication was performed as an additional pass after
copying files, which involve re-traversing all the files that had just
been copied.

* guix/store/deduplication.scm (copy-file/deduplicate): New procedure.
* tests/store-deduplication.scm ("copy-file/deduplicate"): New test.
* guix/build/store-copy.scm (populate-store): Add #:deduplicate?
parameter and honor it.
* tests/gexp.scm ("gexp-&gt;derivation, store copy"): Pass #:deduplicate? #f
to 'populate-store'.
* gnu/build/image.scm (initialize-root-partition): Pass #:deduplicate?
to 'populate-store'.  Pass #:deduplicate? #f to 'register-closure'.
* gnu/build/vm.scm (root-partition-initializer): Likewise.
* gnu/build/install.scm (populate-single-profile-directory): Pass
 #:deduplicate? #f to 'populate-store'.
* gnu/build/linux-initrd.scm (build-initrd): Likewise.
* guix/scripts/pack.scm (self-contained-tarball)[import-module?]: New
procedure.
[build]: Pass it as an argument to 'source-module-closure'.
* guix/scripts/pack.scm (squashfs-image)[build]: Wrap in
'with-extensions'.
* gnu/system/linux-initrd.scm (expression-&gt;initrd)[import-module?]: New
procedure.
[builder]: Pass it to 'source-module-closure'.
* gnu/system/install.scm (cow-store-service-type)[import-module?]: New
procedure.  Pass it to 'source-module-closure'.
</span></span></td><td>Ludovic Courtès</td></tr>
<tr><td><span title='2020-11-21 12:39:14 +0100'>2020-11-21</span></td><td><a href='/guix/commit/gnu/build/linux-initrd.scm?id=2200bb214690ebc78b9fa42887ac9dfb8035bd4f'>linux-initrd: Remove unnecessary timestamp reset phase.</a><span class='msg-avail'>...<span class='msg-tooltip'>* gnu/build/linux-initrd.scm (write-cpio-archive): Mention timestamps in
docstring.
(build-initrd): Remove unnecessary timestamp reset phase.
</span></span></td><td>Ludovic Courtès</td></tr>