From 52af0e3a6ab827464f33b90bf0d39e5df3169499 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 6 Sep 2005 10:24:58 +0000 Subject: [PATCH] ... --- helm/matita/matita.txt | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) 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 -- 2.39.2