diff options
Diffstat (limited to 'debian/patches/test-suite-success-Nsatz.v-comment-out-Ceva.patch')
-rw-r--r-- | debian/patches/test-suite-success-Nsatz.v-comment-out-Ceva.patch | 29 |
1 files changed, 0 insertions, 29 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 deleted file mode 100644 index 2cf6af5c..00000000 --- a/debian/patches/test-suite-success-Nsatz.v-comment-out-Ceva.patch +++ /dev/null @@ -1,29 +0,0 @@ -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 -> |