matitadep now parses notation.

[helm.git] / helm / matita / matita.txt

diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index dd89c7ea4bdf6ad0f9ecd09093b2c67757ea5486..13d946afc9ace54727459dcaba5041767a921492 100644 (file)
--- a/helm/matita/matita.txt
+++ b/helm/matita/matita.txt
@@ -89,9 +89,6 @@ TODO
   - riattaccare hbugs (brrr...) -> Zack
 
   GUI LOGICA
-  - tutte gli script che parsano (e.g. matitaclean, matitadep) debbono
-    processare la notazione per evitare errori di parsing (visibili ora
-    che e' stata committata la contrib list)!
   - la funzione alias_diff e' lentissima (anche se CSC l'ha accellerata di
     un fattore 3x) e puo' essere evitata: chi vuole aggiungere alias (la
     disambiguazione, il comando "alias" e l'add_obj) deve indicare
@@ -120,6 +117,9 @@ TODO
   DEMONI E ALTRO
 
 DONE
+- tutte gli script che parsano (e.g. matitaclean, matitadep) debbono
+  processare la notazione per evitare errori di parsing (visibili ora
+  che e' stata committata la contrib list)! -> Gares
 - E' possibile fare "Build" senza selezionare nulla, ottenendo un
   assert false -> Gares
 - disambiguazione: attualmente io (CSC) ho committato la versione di