From 2e1672d9ba529522ab0c6a058c212a6a75aa22a4 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 20 Sep 2005 11:17:26 +0000 Subject: [PATCH] ... --- helm/matita/matita.txt | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index 3ec54f51e..3947bbbad 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -17,12 +17,6 @@ TODO le eccezioni, farlo quando vengono presentate all'utente. Motivo: il calcolo del messaggio di errore puo' essere estremamente costoso (e' gia' successo!) quando poi il messaggio non serve!!! - - missing feature unification: applicazione di teoremi (~A) quando il goal - e' False o di teoremi $symmetric R P$ quando il goal e' $P(x,y)$. - Fare un passo di delta[-beta?][-iota-etc.] quando da una parte c'e' una - testa rigida (che si espande in una freccia)? Ma il punto e' che il bug - non e' di unificazione, bensi' nella fase di preparazione del goal per - la apply. - verificare il comportamento di tutte le tattiche con il parsing lazy -> CSC - file elim.ma: vengono creati lambda dummy e referenziati nell'outtype di un case @@ -30,12 +24,6 @@ TODO - comportamento di tutte le tattiche nei confronti dei let-in - elim con pattern - assiomi (manca sintassi concreta e AST). - - 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! - Dare errore significativo al posto di NotWellTypedInterpreation -> CSC - elim_intros_simpl e rewrite_simpl: ora non viene usata dal ^^^^^^ ^^^^^^ @@ -115,6 +103,18 @@ TODO DEMONI E ALTRO DONE +- missing feature unification: applicazione di teoremi (~A) quando il goal + e' False o di teoremi $symmetric R P$ quando il goal e' $P(x,y)$. + Fare un passo di delta[-beta?][-iota-etc.] quando da una parte c'e' una + testa rigida (che si espande in una freccia)? Ma il punto e' che il bug + non e' di unificazione, bensi' nella fase di preparazione del goal per + la apply -> CSC, Gares +- 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! -> CSC, Gares - codice di inizializzazione di matita, matitac, matitatop replicato e non in sync -> Gares - tutte gli script che parsano (e.g. matitaclean, matitadep) debbono -- 2.39.2