]> matita.cs.unibo.it Git - helm.git/commitdiff
A new TODO.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 31 Jan 2006 09:24:23 +0000 (09:24 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 31 Jan 2006 09:24:23 +0000 (09:24 +0000)
helm/papers/matita/matita2.tex

index d31afebed073586b685d0074090afcb3268018f9..7f618f656ac51460ead37345fe5fa0c07d367745 100644 (file)
@@ -1437,6 +1437,8 @@ can automatically generate from the selection.
 
 \subsubsection{Tactics supporting patterns}
 
+\TODO{Grazie ai pattern, rispetto a Coq noi abbiamo per esempio la possibilita' di fare riduzioni profonde!!!}
+
 \TODO{mergiare con il successivo facendo notare che i patterns sono una
 interfaccia comune per le tattiche}