From dba5a2c487d4c026c63cef4a9e81662bf11e8b8e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 6 Sep 2005 14:14:13 +0000 Subject: [PATCH] ... --- helm/matita/matita.txt | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index ec623f7e5..df4ac166d 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -5,14 +5,13 @@ TODO noi generiamo i_rec e i_rect con e senza il commento qui sopra; Coq NON genera i_rec e i_rect quando c'e' un argomento ricorsivo. (CSC: manca vincolo aggiuntivo non dipendente dalla sorta per il caso in - questione) -> CSC + questione) -> Gares - bug universi e tipi induttivi - Set predicativo TATTICHE - - tattiche e fallimenti: una tattica che non progredisce dovrebbe fallire, - giusto? + - tattiche e fallimenti: una tattica che non progredisce dovrebbe fallire - comportamento di tutte le tattiche nei confronti dei let-in - tattica unfold su rel a let-in bound variables: c'e' ancora un bug aperto: "unfold x in H:..." la x passata alla unfold vive nel contesto -- 2.39.2