mirror of
https://git.in.rschanz.org/ryan77627/guix.git
synced 2024-12-24 21:38:07 -05:00
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>
This commit is contained in:
parent
11c403ec05
commit
bf1e063be3
3 changed files with 47 additions and 1 deletions
|
@ -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\
|
||||
|
|
|
@ -528,7 +528,9 @@ (define-public coq-autosubst
|
|||
(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
|
||||
|
|
|
@ -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.
|
Loading…
Reference in a new issue