diff -r 45c33e97cb86 -r e1e77265fb1d doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Thu Nov 05 17:03:22 2009 +0100
+++ b/doc-src/Nitpick/nitpick.tex	Thu Nov 05 19:06:35 2009 +0100
@@ -2420,6 +2420,11 @@
 \kern1pt'a~\textit{list}\textrm{''}\}\ \,{*}\}$
 \postw
 
+Inductive datatypes can be registered as coinductive datatypes, given
+appropriate coinductive constructors. However, doing so precludes
+the use of the inductive constructors---Nitpick will generate an error if they
+are needed.
+
 \section{Known Bugs and Limitations}
 \label{known-bugs-and-limitations}
 
@@ -2460,8 +2465,7 @@
 \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.
+morphisms could possibly confuse Nitpick, resulting in spurious counterexamples.
 
 \item[$\bullet$] Local definitions are not supported and result in an error.