...

diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index 2124c9be052f73b50357325b4b9fa691bd3111c7..b882d4d0ad73b904a4d134c0826b1a609715d9f1 100644 (file)
--- 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