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

index c29a9a031dc1a5f96115c3834cf0129d0e96688c..6b0102d1f37bee74d499ed462ca5e325ea6d444c 100644 (file)
@@ -27,6 +27,7 @@ TODO
     con pattern, visto che in tal caso e' l'intero parsing a dover essere
     fatto in un contesto differente. Risolvendo quel bug si risolve
     automaticamente anche questo.
+  - elim con pattern
   - theorem t: True. elim x. ==> BOOM! unificazione di una testa flessibile con
     True.
   - parsing contestuale (tattiche replace, change e forse altre)
@@ -122,10 +123,10 @@ TODO
   - non chiudere transitivamente i moo ?? 
 
   DEMONI E ALTRO
-  - implementare inclusione file di configurazione (perche' ora tutti
-    i demoni scopiazzano venti righe per via del getter embedded :-(
 
 DONE
+- implementare inclusione file di configurazione (perche' ora tutti
+  i demoni scopiazzano venti righe per via del getter embedded :-( -> Zack
 - simplify non debbono zeta-espandere i let-in -> CSC, Gares
 - integrare nuova contrib ferruccio nel bench notturno e rilocarla in
   contribs o qualcosa del genere -> CSC