X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2Fmatita.txt;h=d71a5f510dce1deedd0684eaec42708509013c20;hb=3a12950125e7a4a792546aacea40505f3cecae89;hp=478cd77ab9eb5f3e064fcc9e086b9cb3b1fcc204;hpb=4545d7dd07b44b0a755d516bef082b6a1a83ec24;p=helm.git

diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index 478cd77ab..d71a5f510 100644
--- a/helm/matita/matita.txt
+++ b/helm/matita/matita.txt
@@ -17,7 +17,7 @@ TODO
   - tattiche e fallimenti: una tattica che non progredisce dovrebbe fallire
   - comportamento di tutte le tattiche nei confronti dei let-in
   - elim con pattern
-  - theorem t: True. elim x. ==> BOOM! unificazione di una testa flessibile con
+  - theorem t: True. elim O. ==> BOOM! unificazione di una testa flessibile con
     True.
   - assiomi (manca sintassi concreta e AST).
   - Guardare il commento
@@ -128,8 +128,8 @@ DONE
   NOTA: questo bug e' legato a quello di parsing in presenza di tattiche
   con pattern, visto che in tal caso e' l'intero parsing a dover essere
   fatto in un contesto differente. Risolvendo quel bug si risolve
-  -> Zack, Enrico, CSC
   automaticamente anche questo.
+  -> Zack, Enrico, CSC
 - Usare il cicbrowser per fare "Whelp instance": lui riscrive la barra
   con la notazione alla Coq V7.0 che non riesce piu' a riparsare! -> Zack
 - implementare inclusione file di configurazione (perche' ora tutti