...

diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index d1f44f3e651103c14bf7ecd9a3efb9d431679602..914de2d4f2de297b8ee971ea872d1e0d1f93dffa 100644 (file)
--- a/helm/matita/matita.txt
+++ b/helm/matita/matita.txt
@@ -27,11 +27,8 @@ TODO
   script visibile nella finestra dello script
 - Dare errore significativo al posto di NotWellTypedInterpreation
 - Implementare menu edit: find/replace/cut/copy/undo/etc.
-- Bug vari nella generazione dei principi di eliminazione:
+- Bug nella generazione dei principi di eliminazione:
    1. generazione nomi (usa ref incrementata localmente)
-   2. prodotti dipendenti come non-dipendenti (visibili eseguendo passo
-      passo il test inversion.ma)
-   3. usato trucco outtype non dipendenti per il case
 - elim_intros_simpl e rewrite_simpl: ora non viene usata dal
              ^^^^^^           ^^^^^^
   toplevel la variante che semplifica. Capire quali sono i problemi
@@ -71,6 +68,10 @@ TODO
   diversi/e
 
 DONE
+- Bug vari nella generazione dei principi di eliminazione:
+   2. prodotti dipendenti come non-dipendenti (visibili eseguendo passo
+      passo il test inversion.ma)
+   3. usato trucco outtype non dipendenti per il case
 - controllo per script modificato o meno prima di uscire  -> Gares
 - LApply deve prendere in input gli identificatori che va a generare;
   lascio a Ferruccio la scelta della sintassi concreta    -> Ferruccio