(**********************************************************************)
TODO
+- 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!
+- 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
^^^^^^ ^^^^^^
toplevel la variante che semplifica. Capire quali sono i problemi
e/o cosa fare delle varianti con semplificazione.
- eta_expand non usata da nessuno?
-- eliminare eta_fix? (aspettare notazione da Zack e Luca)
+- notazione -> Luca e Zack
+- eliminare eta_fix? (aspettare notazione)
+- bug di refresh del widget quando si avanza ("swap" tra la finestra dei
+ sequenti e la finestra dello script)
+- feedback su hyperlink nei sequenti e nel browser: rendere visibili gli
+ hyperlink (cursore a "manina"? hyperlink evidenziati?). La maction che
+ collassa la prova e' fastidiosa: la prova si chiude se non si clicca
+ correttamente su un hyperlink
+- disabilitare (set_sensitive false) menu e bottoni mentre matita sta
+ processando lo script per evitare interazioni pericolose
- 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
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
+- script outline -> Zack
- cicBrowser: riagganciare(?) resa di termini scritti
- nella URL(??) ->
-- menu contestuale (tasto dx) nel sequent viewer ->
+ nella URL(??)
+- menu contestuale (tasto dx) nel sequent viewer -> attende notazione
- riattaccare hbugs (brrr...) -> Zack
+- gestione dei path per include: il path deve essere assoluto? da decidere ...
+- highlight degli errori di parsing nello script (usando lo sfondo come per la
+ parte lockata di testo, da ripulire quando si modifica il testo o si sposta il
+ punto di esecuzione)
+- salvare la parte di testo lockata dagli effetti di undo/redo (come?????)
+- supportare l'apertura di piu' script contemporaneamente in tab/finestre
+ diversi/e
DONE
- controllo per script modificato o meno prima di uscire -> Gares
projects / helm.git / blobdiff