From: Claudio Sacerdoti Coen Date: Tue, 6 Sep 2005 14:14:13 +0000 (+0000) Subject: ... X-Git-Tag: V_0_1_2_1~76 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dba5a2c487d4c026c63cef4a9e81662bf11e8b8e;p=helm.git ... --- 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