]> matita.cs.unibo.it Git - helm.git/commitdiff
...
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 6 Sep 2005 14:14:13 +0000 (14:14 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 6 Sep 2005 14:14:13 +0000 (14:14 +0000)
helm/matita/matita.txt

index ec623f7e5ec7f4906b6e00ec863a557867c2e3da..df4ac166d17682dd074cb058b785e6e434b809da 100644 (file)
@@ -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