From a2620a2625d198b6fe42c1af213b7f12ea243abc Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 19 Jul 2005 13:11:27 +0000 Subject: [PATCH] ... --- helm/matita/matita.txt | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) 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 -- 2.39.2