From: Enrico Tassi Date: Mon, 11 Jul 2005 15:41:25 +0000 (+0000) Subject: ... X-Git-Tag: pre_notation~35 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8146c38b7a6658c03fcf825ba7dd25b7c824f499;p=helm.git ... --- diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index b264bd295..5f213100a 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -5,7 +5,7 @@ TODO noi generiamo i_rec e i_rect con e senza il commento qui sopra; Coq NON genera i_rec e i_rect quando c'e' un argomento ricorsivo. (CSC: manca vincolo aggiuntivo non dipendente dalla sorta per il caso in - questione) + questione) -> CSC TATTICHE @@ -21,7 +21,7 @@ TODO reduction without delta. *) in primitiveTactics.ml. Potrebbe essere causa di rallentamento della apply oltre che di bug! - - Dare errore significativo al posto di NotWellTypedInterpreation + - Dare errore significativo al posto di NotWellTypedInterpreation -> CSC - Bug nella generazione dei principi di eliminazione: 1. generazione nomi (usa ref incrementata localmente) - elim_intros_simpl e rewrite_simpl: ora non viene usata dal @@ -29,7 +29,7 @@ TODO toplevel la variante che semplifica. Capire quali sono i problemi e/o cosa fare delle varianti con semplificazione. (con sintassi concreta alla \section*, analogamente cut e similia che fanno - intros... ) + intros... ) -> CSC - eta_expand non usata da nessuno? (ask Andrea?) - eliminare eta_fix? (aspettare notazione) (correlato con sopra?) - bug di ferruccio: fare un refresh dei nomi dopo l'applicazione