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