X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FTEST;h=6f3d571a1c8468d4069443146dd6b8fb909f3186;hb=d344d41028275b6d1451dca8e40a88e33e588389;hp=933460b8d976b6774eff10da64a4feb43ed3e11e;hpb=b38be3a054228c22fbe82cc87bc72504b2b42571;p=helm.git

diff --git a/helm/software/components/ng_kernel/TEST b/helm/software/components/ng_kernel/TEST
index 933460b8d..6f3d571a1 100644
--- a/helm/software/components/ng_kernel/TEST
+++ b/helm/software/components/ng_kernel/TEST
@@ -29,18 +29,18 @@ Rocq/COC: type-checking vecchio nucleo troppo lento
 nijmegen: type-checking vecchio nucleo troppo lento
 Sophia-Antipolis/Float: vecchio nucleo troppo lento
 Sophia-Antipolis/geometry: vecchio nucleo troppo lento
+Rocq/ALGEBRA/CATEGORY_THEORY: vecchio nucleo troppo lento
 
 matita/tests: nuovo nucleo problema con universi!!!
 
+cic:/Rocq/ALGEBRA/CATEGORY_THEORY/LIMITS/FunForget_UA/UA_FM.con: 15.17s vs 0.14s vecchio nucleo!
 coq: nuovo nucleo mooooolto lento in guarded by: cic:/Coq/ZArith/Zsqrt/sqrtrempos.con
 orsay: nuovo nucleo diverge (vedi sopra)
 Sophia-Antipolis/Buchberger: nuovo nucleo diverge
 matita/freescale: nuovo nucleo diverge
 
-Rocq/ALGEBRA/CATEGORY_THEORY: vecchio nucleo: ???
-  cic:/Rocq/ALGEBRA/CATEGORY_THEORY/ADJUNCTION/Adj_FunFreeMon/Adj_FunFreeMon_FunForget.con
-Sophia-Antipolis/Algebra: vecchio nucleo variabili
-lyon/PROCESSES: vecchio nucleo, variabili
+Sophia-Antipolis/Algebra: nuovo nucleo?
+lyon/PROCESSES: nuovo nucleo?
 
 lannion: nuovo nucleo impredicative set
 rocq.higman: nuovo nucleo impredicative set