From: Claudio Sacerdoti Coen Date: Tue, 30 May 2006 14:56:58 +0000 (+0000) Subject: matita.txt updated X-Git-Tag: 0.4.95@7852~1378 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bc6b3da5f91648b34c55478b3db71a485894ebdf;p=helm.git matita.txt updated --- 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