From 028094be3e6de1765a0927a4ebb5c91ae035efe8 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 11 Jul 2005 11:09:02 +0000 Subject: [PATCH] ... --- helm/matita/matita.txt | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) 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 -- 2.39.2