...

[helm.git] / helm / matita / matita.txt

diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index 81b104c3f0f41e396aec08e49e4379ca0bbbf9ef..05ba96189693abd468877a9f060d81b251517ece 100644 (file)
--- 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