X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FTODO;h=cfe8ca1171b17457c49593d977fde8e018289717;hb=761aef3c864626e17004b9785c39def7053271e0;hp=5e418e44bfa10110351193bef82a7816a824f60a;hpb=b763e29c46531b2bee8fabd35fa33746f0784d3b;p=helm.git

diff --git a/helm/software/components/ng_kernel/TODO b/helm/software/components/ng_kernel/TODO
index 5e418e44b..cfe8ca117 100644
--- a/helm/software/components/ng_kernel/TODO
+++ b/helm/software/components/ng_kernel/TODO
@@ -10,7 +10,8 @@ e la si tagga con bound a seconda del test_eq_only <= k.
 
 ?1 <= Type_i -->>  ?1 := ?2,   ?2 : Type_i+1
 
-nel vecchio nucleo la height_of di un b-redex fa 0 e quindi riduci in forma normale
+nel vecchio nucleo la height_of di un b-redex fa 0 e quindi riduci in forma
+normale. Spostare la small_delta_step. 
 
 -------
 ?1 = t