...

diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index 3ec54f51e2ccc0e14f4f5494f0577d44ba52da66..3947bbbadedd8d2c79f1d6bdfd47cc200b88c020 100644 (file)
--- 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