From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
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;hp=ea543eafaae687b248478db7bf6166dd912b5729;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