blob: 2cc8e17c01b7eccfa6f362b2d86eec83ca5d56fe (
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
30
31
32
33
34
35
36
37
38
39
40
41
42
43
|
From: Benjamin Barenblat <bbaren@debian.org>
Subject: Remove heavyweight tests
Forwarded: not-needed
Remove tests that use too much RAM or time to run on a buildd. (The MIPS
buildd is frequently the culprit, as MIPS lacks an OCaml native
compiler.)
--- a/test-suite/bugs/closed/5127.v
+++ /dev/null
@@ -1,15 +0,0 @@
-Fixpoint arrow (n: nat) :=
- match n with
- | S n => bool -> arrow n
- | O => bool
- end.
-
-Fixpoint apply (n : nat) : arrow n -> bool :=
- match n return arrow n -> bool with
- | S n => fun f => apply _ (f true)
- | O => fun x => x
- end.
-
-Axiom f : arrow 10000.
-Definition v : bool := Eval compute in apply _ f.
-Definition w : bool := Eval vm_compute in v.
--- 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 ->
|
