New bug found.

diff --git a/helm/software/components/ng_kernel/TEST b/helm/software/components/ng_kernel/TEST
index cb61452ccc5ef3e0011d31c480fbd39641fd8978..bae9f48d78ae1fe6aa8f3383693001e21f0a771d 100644 (file)
--- 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