From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 30 May 2006 14:56:58 +0000 (+0000)
Subject: matita.txt updated
X-Git-Tag: make_still_working~7275
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9736af82d5c71c085528d02169a35f2ab7c87b64;p=helm.git

matita.txt updated
---

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