From: Claudio Sacerdoti Coen Date: Mon, 11 Jul 2005 11:09:02 +0000 (+0000) Subject: ... X-Git-Tag: pre_notation~51 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=028094be3e6de1765a0927a4ebb5c91ae035efe8;p=helm.git ... --- diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index d1f44f3e6..914de2d4f 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -27,11 +27,8 @@ TODO script visibile nella finestra dello script - Dare errore significativo al posto di NotWellTypedInterpreation - Implementare menu edit: find/replace/cut/copy/undo/etc. -- Bug vari nella generazione dei principi di eliminazione: +- Bug nella generazione dei principi di eliminazione: 1. generazione nomi (usa ref incrementata localmente) - 2. prodotti dipendenti come non-dipendenti (visibili eseguendo passo - passo il test inversion.ma) - 3. usato trucco outtype non dipendenti per il case - elim_intros_simpl e rewrite_simpl: ora non viene usata dal ^^^^^^ ^^^^^^ toplevel la variante che semplifica. Capire quali sono i problemi @@ -71,6 +68,10 @@ TODO diversi/e DONE +- Bug vari nella generazione dei principi di eliminazione: + 2. prodotti dipendenti come non-dipendenti (visibili eseguendo passo + passo il test inversion.ma) + 3. usato trucco outtype non dipendenti per il case - controllo per script modificato o meno prima di uscire -> Gares - LApply deve prendere in input gli identificatori che va a generare; lascio a Ferruccio la scelta della sintassi concreta -> Ferruccio