...

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index 491e925483699e8d83ec396da4d63d44f150e7a5..e2af8870cba8fd4ecfd17cbb8da013a7e19d0177 100644 (file)
--- a/helm/papers/matita/matita2.tex
+++ b/helm/papers/matita/matita2.tex
@@ -191,6 +191,15 @@ overall management of the library, integrating everything into a
 single system. \MATITA{} is the result of this effort. 
 
 \subsection{The System}
+DESCRIZIONE DEL SISTEMA DAL PUNTO DI VISTA ``UTENTE''
+
+\begin{itemize}
+ \item scelta del sistema fondazionale
+ \item sistema indipendente (da Coq)
+ \item compatibilit\`a con sistemi legacy
+\end{itemize}
+
+\subsection{Relationship with \COQ{}}
 
 At first sight, \MATITA{} looks as (and partly is) a \COQ{} clone. This is
 more the effect of the circumstances of its creation described 
@@ -241,19 +250,9 @@ In the future we plan to exploit \MATITA{} as a test bench for new ideas and
 extensions. Keeping the single libraries and the whole architecture as
 simple as possible is thus crucial to speed up future experiments and to
 allow other developers to quickly understand our code and contribute.
-For direct experience of the authors, the learning curve to understand and
-be able to contribute to \COQ{}'s code is quite steep and requires direct
-and frequent interactions with \COQ{} developers.
-
-\begin{itemize}
- \item scelta del sistema fondazionale
- \item sistema indipendente (da Coq)
-  \begin{itemize}
-   \item possibilit\`a di sperimentare (soluzioni architetturali, logiche,
-    implementative, \dots)
-   \item compatibilit\`a con sistemi legacy
-  \end{itemize}
-\end{itemize}
+%For direct experience of the authors, the learning curve to understand and
+%be able to contribute to \COQ{}'s code is quite steep and requires direct
+%and frequent interactions with \COQ{} developers.
 
 \begin{figure}[t]
  \begin{center}