From 06992239ba4ce457cfc73be4bbdda991bc20fc56 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 30 Apr 2008 23:33:38 +0000 Subject: [PATCH] Things are getting better. --- 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 788c6cf82..cb61452cc 100644 --- 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 -- 2.39.2