TODO
NUCLEO
+ - limit_mul non compila (usare test_library per testare l'intera libreria)
+ (15:06:07) Zack: http://www.cs.unibo.it/cgi-bin/viewcvs.cgi/helm/gTopLevel/testlibrary.ml?rev=1.20&hideattic=0&content-type=text/vnd.viewcvs-markup
- 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
- riattaccare hbugs (brrr...) -> Zack
GUI LOGICA
+ - matitac deve fallire quando matita vuole aggiungere un alias!
+ - default equality e famiglia non e' undo-aware
- nuovo pretty-printer testuale: non stampa usando la notazione
(e.g. guardare output di matitac)
- matitaclean (e famiglia) non cancellano le directory vuote
matitamake /x/y/z/foo/a.ma
- notazione -> Luca e Zack
- non chiudere transitivamente i moo ??
+ - matitaclean all (non troglie i moo?)
DEMONI E ALTRO