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
- 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)