con pattern, visto che in tal caso e' l'intero parsing a dover essere
fatto in un contesto differente. Risolvendo quel bug si risolve
automaticamente anche questo.
+ - elim con pattern
- theorem t: True. elim x. ==> BOOM! unificazione di una testa flessibile con
True.
- parsing contestuale (tattiche replace, change e forse altre)
- non chiudere transitivamente i moo ??
DEMONI E ALTRO
- - implementare inclusione file di configurazione (perche' ora tutti
- i demoni scopiazzano venti righe per via del getter embedded :-(
DONE
+- implementare inclusione file di configurazione (perche' ora tutti
+ i demoni scopiazzano venti righe per via del getter embedded :-( -> Zack
- simplify non debbono zeta-espandere i let-in -> CSC, Gares
- integrare nuova contrib ferruccio nel bench notturno e rilocarla in
contribs o qualcosa del genere -> CSC