From 6786da162521427921379f05d064c7e47fc2a825 Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Tue, 5 Feb 2019 10:39:11 -0500 Subject: Stop numbering patches MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Keeping patches sequentially numbered produces a messy Git history with many renames for compaction. It’s also redundant with the series file. --- debian/patches/5127-fails-on-mips.patch | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) create mode 100644 debian/patches/5127-fails-on-mips.patch (limited to 'debian/patches/5127-fails-on-mips.patch') diff --git a/debian/patches/5127-fails-on-mips.patch b/debian/patches/5127-fails-on-mips.patch new file mode 100644 index 00000000..949c33a7 --- /dev/null +++ b/debian/patches/5127-fails-on-mips.patch @@ -0,0 +1,30 @@ +From: Enrico Tassi +Date: Thu, 29 Dec 2016 08:56:45 +0100 +Subject: 5127 fails on mips + +--- + test-suite/bugs/closed/5127.v | 15 --------------- + 1 file changed, 15 deletions(-) + delete mode 100644 test-suite/bugs/closed/5127.v + +diff --git a/test-suite/bugs/closed/5127.v b/test-suite/bugs/closed/5127.v +deleted file mode 100644 +index 831e8fb..0000000 +--- a/test-suite/bugs/closed/5127.v ++++ /dev/null +@@ -1,15 +0,0 @@ +-Fixpoint arrow (n: nat) := +- match n with +- | S n => bool -> arrow n +- | O => bool +- end. +- +-Fixpoint apply (n : nat) : arrow n -> bool := +- match n return arrow n -> bool with +- | S n => fun f => apply _ (f true) +- | O => fun x => x +- end. +- +-Axiom f : arrow 10000. +-Definition v : bool := Eval compute in apply _ f. +-Definition w : bool := Eval vm_compute in v. -- cgit v1.2.3