# HG changeset patch
# User blanchet
# Date 1393955837 -3600
# Node ID 39cc8409373f18c992e7caf4f2ea6eb71dc2d479
# Parent  8c6d49dd8ae1902b40cef20f491c51af2f16ecd0
updated docs

diff -r 8c6d49dd8ae1 -r 39cc8409373f src/Doc/Nitpick/document/root.tex
--- a/src/Doc/Nitpick/document/root.tex	Tue Mar 04 18:57:17 2014 +0100
+++ b/src/Doc/Nitpick/document/root.tex	Tue Mar 04 18:57:17 2014 +0100
@@ -2765,21 +2765,13 @@
 ignored. Again, such nonconservative extensions are generally considered bad
 style.
 
-\item[\labelitemi] Nitpick maintains a global cache of wellfoundedness 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.,
-$0.51$).
-
 \item[\labelitemi] Nitpick produces spurious counterexamples when invoked after a
 \textbf{guess} command in a structured proof.
 
-\item[\labelitemi] Datatypes defined using \textbf{datatype\_new} are not
-supported.
-
-\item[\labelitemi] Codatatypes defined using \textbf{codatatype} that
-involve nested recursion through non-codatatypes are not properly supported
-and may result in spurious counterexamples.
+\item[\labelitemi] Datatypes defined using \textbf{datatype\_new} and
+codatatypes defined using \textbf{codatatype} that involve nested (co)recursion
+through non-(co)datatypes are not properly supported and may result in spurious
+counterexamples.
 
 \item[\labelitemi] The \textit{nitpick\_xxx} attributes and the
 \textit{Nitpick\_xxx.register\_yyy} functions can cause havoc if used