From: Claudio Sacerdoti Coen Date: Tue, 19 Jul 2005 13:11:27 +0000 (+0000) Subject: ... X-Git-Tag: V_0_7_2~169 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a2620a2625d198b6fe42c1af213b7f12ea243abc;p=helm.git ... --- diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index 2124c9be0..b882d4d0a 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -22,8 +22,6 @@ TODO in primitiveTactics.ml. Potrebbe essere causa di rallentamento della apply oltre che di bug! - 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 ^^^^^^ ^^^^^^ toplevel la variante che semplifica. Capire quali sono i problemi @@ -103,6 +101,7 @@ DONE perche' non inserisce nat nel domain di disambiguazione. Deve esserci un bug stupido da qualche parte -> CSC - Bug vari nella generazione dei principi di eliminazione: + 1. generazione nomi (usa ref incrementata localmente) -> Andrea 2. prodotti dipendenti come non-dipendenti (visibili eseguendo passo passo il test inversion.ma) -> CSC, Gares 3. usato trucco outtype non dipendenti per il case -> CSC, Gares