From c97025ab25fcb1ce417d59d1ebfd5dd4f8526de4 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 2 Sep 2005 10:01:55 +0000 Subject: [PATCH] ... --- helm/matita/matita.txt | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index 376061ff6..76d0f873a 100644 --- 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 -- 2.39.2