From 69eb85b72b44b0af8d626fd97324ece59b91077d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 8 Sep 2005 17:13:46 +0000 Subject: [PATCH] ... --- helm/matita/matita.txt | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index 478cd77ab..d71a5f510 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -17,7 +17,7 @@ TODO - tattiche e fallimenti: una tattica che non progredisce dovrebbe fallire - comportamento di tutte le tattiche nei confronti dei let-in - elim con pattern - - theorem t: True. elim x. ==> BOOM! unificazione di una testa flessibile con + - theorem t: True. elim O. ==> BOOM! unificazione di una testa flessibile con True. - assiomi (manca sintassi concreta e AST). - Guardare il commento @@ -128,8 +128,8 @@ DONE NOTA: questo bug e' legato a quello di parsing in presenza di tattiche con pattern, visto che in tal caso e' l'intero parsing a dover essere fatto in un contesto differente. Risolvendo quel bug si risolve - -> Zack, Enrico, CSC automaticamente anche questo. + -> Zack, Enrico, CSC - Usare il cicbrowser per fare "Whelp instance": lui riscrive la barra con la notazione alla Coq V7.0 che non riesce piu' a riparsare! -> Zack - implementare inclusione file di configurazione (perche' ora tutti -- 2.39.2