-records kept by the system. On the contrary, in \MATITA{} proof terms are
-praised as declarative versions of the proof. Playing that role, they are the
-primary mean of communication of proofs (once rendered to natural language
-for human audiences).
-
-The user interfaces now adopted by all the proof assistants based on a
-procedural proof language have been inspired by the CtCoq pioneering
+records kept by the system.
+In \MATITA{}, which has been conceived for a potentially distributed
+library, proof terms are also meant as the primary representation for
+storage and communication with other systems (e.g. \COQ).
+%On the contrary, in \MATITA{} proof terms are
+%praised as declarative versions of the proof. Playing that role, they are the
+%primary mean of communication of proofs (once rendered to natural language
+%for human audiences).
+
+All the user interfaces currently adopted by proof assistants based on a
+procedural proof language have been influenced by the CtCoq pioneering