From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 2 Oct 2008 11:20:43 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~4712
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=b763e29c46531b2bee8fabd35fa33746f0784d3b;p=helm.git

...
---

diff --git a/helm/software/components/ng_kernel/TODO b/helm/software/components/ng_kernel/TODO
index e37d7ffff..5e418e44b 100644
--- a/helm/software/components/ng_kernel/TODO
+++ b/helm/software/components/ng_kernel/TODO
@@ -10,6 +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
+
 -------
 ?1 = t
   (?1,?2)::(?2,t)::subst