fix FTBFS on slow architectures by disabling 4429
Enrico Tassi
8 years ago
|
0 |
coq (8.5-2) unstable; urgency=medium
|
|
1 |
|
|
2 |
* patch: disable test 4429 (timeout too strict for slow architectures)
|
|
3 |
|
|
4 |
-- Enrico Tassi <gareuselesinge@debian.org> Thu, 28 Jan 2016 11:47:07 +0100
|
|
5 |
|
| 0 | 6 |
coq (8.5-1) unstable; urgency=medium
|
| 1 | 7 |
|
| 2 | 8 |
* New upstream release
|
|
0 |
From: Enrico Tassi <gareuselesinge@debian.org>
|
|
1 |
Date: Thu, 28 Jan 2016 10:11:08 +0100
|
|
2 |
Subject: Remove test 4429
|
|
3 |
|
|
4 |
---
|
|
5 |
test-suite/bugs/closed/4429.v | 31 -------------------------------
|
|
6 |
1 file changed, 31 deletions(-)
|
|
7 |
delete mode 100644 test-suite/bugs/closed/4429.v
|
|
8 |
|
|
9 |
diff --git a/test-suite/bugs/closed/4429.v b/test-suite/bugs/closed/4429.v
|
|
10 |
deleted file mode 100644
|
|
11 |
index bf0e570..0000000
|
|
12 |
--- a/test-suite/bugs/closed/4429.v
|
|
13 |
+++ /dev/null
|
|
14 |
@@ -1,31 +0,0 @@
|
|
15 |
-Require Import Arith.Compare_dec.
|
|
16 |
-Require Import Unicode.Utf8.
|
|
17 |
-
|
|
18 |
-Fixpoint my_nat_iter (n : nat) {A} (f : A → A) (x : A) : A :=
|
|
19 |
- match n with
|
|
20 |
- | O => x
|
|
21 |
- | S n' => f (my_nat_iter n' f x)
|
|
22 |
- end.
|
|
23 |
-
|
|
24 |
-Definition gcd_IT_F (f : nat * nat → nat) (mn : nat * nat) : nat :=
|
|
25 |
- match mn with
|
|
26 |
- | (0, 0) => 0
|
|
27 |
- | (0, S n') => S n'
|
|
28 |
- | (S m', 0) => S m'
|
|
29 |
- | (S m', S n') =>
|
|
30 |
- match le_gt_dec (S m') (S n') with
|
|
31 |
- | left _ => f (S m', S n' - S m')
|
|
32 |
- | right _ => f (S m' - S n', S n')
|
|
33 |
- end
|
|
34 |
- end.
|
|
35 |
-
|
|
36 |
-Axiom max_correct_l : ∀ m n : nat, m <= max m n.
|
|
37 |
-Axiom max_correct_r : ∀ m n : nat, n <= max m n.
|
|
38 |
-
|
|
39 |
-Hint Resolve max_correct_l max_correct_r : arith.
|
|
40 |
-
|
|
41 |
-Theorem foo : ∀ p p' p'' : nat, p'' < S (max p (max p' p'')).
|
|
42 |
-Proof.
|
|
43 |
- intros.
|
|
44 |
- Timeout 3 eauto with arith.
|
|
45 |
-Qed.
|
| 0 | 0 |
0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch
|
| 1 | 1 |
0002-Remove-test-4366-too-picky-on-the-timeout.patch
|
|
2 |
0003-Remove-test-4429.patch
|