...

diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index 376061ff6bb9ea7535c9a8b208c7b0b953f379be..76d0f873a56f080528f02e4f8136599a710b8bf5 100644 (file)
--- a/helm/matita/matita.txt
+++ b/helm/matita/matita.txt
@@ -1,9 +1,5 @@
 TODO
   NUCLEO
-  - CRITICO (trovato anche da Ferruccio): typechecking di
-    cic:/Coq/ring/Ring_normalize/index_eq_prop.con
-    asserzione del nucleo (applicazione senza argomenti).
-    Fissare e poi fare una passata su tutto il db.
   - PREOCCUPANTE: per 
     inductive i : Prop := K : True (*-> i*) -> i.
     noi generiamo i_rec e i_rect con e senza il commento qui sopra; Coq NON
@@ -112,6 +108,9 @@ TODO
     i demoni scopiazzano venti righe per via del getter embedded :-(
 
 DONE
+- CRITICO (trovato anche da Ferruccio): typechecking di
+  cic:/Coq/ring/Quote/index_eq_prop.con
+  asserzione del nucleo (applicazione senza argomenti). -> CSC
 - verificare se tutte le query sono ora ottimizzate (usando il comando
   explain) e usano gli indici in maniera ottimale; inoltre migliorare gli
   indici sulle tabelle hits and count -> CSC