X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fpapers%2Fmatita%2Fmatita.tex;h=b5c27f1bfd0eed62ce3beaffa2342fdb78938a81;hb=0f0e760ebe7483631922be798113ec8c514c292f;hp=6738aed4ab1ba5486417b74f0975320875015891;hpb=4cde46f31cb4e9e74d7872d638680d593d294eff;p=helm.git

diff --git a/helm/papers/matita/matita.tex b/helm/papers/matita/matita.tex
index 6738aed4a..b5c27f1bf 100644
--- a/helm/papers/matita/matita.tex
+++ b/helm/papers/matita/matita.tex
@@ -161,7 +161,20 @@ add an authoring interface, and a set of functionalities for the
 overall management of the library, integrating everything into a
 single system. {\em Matita} is the result of this effort. 
 
-
+At first sight, Matita looks as (and partly is) a Coq clone. This is
+more the effect of the circumstances of its creation described 
+above than the result of a deliberate design. In particular, we
+(essentially) share the same foundational dialect of Coq (the
+Calculus of Inductive Constructions), the same implementative
+language (Ocaml), and the same (script based) authoring philosophy.
+However, as we shall see, the analogy essentially stops here. 
+
+In a sense; we like to think of Matita as the way Coq would 
+look like if entirely rerwritten from scratch: just to give an
+idea, although Matita currently supports almost all functionalities of
+Coq, it links 60000 lins of coaml code, against ... of Coq (and
+we are convinced that, starting from scratch againg, we could furtherly
+reduce our code in sensible way).   
 
 
 \begin{itemize}