(**********************************************************************)
TODO
+- eta_expand non usata da nessuno?
+- eliminare eta_fix? (aspettare notazione da Zack e Luca)
+- bug di ferruccio: fare un refresh dei nomi dopo l'applicazione
+ di una tattica. Di quali nomi fare refresh? (Andrea) di quelli
+ veramente ambigui, ovvero dell'ultimo binder tale che sotto di
+ esso un nome viene usato in maniera ambigua. Esempio:
+ \lambda x. \lambda x. (x x) (dove una x e' -2) ==> fare refresh
+ \lambda x. \lambda x. (x x) (dove entrambe sono -1) ==> non fare refresh
+- non eseguire comandi quando lo stato e' diverso da No_proof
+- fare tornare a matitac -1 quando lo stato finale e' diverso da No_proof
+- a volte genera termini con variabili legate da piu' binder
+ Capita quando un tipo dall'environment (e.g. \lambda x.T)
+ viene inserito in un contesto (e.g. x:nat) dove le variabili
+ sono gia' state legate in precedenza.
- script outline -> Zack
- cicBrowser: riagganciare(?) resa di termini scritti
nella URL(??) ->
- controllo per script modificato o meno prima di uscire ->
- riattaccare hbugs (brrr...) -> Zack
- tattica clear ? -> Gares
-- intro = intros 1 -> Gares
-- timetravel -> gares
DONE
+- intro = intros 1 -> Gares
+- timetravel (urimanager) -> Gares
- implementare macro in matitaScript.ml -> Gares
- history deve aggiornare anche la whelp bar -> Gares
- commenti exeguibili (forse devono essere una lista e non