...

diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index ec623f7e5ec7f4906b6e00ec863a557867c2e3da..df4ac166d17682dd074cb058b785e6e434b809da 100644 (file)
--- a/helm/matita/matita.txt
+++ b/helm/matita/matita.txt
@@ -5,14 +5,13 @@ TODO
     noi generiamo i_rec e i_rect con e senza il commento qui sopra; Coq NON
     genera i_rec e i_rect quando c'e' un argomento ricorsivo.
     (CSC: manca vincolo aggiuntivo non dipendente dalla sorta per il caso in
-    questione) -> CSC
+    questione) -> Gares
   - bug universi e tipi induttivi
   - Set predicativo
     
 
   TATTICHE
-  - tattiche e fallimenti: una tattica che non progredisce dovrebbe fallire,
-    giusto?
+  - tattiche e fallimenti: una tattica che non progredisce dovrebbe fallire
   - comportamento di tutte le tattiche nei confronti dei let-in
   - tattica unfold su rel a let-in bound variables: c'e' ancora un bug
     aperto: "unfold x in H:..." la x passata alla unfold vive nel contesto