From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 11 Jul 2005 14:30:47 +0000 (+0000)
Subject: ...
X-Git-Tag: pre_notation~40
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5d6f84f769b7634ae990e0ad5d21c59bc3a9eccf;p=helm.git

...
---

diff --git a/helm/matita/.cvsignore b/helm/matita/.cvsignore
index cb1984a8b..94c16e2d2 100644
--- a/helm/matita/.cvsignore
+++ b/helm/matita/.cvsignore
@@ -33,3 +33,4 @@ matitaclean
 matitaclean.opt
 *.o
 *.swp
+matita.conf.xml
diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index 81b104c3f..05ba96189 100644
--- a/helm/matita/matita.txt
+++ b/helm/matita/matita.txt
@@ -2,6 +2,11 @@
 (**********************************************************************)
 
 TODO
+- matitaclean all dovrebbe radere al suolo la directory .matita
+- tornare indietro in matita dovrebbe essere O(1) e non un Undo passo passo
+- invertibilita' dell'inserimento automatico di alias: quando si torna
+  su bisognerebbe tornare su di un passo e non fare undo degli alias
+- theorem t: True. elim x. ==> BOOM!
 - PREOCCUPANTE: per 
   inductive i : Prop := K : True (*-> i*) -> i.
   noi generiamo i_rec e i_rect con e senza il commento qui sopra; Coq NON