# HG changeset patch
# User blanchet
# Date 1381742054 -7200
# Node ID 67a601c6c301b104f95b6b5f5f2fb7a270a17339
# Parent  0e4994ae761911dc36ecd0cec51d8ea7790845aa
added Nitpick limitations to docs

diff -r 0e4994ae7619 -r 67a601c6c301 src/Doc/Nitpick/document/root.tex
--- a/src/Doc/Nitpick/document/root.tex	Mon Oct 14 11:07:59 2013 +0200
+++ b/src/Doc/Nitpick/document/root.tex	Mon Oct 14 11:14:14 2013 +0200
@@ -2794,11 +2794,12 @@
 \subsection{Registering Coinductive Datatypes}
 \label{registering-coinductive-datatypes}
 
+Coinductive datatypes defined using the \textbf{codatatype} command that do not
+involve nested recursion through non-codatatypes are supported by Nitpick.
 If you have defined a custom coinductive datatype, you can tell Nitpick about
-it, so that it can use an efficient Kodkod axiomatization similar to the one it
-uses for lazy lists. The interface for registering and unregistering coinductive
-datatypes consists of the following pair of functions defined in the
-\textit{Nitpick\_HOL} structure:
+it, so that it can use an efficient Kodkod axiomatization. The interface for
+registering and unregistering coinductive datatypes consists of the following
+pair of functions defined in the \textit{Nitpick\_HOL} structure:
 
 \prew
 $\textbf{val}\,~\textit{register\_codatatype\/} : {}$ \\
@@ -2886,6 +2887,12 @@
 \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 supported.
+
 \item[\labelitemi] The \textit{nitpick\_xxx} attributes and the
 \textit{Nitpick\_xxx.register\_yyy} functions can cause havoc if used
 improperly.