1.1 --- a/doc-src/Nitpick/nitpick.tex	Mon Feb 21 10:44:19 2011 +0100
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Mon Feb 21 11:50:31 2011 +0100
     1.3 @@ -2108,26 +2108,18 @@
     1.4  per-type basis using the \textit{box}~\qty{type} option described above.
     1.5  
     1.6  \opargboolorsmart{finitize}{type}{dont\_finitize}
     1.7 -Specifies whether Nitpick should attempt to finitize an infinite ``shallow
     1.8 -datatype'' (an infinite datatype whose constructors don't appear in the
     1.9 -problem). The option can then take the following values:
    1.10 -
    1.11 -\begin{enum}
    1.12 -\item[$\bullet$] \textbf{\textit{false}:} Don't attempt to finitize the type.
    1.13 -\item[$\bullet$] \textbf{\textit{true}} or \textbf{\textit{smart}:} Finitize the
    1.14 -type wherever possible.
    1.15 -\end{enum}
    1.16 -
    1.17 -The semantics of the option is somewhat different for infinite shallow
    1.18 -datatypes:
    1.19 +Specifies whether Nitpick should attempt to finitize an infinite datatype. The
    1.20 +option can then take the following values:
    1.21  
    1.22  \begin{enum}
    1.23  \item[$\bullet$] \textbf{\textit{true}:} Finitize the datatype. Since this is
    1.24  unsound, counterexamples generated under these conditions are tagged as ``quasi
    1.25  genuine.''
    1.26  \item[$\bullet$] \textbf{\textit{false}:} Don't attempt to finitize the datatype.
    1.27 -\item[$\bullet$] \textbf{\textit{smart}:} Perform a monotonicity analysis to
    1.28 -detect whether the datatype can be soundly finitized before finitizing it.
    1.29 +\item[$\bullet$] \textbf{\textit{smart}:}
    1.30 +If the datatype's constructors don't appear in the problem, perform a
    1.31 +monotonicity analysis to detect whether the datatype can be soundly finitized;
    1.32 +otherwise, don't finitize it.
    1.33  \end{enum}
    1.34  
    1.35  \nopagebreak