- minor corrections in the disambiguation section

[helm.git] / helm / papers / matita / matita2.tex

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index 353066a8837d2acc81f8054cc9db46dcef1ff922..d2e1616ed99d647c9ebd1b78f464bd3572e908ae 100644 (file)
--- a/helm/papers/matita/matita2.tex
+++ b/helm/papers/matita/matita2.tex
@@ -951,7 +951,6 @@ instance, in the example above disambiguation succeeds in the multi-preference
 pass. In the third pass, called \emph{library-preferences}, all aliases
 available in the library are considered.
 
-\TODO{rivedere questo periodo\ldots}
 The rationale behind this choice is trying to respect user preferences in early
 passes that complete quickly in case of failure; later passes are slower but
 have more chances of success.
@@ -979,18 +978,18 @@ it is said to be using \emph{fresh instances} (opposed to a \emph{shared
 instances} pass).
 
 Fresh instances lead to a non negligible performance loss (since the choice of
-an alias for one instances does not constraint the choice of the others). For
+an alias for one instance does not constraint the choice of the others). For
 this reason we always attempt a fresh instances pass only after attempting a
 non-fresh one.
 
 \paragraph{One-shot preferences} Disambiguation preferecens as seen so far are
 instance-independent. However, implicit preferences obtained as a result of a
 disambiguation pass which uses fresh instances ought to be instance-dependent.
-Informally, the set of preferences that can be satisfied by the disambiguator on
+Informally, the set of preferences that can be respected by the disambiguator on
 the theorem above is: ``the first instance of the \OP{<} symbol is over natural
 numbers, while the second is on integer numbers''.
 
-Instance-depend preferences are meaningful only for the term whose
+Instance-dependent preferences are meaningful only for the term whose
 disambiguation generated it. For this reason we call them \emph{one-shot
 preferences} and \MATITA{} does not use them to disambiguate further terms in
 the script.
@@ -1024,19 +1023,20 @@ The choice of whether implicit coercions are enabled or not interact with the
 choice about operator instances. Indeed, consider again
 \texttt{lt\_to\_Zlt\_pos\_pos}, which can be disambiguated using fresh operator
 instances. In case there exists a coercion from natural numbers to (positive)
-integers (which indeed does, it is the \texttt{pos} constructor itself), the
+integers (which indeed does), 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
-coercions, i.e.  we always attempt disambiguation passes with fresh instances
+Motivated by this and similar examples we choose to always prefer fresh
+instances over implicit coercions, i.e.  we always attempt disambiguation
+passes with fresh instances
 and no implicit coercions before attempting passes with implicit coercions.
 
 \subsubsection{Disambiguation passes}
 \label{sec:disambpasses}
 
-According to the criteria described above in \MATITA{} we choose to perform the
-sequence of disambiguation passes depicted in Tab.~\ref{tab:disambpasses}. In
+According to the criteria described above, in \MATITA{} we perform the
+disambiguation passes depicted in Tab.~\ref{tab:disambpasses}. In
 our experience that choice gives reasonable performance and minimize the need of
 user interaction during the disambiguation.
 
@@ -1244,7 +1244,7 @@ fully supported so that mathematical glyphs can be input as such.
 \begin{figure}[!ht]
  \begin{center}
   \includegraphics[width=0.95\textwidth]{pics/matita-screenshot}
-  \caption{\MATITA{} look and feel\strut}
+  \caption{Authoring interface\strut}
   \label{fig:screenshot}
  \end{center}
 \end{figure}