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

diff --git a/helm/software/matita/matita.txt b/helm/software/matita/matita.txt
index 9873b14b2..378fa5a4b 100644
--- a/helm/software/matita/matita.txt
+++ b/helm/software/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