diff options
Diffstat (limited to 'debian/patches/5127-fails-on-mips.patch')
| -rw-r--r-- | debian/patches/5127-fails-on-mips.patch | 30 |
1 files changed, 0 insertions, 30 deletions
diff --git a/debian/patches/5127-fails-on-mips.patch b/debian/patches/5127-fails-on-mips.patch deleted file mode 100644 index 949c33a7..00000000 --- a/debian/patches/5127-fails-on-mips.patch +++ /dev/null @@ -1,30 +0,0 @@ -From: Enrico Tassi <gareuselesinge@debian.org> -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. |