From b38be3a054228c22fbe82cc87bc72504b2b42571 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 3 May 2008 14:52:17 +0000 Subject: [PATCH] Broken XML files either fixed or removed. --- helm/software/components/ng_kernel/TEST | 20 ++++++-------------- 1 file changed, 6 insertions(+), 14 deletions(-) diff --git a/helm/software/components/ng_kernel/TEST b/helm/software/components/ng_kernel/TEST index e4810633e..933460b8d 100644 --- a/helm/software/components/ng_kernel/TEST +++ b/helm/software/components/ng_kernel/TEST @@ -1,6 +1,6 @@ CONTENUTO alluris.txt.OK: -matita +matita tranne freescale e tests BellLabs Cachan Dyade @@ -13,17 +13,12 @@ Muenchen Nancy Paris Rocq tranne ails, coc, higman, ALGEBRA/CATEGORY_THEORY -Sophia-Antipolis tranne algebra, buchberger, huffmann, math_groups, - float, geometry +Sophia-Antipolis tranne algebra, buchberger, math_groups, float, geometry Suresnes Utrecht ++++++++++++++++ -contrib di matita? - -++++++++++++++++ - [CoRN: calcolo grafi da caricare troppo lento] [Coq: calcolo grafi da caricare troppo lento] [Sophia-Antipolis: calcolo grafi da caricare troppo lento] @@ -35,14 +30,15 @@ nijmegen: type-checking vecchio nucleo troppo lento Sophia-Antipolis/Float: vecchio nucleo troppo lento Sophia-Antipolis/geometry: vecchio nucleo troppo lento +matita/tests: nuovo nucleo problema con universi!!! + 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 +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 @@ -60,10 +56,6 @@ Rocq/Paradoxes: Hurkens e Russell Rocq/HistoricalExamples Rocq/HigmanNW -============= BUG VECCHIO NUCLEO ======================= -Problema con permutazione ens? -cic:/Rocq/ALGEBRA/CATEGORY_THEORY/ADJUNCTION/Adj_FunFreeMon/Adj_FunFreeMon_FunForget.con - ============= CONVERSIONE FIX GENERATIVI ================ cic:/Coq/IntMap/Lsort/alist_nth_ad_semantics.con Appl: wrong application of le_S_n: the parameter H1 has type -- 2.39.2