# HG changeset patch
# User blanchet
# Date 1432912670 -7200
# Node ID 72364a93bcb53a260282ca190cff02fc57c68e02
# Parent  f7e406aba90d7e8e86df1fb1fa9d70802f42ba56
document Nitpick issue

diff -r f7e406aba90d -r 72364a93bcb5 src/Doc/Nitpick/document/root.tex
--- a/src/Doc/Nitpick/document/root.tex	Fri May 29 14:35:59 2015 +0100
+++ b/src/Doc/Nitpick/document/root.tex	Fri May 29 17:17:50 2015 +0200
@@ -2773,11 +2773,15 @@
 \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} and
+\item[\labelitemi] Datatypes defined using \textbf{datatype} 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] Types that are registered with several distinct sets of
+constructors, including \textit{enat} if the \textit{Coinductive} entry of
+the \textit{Archive of Formal Proofs} is loaded, can confuse Nitpick.
+
 \item[\labelitemi] The \textit{nitpick\_xxx} attributes and the
 \textit{Nitpick\_xxx.register\_yyy} functions can cause havoc if used
 improperly.