+- Bug: non disambigua
+ inductive i (x:nat) : bool \to Prop \def K : bool \to (i x true) \to (i x false).
+ perche' non inserisce nat nel domain di disambiguazione. Deve esserci un bug
+ stupido da qualche parte
+- preoccupante: per
+ inductive i (x:nat) : bool \to Prop \def K : bool \to (i x true) \to (i x false).
+ noi generiamo anche i_rec e i_rect che Coq non genera (e che NON dovrebbero
+ essere accettati dal nostro nucleo che invece non fa una piega!!!)
+- parsing contestuale (tattiche replace, change e forse altre)
+- assiomi
+- Guardare il commento
+ (*CSC: this code is suspect and/or bugged: we try first without reduction
+ and then using whd. However, the saturate_term always tries with full
+ reduction without delta. *)
+ in primitiveTactics.ml. Potrebbe essere causa di rallentamento della apply
+ oltre che di bug!
+- Bug di cut&paste: se si fa cut&paste di testo lockato si ottiene testo
+ lockato!
+- keybinding globali: CTRL-{su,giu,...} devono fungere anche quando altre
+ finestre hanno il focus (e.g. cicBrowser). C'e' gia' da qualche parte il
+ codice che aggiunge i keybinding a tutte le eventBox, e' da ripristinare
+- quando si sposta il punto di esecuzione dello script cambiare la parte di
+ script visibile nella finestra dello script
+- Dare errore significativo al posto di NotWellTypedInterpreation
+- Implementare menu edit: find/replace/cut/copy/undo/etc.
+- Bug vari nella generazione dei principi di eliminazione:
+ 1. generazione nomi (usa ref incrementata localmente)
+ 2. prodotti dipendenti come non-dipendenti (visibili eseguendo passo
+ passo il test inversion.ma)
+ 3. usato trucco outtype non dipendenti per il case
+- elim_intros_simpl e rewrite_simpl: ora non viene usata dal
+ ^^^^^^ ^^^^^^