...

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

diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index 25980c66f4eee57ffc0c658d69ebce935e6bd7fd..e0ecd399363ac88319d691e122a0de2ba8c67fcd 100644 (file)
--- 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