--- a/doc-src/Nitpick/nitpick.tex Mon Feb 21 10:44:19 2011 +0100
+++ b/doc-src/Nitpick/nitpick.tex Mon Feb 21 11:50:31 2011 +0100
@@ -2108,26 +2108,18 @@
per-type basis using the \textit{box}~\qty{type} option described above.
\opargboolorsmart{finitize}{type}{dont\_finitize}
-Specifies whether Nitpick should attempt to finitize an infinite ``shallow
-datatype'' (an infinite datatype whose constructors don't appear in the
-problem). The option can then take the following values:
-
-\begin{enum}
-\item[$\bullet$] \textbf{\textit{false}:} Don't attempt to finitize the type.
-\item[$\bullet$] \textbf{\textit{true}} or \textbf{\textit{smart}:} Finitize the
-type wherever possible.
-\end{enum}
-
-The semantics of the option is somewhat different for infinite shallow
-datatypes:
+Specifies whether Nitpick should attempt to finitize an infinite datatype. The
+option can then take the following values:
\begin{enum}
\item[$\bullet$] \textbf{\textit{true}:} Finitize the datatype. Since this is
unsound, counterexamples generated under these conditions are tagged as ``quasi
genuine.''
\item[$\bullet$] \textbf{\textit{false}:} Don't attempt to finitize the datatype.
-\item[$\bullet$] \textbf{\textit{smart}:} Perform a monotonicity analysis to
-detect whether the datatype can be soundly finitized before finitizing it.
+\item[$\bullet$] \textbf{\textit{smart}:}
+If the datatype's constructors don't appear in the problem, perform a
+monotonicity analysis to detect whether the datatype can be soundly finitized;
+otherwise, don't finitize it.
\end{enum}
\nopagebreak