--- a/doc-src/Nitpick/nitpick.tex Tue Oct 27 15:55:36 2009 +0100
+++ b/doc-src/Nitpick/nitpick.tex Tue Oct 27 16:52:06 2009 +0100
@@ -1836,14 +1836,14 @@
\nopagebreak
{\small See also \textit{card} (\S\ref{scope-of-search}),
-\textit{coalesce\_type\_vars} (\S\ref{scope-of-search}), and \textit{verbose}
+\textit{merge\_type\_vars} (\S\ref{scope-of-search}), and \textit{verbose}
(\S\ref{output-format}).}
\opsmart{mono}{non\_box}
Specifies the default monotonicity setting to use. This can be overridden on a
per-type basis using the \textit{mono}~\qty{type} option described above.
-\opfalse{coalesce\_type\_vars}{dont\_coalesce\_type\_vars}
+\opfalse{merge\_type\_vars}{dont\_merge\_type\_vars}
Specifies whether type variables with the same sort constraints should be
merged. Setting this option to \textit{true} can reduce the number of scopes
tried and the size of the generated Kodkod formulas, but it also diminishes the
@@ -2220,7 +2220,7 @@
\nopagebreak
{\small See also \textit{auto} (\S\ref{mode-of-operation}).}
-\opt{tac\_timeout}{time}{$\mathbf{500}$ ms}
+\opt{tac\_timeout}{time}{$\mathbf{500}$\,ms}
Specifies the maximum amount of time that the \textit{auto} tactic should use
when checking a counterexample, and similarly that \textit{lexicographic\_order}
and \textit{sizechange} should use when checking whether a (co)in\-duc\-tive
@@ -2467,6 +2467,12 @@
representation of functions synthesized by Isabelle, which is an implementation
detail.
+\item[$\bullet$] Nitpick maintains a global cache of wellformedness conditions,
+which can become invalid if you change the definition of an inductive predicate
+that is registered in the cache. To clear the cache,
+run Nitpick with the \textit{tac\_timeout} option set to a new value (e.g.,
+501$\,\textit{ms}$).
+
\item[$\bullet$] Nitpick produces spurious counterexamples when invoked after a
\textbf{guess} command in a structured proof.