...

[helm.git] / helm / matita / matita.txt

diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index c29a9a031dc1a5f96115c3834cf0129d0e96688c..6b0102d1f37bee74d499ed462ca5e325ea6d444c 100644 (file)
--- 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