X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fpapers%2Fmatita%2Fmatita2.tex;fp=helm%2Fpapers%2Fmatita%2Fmatita2.tex;h=bd22ffe544f5ff51e1df4f95888f2e911b873314;hb=a031418f35afefcad507d6f13d6a33fd35f3c86b;hp=65b5882af121a964c1c2ec38d7c98055b0c4852f;hpb=ed308fc03be5397081ac0e00bbc73b3f71da1e67;p=helm.git

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index 65b5882af..bd22ffe54 100644
--- a/helm/papers/matita/matita2.tex
+++ b/helm/papers/matita/matita2.tex
@@ -134,7 +134,7 @@ features.
 \subsection{Historical perspective}
 
 The origins of \MATITA{} go back to 1999. At the time we were mostly 
-interested to develop tools and techniques to enhance the accessibility
+interested in developing tools and techniques to enhance the accessibility
 via Web of libraries of formal mathematics. Due to its dimension, the
 library of the \COQ~\cite{CoqManual} proof assistant (of the order of 35'000 theorems) 
 was chosen as a privileged test bench for our work, although experiments
@@ -150,7 +150,7 @@ following steps:
   the time an emerging standard, we naturally adopted that technology,
   fostering a content-centric architecture~\cite{content-centric} where
   the documents of the library were the the main components around which
-  everything else has to be build;
+  everything else has to be built;
 
  \item developing indexing and searching techniques supporting semantic
   queries to the library; 
@@ -273,7 +273,7 @@ assistants. Among them, the advanced indexing tools over the library and
 the parser for ambiguous mathematical notation.
 
 The size and complexity improvements over \COQ{} must be understood
-historically. \COQ{} is a quite old
+historically. \COQ{}\cite{CoqArt} is a quite old
 system whose development started 20 years ago. Since then,
 several developers have took over the code and several new research ideas
 that were not considered in the original architecture have been experimented