]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_kernel/TODO
- Bug fixed: removed URIs were not removed from the dependencies DB.
[helm.git] / helm / software / components / ng_kernel / TODO
index 5e418e44bfa10110351193bef82a7816a824f60a..02913a155a14729973b80b7c9c56606a349f3723 100644 (file)
@@ -10,8 +10,11 @@ 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. 
 
+
+@ tra universi senza duplicati
 -------
 ?1 = t
   (?1,?2)::(?2,t)::subst