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