...

diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index 914de2d4f2de297b8ee971ea872d1e0d1f93dffa..ebad4ed6172d6134d3e028e06802790585f952c2 100644 (file)
--- a/helm/matita/matita.txt
+++ b/helm/matita/matita.txt
@@ -2,10 +2,6 @@
 (**********************************************************************)
 
 TODO
-- Bug: non disambigua
-  inductive i (x:nat) : bool \to Prop \def K : bool \to (i x true) \to (i x false).
-  perche' non inserisce nat nel domain di disambiguazione. Deve esserci un bug
-  stupido da qualche parte
 - preoccupante: per 
   inductive i (x:nat) : bool \to Prop \def K : bool \to (i x true) \to (i x false).
   noi generiamo anche i_rec e i_rect che Coq non genera (e che NON dovrebbero
@@ -68,10 +64,14 @@ TODO
   diversi/e
 
 DONE
+- Bug: non disambigua
+  inductive i (x:nat) : bool \to Prop \def K : bool \to (i x true) \to (i x false).
+  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:
    2. prodotti dipendenti come non-dipendenti (visibili eseguendo passo
-      passo il test inversion.ma)
-   3. usato trucco outtype non dipendenti per il case
+      passo il test inversion.ma) -> CSC, Gares
+   3. usato trucco outtype non dipendenti per il case -> CSC, Gares
 - 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