...

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

diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index 478cd77ab9eb5f3e064fcc9e086b9cb3b1fcc204..d71a5f510dce1deedd0684eaec42708509013c20 100644 (file)
--- 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