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.