From 8c09d8af35c34798270b484f2dfe6098be2eb0a2 Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:46:58 -0500 Subject: Refresh patches Remove 0002-Remove-test-4366-too-picky-on-the-timeout.patch, since upstream has increased the timeout. --- debian/patches/0003-Remove-test-4429.patch | 46 ------------------------------ 1 file changed, 46 deletions(-) delete mode 100644 debian/patches/0003-Remove-test-4429.patch (limited to 'debian/patches/0003-Remove-test-4429.patch') diff --git a/debian/patches/0003-Remove-test-4429.patch b/debian/patches/0003-Remove-test-4429.patch deleted file mode 100644 index 9baee306..00000000 --- a/debian/patches/0003-Remove-test-4429.patch +++ /dev/null @@ -1,46 +0,0 @@ -From: Enrico Tassi -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. -- cgit v1.2.3