X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita.txt;h=378fa5a4bdcd6f223544b5fc419e8de03c7a8385;hb=94873bb61a663b4fca3dc6d07b7bb9f42122003e;hp=9873b14b2405e37adc14a24c9aa0d6a2974089bd;hpb=a526b1a92a355eaa4309c06ce97986d1e41e7845;p=helm.git

diff --git a/matita/matita.txt b/matita/matita.txt
index 9873b14b2..378fa5a4b 100644
--- a/matita/matita.txt
+++ b/matita/matita.txt
@@ -69,7 +69,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
-  - assiomi (manca sintassi concreta e AST).
   - Dare errore significativo al posto di NotWellTypedInterpreation -> CSC
   - elim_intros_simpl e rewrite_simpl: ora non viene usata dal
                ^^^^^^           ^^^^^^
@@ -145,9 +144,10 @@ TODO
   - non chiudere transitivamente i moo ?? 
 
   DEMONI E ALTRO
-  - compilare Whelp
 
 DONE
+- compilare Whelp -> Gares, Zack, CSC
+- assiomi (manca sintassi concreta e AST) -> CSC
 - in MatitaEngine unificare/rimuovere eval_string, eval_from_stream e
   eval_from_stream_greedy -> CSC
 - menu contestuale (tasto dx) nel sequent viewer -> Zack