From 23641e7c4b061a2dbc5862d763e8c3602793a94c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 27 Jun 2005 13:58:29 +0000 Subject: [PATCH] ... --- helm/matita/matita.txt | 2 ++ 1 file changed, 2 insertions(+) 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 -- 2.39.2