X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FTEST;h=cefa809139e582b1ca3bdfd3a85e049c0fb82231;hb=68d4a148f1dbd1b22bbc962c99b12835a743ef67;hp=b2dd219c7bb26828d4f8a26ea5730dc933464b83;hpb=e8a373c61ed58f91682b16c753d1926fa647fa7d;p=helm.git diff --git a/helm/software/components/ng_kernel/TEST b/helm/software/components/ng_kernel/TEST index b2dd219c7..cefa80913 100644 --- a/helm/software/components/ng_kernel/TEST +++ b/helm/software/components/ng_kernel/TEST @@ -1,23 +1,25 @@ -CONTENUTO alluris.txt.OK: - -matita tranne freescale e tests -Coq -BellLabs -Cachan -Dyade -Eindhoven -IdealX -Lyon -Marseille -Montevideo -Muenchen -Nancy -Orsay -Paris -Rocq tranne ails, coc, higman, ALGEBRA/CATEGORY_THEORY -Sophia-Antipolis tranne algebra, buchberger, math_groups, float, geometry -Suresnes -Utrecht +CONTENUTO alluris.txt.OK, NEW typing, OLD typing + +matita 11.89 11.71 tranne freescale e tests +Coq fixpoints +BellLabs 0.21 0.22 +Cachan ..... +Dyade fixpoints +Eindhoven 0.23 0.85 +IdealX 0.05 0.06 +Lyon impredicative set +Marseille 1.04 2.23 +Montevideo 1.90 4.29 +Muenchen 0.05 0.07 +Nancy 0.13 0.24 +Orsay fixpoints +Paris 0.39 0.48 +Rocq impredicative set tranne ails, coc, higman, + ALGEBRA/CATEGORY_THEORY +Sophia-Antipolis tranne algebra, buchberger, + math_groups, float, geometry +Suresnes fixpoints +Utrecht 0.82 0.92 ++++++++++++++++