From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 6 Sep 2005 14:14:13 +0000 (+0000)
Subject: ...
X-Git-Tag: V_0_1_2_1~76
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dba5a2c487d4c026c63cef4a9e81662bf11e8b8e;p=helm.git

...
---

diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index ec623f7e5..df4ac166d 100644
--- 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