Consolidate patches to disable tests that are too big or too slow

Consolidate the several patches that disable tests that time out on
MIPS or use too much RAM/time on the buildds.

1 files changed, 0 insertions, 46 deletions

diff --git a/debian/patches/Remove-test-4429.patch b/debian/patches/Remove-test-4429.patch
deleted file mode 100644
index 9baee306..00000000
--- a/debian/patches/Remove-test-4429.patch
+++ /dev/null
@@ -1,46 +0,0 @@
-From: Enrico Tassi <gareuselesinge@debian.org>
-Date: Thu, 28 Jan 2016 10:11:08 +0100
-Subject: Remove test 4429
-
----
- test-suite/bugs/closed/4429.v | 31 -------------------------------
- 1 file changed, 31 deletions(-)
- delete mode 100644 test-suite/bugs/closed/4429.v
-
-diff --git a/test-suite/bugs/closed/4429.v b/test-suite/bugs/closed/4429.v
-deleted file mode 100644
-index bf0e570..0000000
---- a/test-suite/bugs/closed/4429.v
-+++ /dev/null
-@@ -1,31 +0,0 @@
--Require Import Arith.Compare_dec.
--Require Import Unicode.Utf8.
--
--Fixpoint my_nat_iter (n : nat) {A} (f : A → A) (x : A) : A :=
--  match n with
--    | O    => x
--    | S n' => f (my_nat_iter n' f x)
--  end.
--
--Definition gcd_IT_F (f : nat * nat → nat) (mn : nat * nat) : nat :=
--  match mn with
--    | (0, 0)       => 0
--    | (0, S n')    => S n'
--    | (S m', 0)    => S m'
--    | (S m', S n') =>
--      match le_gt_dec (S m') (S n') with
--        | left  _ => f (S m', S n' - S m')
--        | right _ => f (S m' - S n', S n')
--      end
--  end.
--
--Axiom max_correct_l : ∀ m n : nat, m <= max m n.
--Axiom max_correct_r : ∀ m n : nat, n <= max m n.
--
--Hint Resolve max_correct_l max_correct_r : arith.
--
--Theorem foo : ∀ p p' p'' : nat, p'' < S (max p (max p' p'')).
--Proof.
--  intros.
--  Timeout 3 eauto with arith.
--Qed.