one line more

practical.tex

@@ -173,18 +173,17 @@ We consider \True, \Any, and $\lnot\True$ as candidate types for
 \end{alltt}
 for which the very same types as in Table~\ref{tab:implem} are deduced.
 
-Last but not least Code~10 (which corresponds to our introductory
-Example~\ref{nest1}) illustrate the need for iterative refinement of
-type environments, as defined in Section~\ref{sec:typenv}. Indeed, has
-we have explained, a single pass analysis would deduce independently
+Last but not least Code~10 (corresponding to our introductory
+example~\eqref{nest1}) illustrates the need for iterative refinement of
+type environments, as defined in Section~\ref{sec:typenv}. As
+explained, a single pass analysis would deduce independently
 for {\tt x}
-a type \Int from the {\tt f~x} application and \Any from the {\tt g~x}
+a type \Int{} from the {\tt f\;x} application and \Any{} from the {\tt g\;x}
 application. Here by iterating a second time, the algorithm deduces
 that {\tt x} has type \Empty, that is that the first branch can never
-be selected (and our implementation warns the user accordingly). In
-hindsight, the only way for a well typed overloaded function to have
+be selected (and our implementation warns the user accordingly). In hindsight, the only way for a well-typed overloaded function to have
 type $(\Int\to\Int)\land(\Any\to\Bool)$ is to diverge when the
-argument is of type \Int (since this intersection types states that
+argument is of type \Int: since this intersection types states that
 whenever the input is \Int, {\em both\/} branches can be selected,
 yielding a result that is at the same time an integer and a Boolean.
 This is precisely reflected by the case $\Int\to\Empty$ in the result.