From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 25 Nov 2005 18:07:41 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~8093
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=720068a32f4353cdb5b35ca6e6b6cfde93f72836;p=helm.git

...
---

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index 491e92548..e2af8870c 100644
--- 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}