Bug fixed in handling of explicit named substitutions: it could happen that

[helm.git] / helm / software / components / ng_kernel / TEST

diff --git a/helm/software/components/ng_kernel/TEST b/helm/software/components/ng_kernel/TEST
index 933460b8d976b6774eff10da64a4feb43ed3e11e..6f3d571a1c8468d4069443146dd6b8fb909f3186 100644 (file)
--- a/helm/software/components/ng_kernel/TEST
+++ b/helm/software/components/ng_kernel/TEST
@@ -29,18 +29,18 @@ Rocq/COC: type-checking vecchio nucleo troppo lento
 nijmegen: type-checking vecchio nucleo troppo lento
 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!!!
 
+cic:/Rocq/ALGEBRA/CATEGORY_THEORY/LIMITS/FunForget_UA/UA_FM.con: 15.17s vs 0.14s vecchio nucleo!
 coq: nuovo nucleo mooooolto lento in guarded by: cic:/Coq/ZArith/Zsqrt/sqrtrempos.con
 orsay: nuovo nucleo diverge (vedi sopra)
 Sophia-Antipolis/Buchberger: nuovo nucleo diverge
 matita/freescale: nuovo nucleo diverge
 
-Rocq/ALGEBRA/CATEGORY_THEORY: vecchio nucleo: ???
-  cic:/Rocq/ALGEBRA/CATEGORY_THEORY/ADJUNCTION/Adj_FunFreeMon/Adj_FunFreeMon_FunForget.con
-Sophia-Antipolis/Algebra: vecchio nucleo variabili
-lyon/PROCESSES: vecchio nucleo, variabili
+Sophia-Antipolis/Algebra: nuovo nucleo?
+lyon/PROCESSES: nuovo nucleo?
 
 lannion: nuovo nucleo impredicative set
 rocq.higman: nuovo nucleo impredicative set