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