From 279dbb3ddc726dc74571bdf67d631891c9cbebf9 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 1 May 2008 10:45:19 +0000 Subject: [PATCH] New bug found. --- helm/software/components/ng_kernel/TEST | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) 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 -- 2.39.2