diff options
Diffstat (limited to 'debian/patches/0003-Remove-test-4429.patch')
| -rw-r--r-- | debian/patches/0003-Remove-test-4429.patch | 46 |
1 files changed, 46 insertions, 0 deletions
diff --git a/debian/patches/0003-Remove-test-4429.patch b/debian/patches/0003-Remove-test-4429.patch new file mode 100644 index 00000000..9baee306 --- /dev/null +++ b/debian/patches/0003-Remove-test-4429.patch @@ -0,0 +1,46 @@ +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. |