From: Claudio Sacerdoti Coen Date: Thu, 24 Apr 2008 17:08:25 +0000 (+0000) Subject: Update... X-Git-Tag: make_still_working~5285 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=36c07ee08f1d0e63719f69f41ee6537f47f2c265;p=helm.git Update... --- diff --git a/helm/software/components/ng_kernel/TEST b/helm/software/components/ng_kernel/TEST index ac35d4e94..caa72bb61 100644 --- a/helm/software/components/ng_kernel/TEST +++ b/helm/software/components/ng_kernel/TEST @@ -1,3 +1,4 @@ +matita BellLabs Cachan Dyade @@ -5,30 +6,39 @@ Eindhoven IdealX Marseille Montevideo +Muenchen Nancy Paris +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 - -Suresnes: nuovo nucleo +[Sophia-Antipolis: calcolo grafi da caricare troppo lento] Rocq/AILS: type-checking vecchio nucleo troppo lento Rocq/COC: type-checking vecchio nucleo troppo lento nijmegen: type-checking vecchio nucleo troppo lento Rocq/TreeAutomata vecchio nucleo troppo lento orsay: type-checking vecchio nucleo troppo lento +Sophia-Antipolis/Bertrand: vecchio nucleo troppo lento +Sophia-Antipolis/Buchberger: vecchio nucleo troppo lento +Sophia-Antipolis/Float: vecchio nucleo troppo lento +Sophia-Antipolis/geometry: vecchio nucleo troppo lento -Rocq/ALGEBRA/CATEGORY_THEORY: vecchio nucleo +Sophia-Antipolis/huffmann: Unknown constant +Sophia-Antipolis/MATH/GROUPS: Unknown constant -Altre Rocq: bug vari nuovo nucleo, compresi universi! -matita: nuovo nucleo universi e altro + +Rocq/ALGEBRA/CATEGORY_THEORY: vecchio nucleo +Sophia-Antipolis/Algebra: vecchio nucleo variabili lyon.ok: vecchio nucleo, variabili -muenchen: nuovo nucleo, guarded by -cachan: nuovo nucleo, guarded by cic:/Coq/Init/Wf/Acc_ind.con +Altre Rocq: bug vari nuovo nucleo, compresi universi! lannion: nuovo nucleo impredicative set lyon.impredicative_set: nuovo nucleo impredicative set. Altro? @@ -191,5 +201,3 @@ but it should have type ∀p: positive. eq positive (Pplus p p) (xO p) → eq positive (Pplus (xI p) (xI p)) (xO (xI p)) - -