1 files changed, 29 insertions, 0 deletions
diff --git a/debian/patches/test-suite-success-Nsatz.v-comment-out-Ceva.patch b/debian/patches/test-suite-success-Nsatz.v-comment-out-Ceva.patch
new file mode 100644
index 00000000..2cf6af5c
--- /dev/null
+++ b/debian/patches/test-suite-success-Nsatz.v-comment-out-Ceva.patch
@@ -0,0 +1,29 @@
+From: Stephane Glondu <steph@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 file changed, 2 insertions(+)
+
+diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v
+index e38affd..040169e 100644
+--- a/test-suite/success/Nsatz.v
++++ b/test-suite/success/Nsatz.v
+@@ -462,6 +462,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 ->
+@@ -473,6 +474,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 ->