]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/papers/matita/matita2.tex
A new TODO.
[helm.git] / 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}