# HG changeset patch
# User blanchet
# Date 1257436828 -3600
# Node ID da0fea4b6e369e325abda9906b01e66fa9767aae
# Parent  0c3ba1e010d2cc22fc9332c8a9d65173b93ab012
don't promise too much in the Nitpick manual

diff -r 0c3ba1e010d2 -r da0fea4b6e36 doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Thu Nov 05 11:58:36 2009 +0100
+++ b/doc-src/Nitpick/nitpick.tex	Thu Nov 05 17:00:28 2009 +0100
@@ -2459,6 +2459,10 @@
 \item[$\bullet$] The \textit{nitpick\_} attributes and the
 \textit{Nitpick.register\_} functions can cause havoc if used improperly.
 
+\item[$\bullet$] Although this has never been observed, arbitrary theorem
+morphisms could possibly confuse Nitpick and lead it to generate spurious
+counterexamples.
+
 \item[$\bullet$] Local definitions are not supported and result in an error.
 
 \item[$\bullet$] All constants and types whose names start with