tagging rc-1

[helm.git] / matita / matita.txt

diff --git a/matita/matita.txt b/matita/matita.txt
index 9873b14b2405e37adc14a24c9aa0d6a2974089bd..378fa5a4bdcd6f223544b5fc419e8de03c7a8385 100644 (file)
--- 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