Refresh patches

4 files changed, 2 insertions, 58 deletions

diff --git a/debian/patches/0001-Add-distclean-back-to-test-suite-Makefile.patch b/debian/patches/0001-Add-distclean-back-to-test-suite-Makefile.patch
deleted file mode 100644
index 80cd27ae..00000000
--- a/debian/patches/0001-Add-distclean-back-to-test-suite-Makefile.patch
+++ /dev/null
@@ -1,23 +0,0 @@
-From: Stephane Glondu <steph@glondu.net>
-Date: Thu, 12 Jan 2012 16:30:10 +0100
-Subject: Add distclean back to test-suite/Makefile
-
----
- test-suite/Makefile |    3 +++
- 1 files changed, 3 insertions(+), 0 deletions(-)
-
-diff --git a/test-suite/Makefile b/test-suite/Makefile
-index cd5886f..f3013c0 100644
---- a/test-suite/Makefile
-+++ b/test-suite/Makefile
-@@ -97,6 +97,9 @@ clean:
- 	  -name '*.stamp' -o -name '*.vo' -o -name '*.log' \
- 	\) -print0 | xargs -0 rm -f
- 
-+distclean: clean
-+	$(HIDE)find . -name '*.log' -print0 | xargs -0 rm -f
-+
- #######################################################################
- # Per-subsystem targets
- #######################################################################
--- 
diff --git a/debian/patches/0003-test-suite-success-Nsatz.v-comment-out-Ceva.patch b/debian/patches/0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch
index 6969f7dd..722ab00c 100644
--- a/debian/patches/0003-test-suite-success-Nsatz.v-comment-out-Ceva.patch
+++ b/debian/patches/0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch
@@ -5,7 +5,7 @@ Subject: test-suite/success/Nsatz.v: comment out Ceva
 This lemma uses too much memory for many buildds...
 ---
  test-suite/success/Nsatz.v |    2 ++
- 1 files changed, 2 insertions(+), 0 deletions(-)
+ 1 file changed, 2 insertions(+)
 
 diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v
 index d316e4a..d783b2a 100644
diff --git a/debian/patches/0002-coq_micromega.ml-fix-order-of-recursive-calls-to-rco.patch b/debian/patches/0002-coq_micromega.ml-fix-order-of-recursive-calls-to-rco.patch
deleted file mode 100644
index 3307023d..00000000
--- a/debian/patches/0002-coq_micromega.ml-fix-order-of-recursive-calls-to-rco.patch
+++ /dev/null
@@ -1,31 +0,0 @@
-From: Stephane Glondu <steph@glondu.net>
-Date: Sat, 14 Jan 2012 01:24:30 +0100
-Subject: coq_micromega.ml: fix order of recursive calls to rconstant
-
-Some tests were failing on architectures without native code because
-the evaluation order of arguments in a function call is not the same
-on bytecode, leading to different behaviours for the psatzl tactic.
----
- plugins/micromega/coq_micromega.ml |    8 ++++++--
- 1 files changed, 6 insertions(+), 2 deletions(-)
-
-diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
-index 1ad49bb..543ab1b 100644
---- a/plugins/micromega/coq_micromega.ml
-+++ b/plugins/micromega/coq_micromega.ml
-@@ -991,8 +991,12 @@ struct
-         else raise ParseError
-     | App(op,args) -> 
- 	begin
--	  try 
--	    (assoc_const   op rconst_assoc) (rconstant args.(0)) (rconstant args.(1))
-+	  try
-+            (* the evaluation order is important in the following *)
-+            let f = assoc_const op rconst_assoc in
-+            let a = rconstant args.(0) in
-+            let b = rconstant args.(1) in
-+            f a b
- 	  with
- 	      ParseError -> 
- 		match op with
--- 
diff --git a/debian/patches/series b/debian/patches/series
index b0df385f..53d51a16 100644
--- a/debian/patches/series
+++ b/debian/patches/series
@@ -1,3 +1 @@
-0001-Add-distclean-back-to-test-suite-Makefile.patch
-0002-coq_micromega.ml-fix-order-of-recursive-calls-to-rco.patch
-0003-test-suite-success-Nsatz.v-comment-out-Ceva.patch
+0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch