blob: 949c33a707b678feaa9cdab055edf03dc3cf3de9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
|
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.
|
