From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 30 Apr 2008 23:33:38 +0000 (+0000)
Subject: Things are getting better.
X-Git-Tag: make_still_working~5268
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=06992239ba4ce457cfc73be4bbdda991bc20fc56;p=helm.git

Things are getting better.
---

diff --git a/helm/software/components/ng_kernel/TEST b/helm/software/components/ng_kernel/TEST
index 788c6cf82..cb61452cc 100644
--- a/helm/software/components/ng_kernel/TEST
+++ b/helm/software/components/ng_kernel/TEST
@@ -9,6 +9,9 @@ Montevideo
 Muenchen
 Nancy
 Paris
+Rocq/TreeAutomata
+Rocq/tutto tranne ails, coc, higman, ALGEBRA/CATEGORY_THEORY
+Sophia-Antipolis/Bertrand
 Suresnes
 Utrecht
 
@@ -29,10 +32,8 @@ Sophia-Antipolis/Float: vecchio nucleo troppo lento
 Sophia-Antipolis/geometry: vecchio nucleo troppo lento
 
 coq: nuovo nucleo mooooolto lento in guarded by: cic:/Coq/ZArith/Zsqrt/sqrtrempos.con
-orsay: nuovo nucleo
-Rocq/TreeAutomata nuovo nucleo
-Sophia-Antipolis/Bertrand: nuovo nucleo
-Sophia-Antipolis/Buchberger: nuovo nucleo
+orsay: nuovo nucleo diverge (vedi sopra)
+Sophia-Antipolis/Buchberger: nuovo nucleo diverge
 
 Sophia-Antipolis/huffmann: Unknown constant
 Sophia-Antipolis/MATH/GROUPS: Unknown constant
@@ -41,10 +42,10 @@ Sophia-Antipolis/MATH/GROUPS: Unknown constant
 Rocq/ALGEBRA/CATEGORY_THEORY: vecchio nucleo
 Sophia-Antipolis/Algebra: vecchio nucleo variabili
 lyon.ok: vecchio nucleo, variabili
-Altre Rocq: bug vari nuovo nucleo, compresi universi!
 
 lannion: nuovo nucleo impredicative set
 lyon.impredicative_set: nuovo nucleo impredicative set. Altro?
+rocq.higman: impredicative set
 
 ============= IMPREDICATIVE SET ======================
 Lannion/Continuations