doc-src/Nitpick/nitpick.tex
changeset 33556 cba22e2999d5
parent 33232 f93390060bbe
child 33557 107f3df799f6
--- 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.