diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-01-26 17:18:24 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-01-26 17:18:24 +0100 |
commit | ad20f9ab9a6f4d9e080b27571fa411aa68a53907 (patch) | |
tree | 182f2c6cb72c2d450149c0a4f82463a2a6179663 /debian/patches/0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch | |
parent | bb08c29807439697fa7c2045000dd3e17a9428b1 (diff) |
8.5
Diffstat (limited to 'debian/patches/0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch')
-rw-r--r-- | debian/patches/0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/debian/patches/0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch b/debian/patches/0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch index 198188e7..2cf6af5c 100644 --- a/debian/patches/0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch +++ b/debian/patches/0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch @@ -8,10 +8,10 @@ This lemma uses too much memory for many buildds... 1 file changed, 2 insertions(+) diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v -index d316e4a..d783b2a 100644 +index e38affd..040169e 100644 --- a/test-suite/success/Nsatz.v +++ b/test-suite/success/Nsatz.v -@@ -461,6 +461,7 @@ idtac "chords". +@@ -462,6 +462,7 @@ idtac "chords". (*Finished transaction in 4. secs (3.959398u,0.s)*) Qed. @@ -19,7 +19,7 @@ index d316e4a..d783b2a 100644 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". +@@ -473,6 +474,7 @@ idtac "Ceva". Time nsatz. (*Finished transaction in 105. secs (104.121171u,0.474928s)*) Qed. @@ -27,4 +27,3 @@ index d316e4a..d783b2a 100644 Lemma bissectrices: forall A B C M:point, equaltangente C A M M A B -> --- |