-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
-
-Sophia-Antipolis/huffmann: Unknown constant
-Sophia-Antipolis/MATH/GROUPS: Unknown constant
-
-lyon: Appl con meno di due argomenti, cic:/Lyon/COINDUCTIVES/STREAMS/Alter/eqalters_III.con
-
-Rocq/ALGEBRA/CATEGORY_THEORY: vecchio nucleo
-Sophia-Antipolis/Algebra: vecchio nucleo variabili
-lyon.ok: vecchio nucleo, variabili
+## = 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?