TATTICHE
+ - generazione di principi di co-induzione per co-induttivi
+ - ARGOMENTI IMPLICIT: li vogliamo? come? come disabilitarli localmente?
- in generale: invece di spiegare gli errori nel momento in cui si sollevano
le eccezioni, farlo quando vengono presentate all'utente. Motivo: il calcolo
del messaggio di errore puo' essere estremamente costoso (e' gia' successo!)
- riattaccare hbugs (brrr...) -> Zack
GUI LOGICA
+ - generazione di dipendenze verso .moo di Coq (non esistenti!)
- proposta di Zack: NON calcolare (ed esportare) per default gli inner-types;
aggiungere un'opzione per questo a matitac (riduce drasticamente il tempo
di qed)
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
DONE
+- matitaclean all (non troglie i moo?) -> Gares
- matitaclean (e famiglia) non cancellano le directory vuote
(e per giunta il cicbrowser le mostra :-) -> Gares
- missing feature unification: applicazione di teoremi (~A) quando il goal