- use "sec:libmanagement" as label for compilation/decompilation (it was not

  uniformly used before)
- typos in the disambiguation section

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index 49c5315902d20737540263e8319cd1a2b4a5ae4c..f1bc990c7d36c6799535bf47edd3e26e688fed4c 100644 (file)
--- a/helm/papers/matita/matita2.tex
+++ b/helm/papers/matita/matita2.tex
@@ -411,7 +411,7 @@ content level terms; presentation level terms.
    of preserving the coherence of the library and the database. For instance,
    when a notion is removed, all the notions that depend on it and their
    metadata are removed from the library. This aspect will be better detailed
-   in Sect.~\ref{decompilazione}.
+   in Sect.~\ref{sec:libmanagement}.
    
 \subsection{Partially specified terms}
 \emph{Partially specified terms} are CIC terms where subterms can be omitted.
@@ -695,7 +695,7 @@ content selection and copy-paste.
 
 
 \subsection{Compilation and decompilation}
-\label{compilazione}
+\label{sec:libmanagement}
 
 The aim of this section is to describe the way matita 
 preserves the consistency and the availability of the library
@@ -912,7 +912,7 @@ translated (in multiple steps) to partially specified terms as sketched in
 Sect.~\ref{sec:contentintro}.
 
 The key component of the translation is the generic disambiguation algorithm
-implemented in the \texttt{disambiguation} library of Fig.~\ref{fig:libraries}
+implemented in the \texttt{disambiguation} component of Fig.~\ref{fig:libraries}
 and presented in~\cite{disambiguation}. In this section we present how to use
 such an algorithm in the context of the development of a library of formalized
 mathematics. We will see that using multiple passes of the algorithm, varying
@@ -933,7 +933,7 @@ definition gt: nat \to nat \to Prop \def
 
 The \texttt{include} statement adds the requirement that the part of the library
 defining the notion of natural numbers should be defined before
-processing the following definition. Note indeed that the algorithm presented
+processing the what follows. Note indeed that the algorithm presented
 in~\cite{disambiguation} does not describe where interpretations for ambiguous
 expressions come from, since it is application-specific. As a first
 approximation, we will assume that in \MATITA{} they come from the library (i.e.
@@ -1029,7 +1029,7 @@ theorem lt_to_Zlt_pos_pos:
 Unfortunately, none of the passes described above is able to disambiguate its
 type, no matter how aliases are defined. This is because the \OP{<} operator
 occurs twice in the content level term (it has two \emph{instances}) and two
-different interpretation for it have to be used in order to obtain a refinable
+different interpretations for it have to be used in order to obtain a refinable
 partially specified term. To address this issue, we have the ability to consider
 each instance of a single symbol as a different ambiguous expression in the
 content level term, and thus we can assign a different interpretation to each of
@@ -1076,7 +1076,7 @@ the \texttt{pos} constructor itself), the theorem can be disambiguated using
 twice that coercion on the left hand side of the implication. The obtained
 partially specified term however would not probably be the expected one, being a
 theorem which prove a trivial implication. For this reason we choose to always
-prefer fresh instances over implicit coercion, i.e. we always attempt
+prefer fresh instances over implicit coercions, i.e. we always attempt
 disambiguation passes with fresh instances before attempting passes with
 implicit coercions.