From 06c60deb62c2f7d967e68c98b6c81cbcdbcb534d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 18 May 2008 21:29:29 +0000 Subject: [PATCH] ... --- helm/software/components/ng_kernel/TEST | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/helm/software/components/ng_kernel/TEST b/helm/software/components/ng_kernel/TEST index fc1e2323f..bf33415d3 100644 --- a/helm/software/components/ng_kernel/TEST +++ b/helm/software/components/ng_kernel/TEST @@ -1,6 +1,6 @@ CONTENUTO alluris.txt.OK, NEW typing, OLD typing -matita 11.89 11.71 tranne freescale e tests +matita 11.89 11.71 tranne freescale Coq fixpoints BellLabs 0.21 0.22 Cachan ..... @@ -23,6 +23,9 @@ Utrecht 0.82 0.92 ++++++++++++++++ +TODO: Andrea mi ha cassato la parte sulla reentrance; secondo me quella e' +importante + ATTENZIONE: cosa succede con un PTS non full? Un (Prod : Type) non lo tipiamo, ma tipiamo (Lambda : Type)! @@ -40,8 +43,6 @@ Sophia-Antipolis/Float: vecchio nucleo troppo lento Sophia-Antipolis/geometry: vecchio nucleo troppo lento Rocq/ALGEBRA/CATEGORY_THEORY: vecchio nucleo troppo lento -matita/tests: nuovo nucleo problema con universi!!! - Sophia-Antipolis/Algebra: nuovo nucleo diverge cic:/Sophia-Antipolis/Algebra/Sub_module/submodule_op.con Sophia-Antipolis/Buchberger: nuovo nucleo diverge -- 2.39.2