]> matita.cs.unibo.it Git - helm.git/commitdiff
...
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 27 Jun 2005 13:58:29 +0000 (13:58 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 27 Jun 2005 13:58:29 +0000 (13:58 +0000)
helm/matita/matita.txt

index cc75cefaaa9bcb2a62c6330fa144feb4d57d8439..4ff85a1aa2281c6146a5987b20a20633decbc3cb 100644 (file)
@@ -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