X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FTEST;h=3479aed5bd9e386dee0b2e0f902fa7bf9e92488f;hb=57e708bca8555d6146c4e3d07c0a9b6a546373ce;hp=bf33415d3b1a5408f665e63d22c480e745fc45ac;hpb=f4d71b463ae8510e80a40cf4df475d19fab3df2c;p=helm.git

diff --git a/helm/software/components/ng_kernel/TEST b/helm/software/components/ng_kernel/TEST
index bf33415d3..3479aed5b 100644
--- a/helm/software/components/ng_kernel/TEST
+++ b/helm/software/components/ng_kernel/TEST
@@ -43,10 +43,11 @@ Sophia-Antipolis/Float: vecchio nucleo troppo lento
 Sophia-Antipolis/geometry: vecchio nucleo troppo lento
 Rocq/ALGEBRA/CATEGORY_THEORY: vecchio nucleo troppo lento
 
-Sophia-Antipolis/Algebra: nuovo nucleo diverge
-   cic:/Sophia-Antipolis/Algebra/Sub_module/submodule_op.con
-Sophia-Antipolis/Buchberger: nuovo nucleo diverge
-   cic:/Sophia-Antipolis/Buchberger/BuchRed/redbuch_stable.con
+## = diventato addirittura velocissimo dopo universi + proof irrelevance + altezze
+##Sophia-Antipolis/Algebra: nuovo nucleo diverge
+##   cic:/Sophia-Antipolis/Algebra/Sub_module/submodule_op.con
+##Sophia-Antipolis/Buchberger: nuovo nucleo diverge
+##   cic:/Sophia-Antipolis/Buchberger/BuchRed/redbuch_stable.con
 matita/freescale: nuovo nucleo molto piu' lento del vecchio?
 
 lannion: nuovo nucleo impredicative set