X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FTODO;h=e37d7ffffe5739438f29b4dd65cea9935090f620;hb=01001c883a8151edba81cd03a6f254d24a81c867;hp=ed64039cbb36a1199e3d411e8aa1c481805a3c9e;hpb=84762225fd1bbacf9d9ce7d1fe259a4dd17f4351;p=helm.git

diff --git a/helm/software/components/ng_kernel/TODO b/helm/software/components/ng_kernel/TODO
index ed64039cb..e37d7ffff 100644
--- a/helm/software/components/ng_kernel/TODO
+++ b/helm/software/components/ng_kernel/TODO
@@ -3,7 +3,12 @@ in are_convertible togliere il caso Prop,Prop in quanto catturato da ===
 in are_convertible togliere il caso Meta,Meta in quanto catturato da ===
 in are_convertible caso Meta,Meta non fare lift ma accorcia il ctx
 
+taggare le meta con tag::Type e in sort_of_prod verificare che i Pi
+tra meta coinvolgano meta taggate. Il tag potrebbe contenere un bound,
+in modo che si possano taggare anche meta quando si unifica ? ==vs== Type_k
+e la si tagga con bound a seconda del test_eq_only <= k.
 
+?1 <= Type_i -->>  ?1 := ?2,   ?2 : Type_i+1
 
 -------
 ?1 = t