From ab7910f821b16fceae542ac7a7588b93051d7359 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 7 Jul 2005 12:15:27 +0000 Subject: [PATCH] ... --- helm/matita/matita.txt | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index 3d272d378..566d59e6a 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -2,6 +2,11 @@ (**********************************************************************) TODO +- Bug vari 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 -- 2.39.2