completed disambiguation part

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index 84c98b48406b0155959e8779257e5a82ef2bc746..2a5f3fd2e01e84bb9677885a6446c727a241bc61 100644 (file)
--- a/helm/papers/matita/matita2.tex
+++ b/helm/papers/matita/matita2.tex
@@ -1041,6 +1041,16 @@ an interpretation for one instances does not constraint the choice for the
 others). For this reason we always attempt a fresh instances pass only after
 attempting a non-fresh one.
 
+\paragraph{One-shot aliases} Disambiguation aliases as seen so far are
+instance-independent. However, aliases obtained as a result of a disambiguation
+pass which uses fresh instances ought to be instance-dependent, that is: to
+ensure a term can be disambiguated in a batch fashion we may need to state that
+an \emph{i}-th instance of a symbol should be mapped to a given partially
+specified term. Instance-depend aliases are meaningful only for the term whose
+disambiguation generated it. For this reason we call them \emph{one-shot
+aliases} and \MATITA{} doesn't use it to disambiguate further terms down in the
+script.
+
 \subsubsection{Implicit coercions}
 
 Let's now consider a (rather hypothetical) theorem about derivation:
@@ -1082,19 +1092,14 @@ attempting passes with implicit coercions.
 
 \subsubsection{Disambiguation passes}
 
-Summarizing, we perform multiple disambiguation passes for each presentation
-level term and in each of them we have 3 degree of freedom: disambiguation
-aliases (mono/multi/library), operator instances (shared/fresh), and implicit
-coercions (enabled/disabled). This would lead to up to 12 different
-disambiguation passes with ordering to be decided upon. Our choice in \MATITA{}
-is depicted in Tab.~\ref{tab:disambpasses}.
-
-\TODO{spiegazione della tabella}
+According to the criteria described above in \MATITA{} we choose to perform the
+sequence of disambiguation passes depicted in Tab.~\ref{tab:disambpasses}.  In
+our experience that choice implements a good trade off among disambiguation time
+and admitted ambiguity in terms input by users.
 
-\begin{table}
- \caption{Disambiguation passes.\strut}
+\begin{table}[ht]
+ \caption{Sequence of disambiguation passes used in \MATITA.\strut}
  \label{tab:disambpasses} 
- \footnotesize
  \begin{center}
   \begin{tabular}{c|c|c|c}
    \multicolumn{1}{p{1.5cm}|}{\centering\raisebox{-1.5ex}{\textbf{Pass}}}
@@ -1113,14 +1118,6 @@ is depicted in Tab.~\ref{tab:disambpasses}.
  \end{center}
 \end{table}
 
-\TODO{alias one shot}
-
-
-
-
-
-
-
 \subsection{Patterns}
 
 serve una intro che almeno cita il widget (per i patterns) e che fa