Things are getting better.

diff --git a/helm/software/components/ng_kernel/TEST b/helm/software/components/ng_kernel/TEST
index 788c6cf82d92358faa130b40cbfc3368f73bca7f..cb61452ccc5ef3e0011d31c480fbd39641fd8978 100644 (file)
--- 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