blob: e71306ce0079f79f99bacdc382ee9f9d898faf2d (
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: Tue, 26 Jan 2016 16:58:25 +0100
Subject: Remove test 4366 (too picky on the timeout)
---
test-suite/bugs/closed/4366.v | 15 ---------------
1 file changed, 15 deletions(-)
delete mode 100644 test-suite/bugs/closed/4366.v
diff --git a/test-suite/bugs/closed/4366.v b/test-suite/bugs/closed/4366.v
deleted file mode 100644
index 6a5e9a4..0000000
--- a/test-suite/bugs/closed/4366.v
+++ /dev/null
@@ -1,15 +0,0 @@
-Fixpoint stupid (n : nat) : unit :=
-match n with
-| 0 => tt
-| S n =>
- let () := stupid n in
- let () := stupid n in
- tt
-end.
-
-Goal True.
-Proof.
-pose (v := stupid 24).
-Timeout 2 vm_compute in v.
-exact I.
-Qed.
|
