From ccb64f7d77f64e17668e286b60cd2b6631a2e57f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 12 Sep 2005 10:26:36 +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 25980c66f..e0ecd3993 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -17,8 +17,6 @@ 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 O. ==> BOOM! unificazione di una testa flessibile con - True. - assiomi (manca sintassi concreta e AST). - Guardare il commento (*CSC: this code is suspect and/or bugged: we try first without reduction @@ -121,6 +119,8 @@ TODO DEMONI E ALTRO DONE +- theorem t: True. elim O. ==> BOOM! unificazione di una testa flessibile con + True -> Gares - parsing contestuale (tattiche replace, change e forse altre) capire dove fare la select per avere i contesti in cui disambiguare gli altri argomenti. -> Zack, Enrico, CSC -- 2.39.2