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

...
---

diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index c29a9a031..6b0102d1f 100644
--- a/helm/matita/matita.txt
+++ b/helm/matita/matita.txt
@@ -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