--- /dev/null
+V7.2:
+
+Da valutare:
+ * MetaLinguaggio di David Delayale per l'implementazione di tattiche
+
+V6.3:
+
+Da valutare:
+ * Print
+ * Extraction
+ * Opaque/Transparent
+ * SearchIsos
+ * Load di script di tattiche
+ * "Pretty" Parsing
+ * Log dei tempi per ogni possibile richiesta
+ * Undo
+ * Focus/Unfocus (nella prova completa in linguaggio naturale)
+ * Show Tree (resa dell'albero dei sequenti)
+ * Tatticali:
+ - OrElse
+ - Repeat
+ - Do
+ - Info
+ - Try
+ - First
+ - Solve
+ - Abstract
+ - ;
+ - ; [ ... | ... | ... ]
+ - (...)
+ * Assumption
+ * Apply with
+ * LApply
+ * Absurd
+ * Contradiction
+ * Cbv/Lazy Beta Delta Iota Zeta
+ * Red (riduzione di un backbone con delta della testa + beta e iota)
+ * Unfold (equivalente a Hnf dell'occorrenza)
+ * Pattern
+ * Constructor n / Split / Left/ Right/ Exists/ Reflexivity
+ * Elim term quando term ha come tipo un Pi
+ * ElimType (fatta da Zack; metterla disponibile)
+ * Induction su una applicazione
+ * Induction su una ipotesi
+ * Case su una applicazione e su una ipotesi
+ * Intros destrutturante
+ * Decompose
+ * Double Induction
+ * Rewrite (ma eliminare un'uguaglianza o applicare eq_ind_r non funziona gia'?)
+ * Replace (che prende due termini _NON_ convertibili e genera come goal
+ l'uguaglianza dei due). Unificarla con la change, che diventa la replace
+ non overkilling?
+ * Symmetry e Transitivity (basta applicare i due teoremi giusti)
+ * Decide Equality (ma non dovrebbe essere un teorema???)
+ * Compare
+ * Discriminate
+ * Injection
+ * Simplify_eq (== Discriminate o Injection su una ipotesi)
+ * Dependent Rewrite
+ * Inversion [Nota: Derive Inversion genera e salva il teorema!]
+ * Quote (per implementare tattiche riflessive senza scrivere codice ML!!!!)
+ * Tauto/Intuition
+ * Linear
+ * AutoRewrite
+ * Realizer/Program
+ * Scheme
+ * Omega
+
+Implementate:
+ * Enunciare un teorema
+ * (Ri)aprire un teorema gia' dimostrato per modificarne certe parti
+ * Check (e successiva possibilita' di applicare reduction tactics)
+ * Exact
+ * Apply/EApply
+ * Cut
+ * Change [Una conversion tactic. Problema: il termine digitato viene
+ parsato nel contesto della conclusione e non in quello della selezione!!!]
+ * Conversion tactics, sia nelle ipotesi che nella conclusione:
+ - Reduce (== Compute)
+ - Hnf
+ - Simpl
+ * Fold
+ * ElimIntrosSimpl
+ * Let...In (= LetTac)
+ * Salvare e caricare una prova incompleta (ma nel posto sbagliato!)
+ * ClearBody
+ * Clear
+ * Ring
+
+Da implementare:
+ * Implicit: quando si usano gli implicit, l'input non puo' piu' essere
+ type-checkato, ma bisogna fare una refine (ancora non implementata).
+ Di conseguenza _OGNI_ tattica si rompe. Inoltre l'implementazione di
+ Implicit e' ancora errata in quanto il contesto canonico delle nuove
+ variabili e' sempre vuoto anche se dovrebbe essere uguale a quello
+ di partenza + le nuove variabili introdotte durante il parsing.
+ * Nella type_of NON viene controllato che il metasenv di una current-proof
+ sia ben formato. PUNTO IMPORTANTE: farlo nel metasenv parziale, cosi' da
+ evitare cicli; ma dopo e' un bordello l'unificazione. Oppure fare un
+ semplice controllo di aciclicita'.
+ * ClearBody e Clear NON restringono ancora altre metavariabili. Invece viene
+ sollevata un'eccezione di tipaggio. Esempio: n:nat |- ?1[n] se faccio clear
+ di n dovrei restringere ?1. Se invece prima faccio clear di n in ?1, quando
+ torno su questo goal e faccio clear di n ottengo un'eccezione di CicPp.
+ * La reduction_tactic (in ProofEngine.ml) e' bacatissima, come descritto
+ nei commenti. Fixare.
+ * Reimplementare Cut usando LetIn + applicazione + Intro oppure usando
+ LetIn + ClearBody (soluzione piu' elegante IMHO)
+ * Refine
+ ? Sia [x:=t]r il tipo di [x:t]k e x non occorra mai libera in r.
+ Dovrei forse tornare semplicemente r?
+ ? Cambiare il nome delle META da int a una stringa?
+ [ATTENZIONE: CAMBIAMENTO NELLA DTD]
+ * Fold e' l'inverso di Reduce e quindi non disfa cio' che viene fatto da
+ Simpl e da Whd. Generalizzarlo facendo Reduce e poi Change con ogni termine?
+ Oppure fare una FoldWhd, una FoldHnf, una FoldSimpl, etc.?
+ * Fold localizzato in un termine selezionato
+ * Move e "Unclear" (che fa l'undo di Clear/Move e conversioni nelle ipotesi)
+ Non sono implementabili. Ma avrebbero senso?
+ * queries e roba basata sulle queries:
+ - Search
+ - Locate (anche di tipi induttivi e costruttori)
+ - Auto
+ - EAuto
+ - Prolog (???????????)
+ * Save con tanto di esportazione: esportare nel posto giusto!
+ * Dare una definizione (quasi equivalente a check + unfold, ma mancano
+ gli inner-types)
+ * Dare una definizione induttiva
+ * Intro (Come scegliere i nomi freschi?) e Intros until
+ * Generalize
+ * Fissare il bug di change (ovvero il problema del contesto in cui viene
+ parsato l'input dell'utente)
+ * Tornare un errore se si cerca di applicare una reduction tactic in una
+ ipotesi nella scratch area
+ * Field
+ * JProver. Che rapporto c'e' fra JProver e Tauto/Intuition?
+ * altre contrib da integrare?
+
+Da non implementare:
+ * Print All
+ * Compile/Read/Require
+ * Print/Save/Restore States
+ * Let