summaryrefslogtreecommitdiff
path: root/debian/patches/test-suite-success-Nsatz.v-comment-out-Ceva.patch
diff options
context:
space:
mode:
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.patch29
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 ->