[Pkg-ocaml-maint-commits] [SCM] coq packaging branch, experimental/master, updated. debian/8.4_beta+dfsg-2-3-gd136352

[Stephane Glondu]

The following commit has been merged in the experimental/master branch:
commit 5eb084011ecf23993159a2e1e057ecdb7d7aa06f
Author: Stephane Glondu <steph at glondu.net>
Date:   Sun Jan 15 12:36:33 2012 +0100

    Disable a test that uses too much memory

diff --git a/debian/patches/0003-test-suite-success-Nsatz.v-comment-out-Ceva.patch b/debian/patches/0003-test-suite-success-Nsatz.v-comment-out-Ceva.patch
new file mode 100644
index 0000000..6969f7d
--- /dev/null
+++ b/debian/patches/0003-test-suite-success-Nsatz.v-comment-out-Ceva.patch
@@ -0,0 +1,30 @@
+From: Stephane Glondu <steph at glondu.net>
+Date: Sun, 15 Jan 2012 12:34:19 +0100
+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(-)
+
+diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v
+index d316e4a..d783b2a 100644
+--- a/test-suite/success/Nsatz.v
++++ b/test-suite/success/Nsatz.v
+@@ -461,6 +461,7 @@ idtac "chords".
+ (*Finished transaction in 4. secs (3.959398u,0.s)*)
+ Qed.
+ 
++(*
+ Lemma Ceva: forall A B C D E F M:point,
+   collinear M A D -> collinear M B E -> collinear M C F ->
+   collinear B C D -> collinear E A C -> collinear F A B ->
+@@ -472,6 +473,7 @@ idtac "Ceva".
+ Time nsatz.
+ (*Finished transaction in 105. secs (104.121171u,0.474928s)*)
+ Qed.
++*)
+ 
+ Lemma bissectrices: forall A B C M:point,
+   equaltangente C A M M A B ->
+-- 
diff --git a/debian/patches/series b/debian/patches/series
index 4196559..b0df385 100644
--- a/debian/patches/series
+++ b/debian/patches/series
@@ -1,2 +1,3 @@
 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

-- 
coq packaging