From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 20 Sep 2005 11:17:26 +0000 (+0000)
Subject: ...
X-Git-Tag: LAST_BEFORE_NEW~86
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2e1672d9ba529522ab0c6a058c212a6a75aa22a4;p=helm.git

...
---

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