From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 12 Sep 2005 10:26:36 +0000 (+0000)
Subject: ...
X-Git-Tag: V_0_1_2_1~45
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ccb64f7d77f64e17668e286b60cd2b6631a2e57f;p=helm.git

...
---

diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index 25980c66f..e0ecd3993 100644
--- a/helm/matita/matita.txt
+++ b/helm/matita/matita.txt
@@ -17,8 +17,6 @@ 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 O. ==> BOOM! unificazione di una testa flessibile con
-    True.
   - assiomi (manca sintassi concreta e AST).
   - Guardare il commento
     (*CSC: this code is suspect and/or bugged: we try first without reduction
@@ -121,6 +119,8 @@ TODO
   DEMONI E ALTRO
 
 DONE
+- theorem t: True. elim O. ==> BOOM! unificazione di una testa flessibile con
+  True -> Gares
 - parsing contestuale (tattiche replace, change e forse altre)
   capire dove fare la select per avere i contesti in cui disambiguare gli
   altri argomenti. -> Zack, Enrico, CSC