blob: 2cf6af5c92a7fb1e8ff64486d0e773c765e4896c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
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 ->
|
