...

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index 44e301a79319d6f65b19db2854f709e9da20b393..f1699bc2f495f1a9ad7e2ebb020fad09117efa07 100644 (file)
--- a/helm/papers/matita/matita2.tex
+++ b/helm/papers/matita/matita2.tex
@@ -409,6 +409,19 @@ translation is an ambiguous language and the user is free to associate
 to every content level term several different interpretations (as a
 partially specified term).
 
+The \MATITA{} proof assistant and the \WHELP{} search engine are both linked
+against the \texttt{cic\_disambiguation} and \texttt{content\_pres} libraries
+since they provide an interface to the user. In both cases the formulae
+written by the user are parsed using the \texttt{content\_pres} library and
+then disambiguated using the \texttt{cic\_disambiguation} library.
+
+The \UWOBO{} Web service wraps the \texttt{content\_pres} library,
+providing a rendering service for the documents in the distributed library.
+To render a document given its URI, \UWOBO{} retrieves it using the
+\GETTER{} obtaining a document with fully specified terms. Then it translates
+it to the presentation level passing through the content level. Finally
+it returns the result document to be rendered by the user's browser.
+
 \hrule
 
 At the bottom of the DAG we have a few libraries (\texttt{extlib},