From: Claudio Sacerdoti Coen Date: Thu, 1 May 2008 10:45:19 +0000 (+0000) Subject: New bug found. X-Git-Tag: make_still_working~5267 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=279dbb3ddc726dc74571bdf67d631891c9cbebf9;p=helm.git New bug found. --- diff --git a/helm/software/components/ng_kernel/TEST b/helm/software/components/ng_kernel/TEST index cb61452cc..bae9f48d7 100644 --- a/helm/software/components/ng_kernel/TEST +++ b/helm/software/components/ng_kernel/TEST @@ -38,14 +38,15 @@ Sophia-Antipolis/Buchberger: nuovo nucleo diverge Sophia-Antipolis/huffmann: Unknown constant Sophia-Antipolis/MATH/GROUPS: Unknown constant +lyon: Appl con meno di due argomenti, cic:/Lyon/COINDUCTIVES/STREAMS/Alter/eqalters_body.con Rocq/ALGEBRA/CATEGORY_THEORY: vecchio nucleo Sophia-Antipolis/Algebra: vecchio nucleo variabili lyon.ok: vecchio nucleo, variabili lannion: nuovo nucleo impredicative set -lyon.impredicative_set: nuovo nucleo impredicative set. Altro? -rocq.higman: impredicative set +rocq.higman: nuovo nucleo impredicative set +lyon.impredicative_set: nuovo nucleo impredicative set ============= IMPREDICATIVE SET ====================== Lannion/Continuations