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 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. e='grep'>log msg
path: root/gnu/packages/ada.scm
AgeCommit message (Expand)Author
2023-02-16gnu: Remove unneeded module imports....* gnu/packages/abiword.scm, * gnu/packages/ada.scm, * gnu/packages/agda.scm, * gnu/packages/backup.scm, * gnu/packages/barrier.scm, * gnu/packages/bioinformatics.scm, * gnu/packages/bootstrap.scm, * gnu/packages/bqn.scm, * gnu/packages/c.scm, * gnu/packages/chemistry.scm, * gnu/packages/coq.scm, * gnu/packages/cross-base.scm, * gnu/packages/databases.scm, * gnu/packages/emacs-xyz.scm, * gnu/packages/enlightenment.scm, * gnu/packages/games.scm, * gnu/packages/geo.scm, * gnu/packages/ghostscript.scm, * gnu/packages/gl.scm, * gnu/packages/golang.scm, * gnu/packages/jami.scm, * gnu/packages/java-maths.scm, * gnu/packages/kde-frameworks.scm, * gnu/packages/kde-plasma.scm, * gnu/packages/language.scm, * gnu/packages/libreoffice.scm, * gnu/packages/linphone.scm, * gnu/packages/lisp.scm, * gnu/packages/llvm.scm, * gnu/packages/machine-learning.scm, * gnu/packages/minetest.scm, * gnu/packages/monitoring.scm, * gnu/packages/nfs.scm, * gnu/packages/ocr.scm, * gnu/packages/opencl.scm, * gnu/packages/pdf.scm, * gnu/packages/python-xyz.scm, * gnu/packages/racket.scm, * gnu/packages/rust.scm, * gnu/packages/syncthing.scm, * gnu/packages/syndication.scm, * gnu/packages/telegram.scm, * gnu/packages/vulkan.scm, * gnu/packages/web-browsers.scm, * gnu/packages/web.scm, * gnu/packages/webkit.scm: Remove some unecessary module imports. Efraim Flashner