From: Claudio Sacerdoti Coen Date: Mon, 27 Jun 2005 13:58:29 +0000 (+0000) Subject: ... X-Git-Tag: INDEXING_NO_PROOFS~42 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=23641e7c4b061a2dbc5862d763e8c3602793a94c;p=helm.git ... --- diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index cc75cefaa..4ff85a1aa 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -2,6 +2,8 @@ (**********************************************************************) TODO +- LApply deve prendere in input gli identificatori che va a generare; + lascio a Ferruccio la scelta della sintassi concreta - elim_intros_simpl e rewrite[_back]_simpl: ora non viene usata dal ^^^^^^ ^^^^^^ toplevel la variante che semplifica. Capire quali sono i problemi