From 496dd0c2b103fc533c38a94fa7d43ba13fb86a35 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 7 May 2008 22:43:37 +0000 Subject: [PATCH] Update after some more bug fixing. --- helm/software/components/ng_kernel/TEST | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/helm/software/components/ng_kernel/TEST b/helm/software/components/ng_kernel/TEST index d56939cca..b2dd219c7 100644 --- a/helm/software/components/ng_kernel/TEST +++ b/helm/software/components/ng_kernel/TEST @@ -1,6 +1,7 @@ CONTENUTO alluris.txt.OK: matita tranne freescale e tests +Coq BellLabs Cachan Dyade @@ -11,6 +12,7 @@ Marseille Montevideo Muenchen Nancy +Orsay Paris Rocq tranne ails, coc, higman, ALGEBRA/CATEGORY_THEORY Sophia-Antipolis tranne algebra, buchberger, math_groups, float, geometry @@ -33,12 +35,11 @@ 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 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 rocq.higman: nuovo nucleo impredicative set -- 2.39.2