Refresh patches

Remove 0002-Remove-test-4366-too-picky-on-the-timeout.patch, since
upstream has increased the timeout.

5 files changed, 4 insertions, 50 deletions

diff --git a/debian/patches/0002-Remove-test-4366-too-picky-on-the-timeout.patch b/debian/patches/0002-Remove-test-4366-too-picky-on-the-timeout.patch
deleted file mode 100644
index e71306ce..00000000
--- a/debian/patches/0002-Remove-test-4366-too-picky-on-the-timeout.patch
+++ /dev/null
@@ -1,30 +0,0 @@
-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.
diff --git a/debian/patches/0003-Remove-test-4429.patch b/debian/patches/0002-Remove-test-4429.patch
index 9baee306..9baee306 100644
--- a/debian/patches/0003-Remove-test-4429.patch
+++ b/debian/patches/0002-Remove-test-4429.patch
diff --git a/debian/patches/0004-Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch b/debian/patches/0003-Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch
index f762e040..45acd396 100644
--- a/debian/patches/0004-Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch
+++ b/debian/patches/0003-Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch
@@ -1,17 +1,6 @@
 From: Enrico Tassi <gareuselesinge@debian.org>
 Date: Wed, 28 Dec 2016 18:18:34 +0100
 Subject: Remove 3441.v and 4811.v due to timeout on small platforms
-
----
- test-suite/bugs/closed/3441.v |   23 -
- test-suite/bugs/closed/4811.v | 1685 -----------------------------------------
- 2 files changed, 1708 deletions(-)
- delete mode 100644 test-suite/bugs/closed/3441.v
- delete mode 100644 test-suite/bugs/closed/4811.v
-
-diff --git a/test-suite/bugs/closed/3441.v b/test-suite/bugs/closed/3441.v
-deleted file mode 100644
-index 50d2978..0000000
 --- a/test-suite/bugs/closed/3441.v
 +++ /dev/null
 @@ -1,23 +0,0 @@
@@ -38,10 +27,6 @@ index 50d2978..0000000
 -     let x := constr:(let n := 17 in do_n n = do_n n) in
 -     let y := (eval lazy in x) in
 -     assert (H := y). (* Finished transaction in 1.19 secs (1.164u,0.024s) (successful) *)
-\ No newline at end of file
-diff --git a/test-suite/bugs/closed/4811.v b/test-suite/bugs/closed/4811.v
-deleted file mode 100644
-index a914962..0000000
 --- a/test-suite/bugs/closed/4811.v
 +++ /dev/null
 @@ -1,1685 +0,0 @@
@@ -49,7 +34,7 @@ index a914962..0000000
 -
 -(* Submitted by Jason Gross *)
 -
--(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "src" "Crypto" "-R" "Bedrock" "Bedrock" "-R" "coqprime-8.5/Coqprime" "Coqprime" "-top" "GF255192") -*- *)
+-(* -*- mode: coq; coq-prog-args: ("-R" "src" "Crypto" "-R" "Bedrock" "Bedrock" "-R" "coqprime-8.5/Coqprime" "Coqprime" "-top" "GF255192") -*- *)
 -(* File reduced by coq-bug-finder from original input, then from 162 lines to 23 lines, then from 245 lines to 95 lines, then from 198 lines to 101 lines, then from 654 lines to 452 lines, then from 591 lines to 505 lines, then from 1770 lines to 580 lines, then from 2238 lines to 1715 lines, then from 1776 lines to 1738 lines, then from 1750 lines to 1679 lines, then from 1693 lines to 1679 lines *)
 -(* coqc version 8.5pl1 (April 2016) compiled on Apr 18 2016 14:48:5 with OCaml 4.02.3
 -   coqtop version 8.5pl1 (April 2016) *)
diff --git a/debian/patches/0005-5127-fails-on-mips.patch b/debian/patches/0004-5127-fails-on-mips.patch
index 949c33a7..949c33a7 100644
--- a/debian/patches/0005-5127-fails-on-mips.patch
+++ b/debian/patches/0004-5127-fails-on-mips.patch
diff --git a/debian/patches/series b/debian/patches/series
index 7285ccd8..aea3a7f2 100644
--- a/debian/patches/series
+++ b/debian/patches/series
@@ -1,5 +1,4 @@
 0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch
-0002-Remove-test-4366-too-picky-on-the-timeout.patch
-0003-Remove-test-4429.patch
-0004-Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch
-0005-5127-fails-on-mips.patch
+0002-Remove-test-4429.patch
+0003-Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch
+0004-5127-fails-on-mips.patch