From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 8 Sep 2005 17:13:46 +0000 (+0000)
Subject: ...
X-Git-Tag: V_0_1_2_1~54
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=69eb85b72b44b0af8d626fd97324ece59b91077d;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