+- 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
+ genera i_rec e i_rect quando c'e' un argomento ricorsivo
+- parsing contestuale (tattiche replace, change e forse altre)
+- assiomi
+- Guardare il commento
+ (*CSC: this code is suspect and/or bugged: we try first without reduction
+ and then using whd. However, the saturate_term always tries with full
+ reduction without delta. *)
+ in primitiveTactics.ml. Potrebbe essere causa di rallentamento della apply
+ oltre che di bug!
+- Bug di cut&paste: se si fa cut&paste di testo lockato si ottiene testo
+ lockato!
+- keybinding globali: CTRL-{su,giu,...} devono fungere anche quando altre
+ finestre hanno il focus (e.g. cicBrowser). C'e' gia' da qualche parte il
+ codice che aggiunge i keybinding a tutte le eventBox, e' da ripristinare
+- quando si sposta il punto di esecuzione dello script cambiare la parte di
+ script visibile nella finestra dello script
+- Dare errore significativo al posto di NotWellTypedInterpreation