X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fpapers%2Fmatita%2Fmatita2.tex;h=9e3739f320c4c5ef6b45a3f6f2bc140ff3513d42;hb=d40dccf9dbf0f1792e0f2cbac3c3b3c8fb0c14cb;hp=9617915f2d7631b54f021a0d37f69fd615bb44f1;hpb=5d86c5b5ef8d3c4b92bd00a1aebdad10143bc58e;p=helm.git

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index 9617915f2..9e3739f32 100644
--- a/helm/papers/matita/matita2.tex
+++ b/helm/papers/matita/matita2.tex
@@ -221,12 +221,12 @@ that has set a sort of
 standard way to interact with the system. Several procedural proof assistants
 have either adopted or cloned Proof General as their main user interface.
 The authoring interface of \MATITA{} is a clone of the Proof General interface.
+On the contrary, the interface to interact with the library is rather
+innovative and directly inspired by the Web interfaces to our Web servers.
 
-\TODO{item che seguono:}
-\begin{itemize}
- \item sistema indipendente (da \COQ)
- \item compatibilit\`a con sistemi legacy
-\end{itemize}
+\MATITA{} is backward compatible with the XML library of proof objects exported
+from \COQ{}, but, in order to test the actual usability of the system, we are
+also developing a new library of basic results from scratch.
 
 \subsection{Relationship with \COQ{}}