1.1 --- a/doc-src/Nitpick/nitpick.tex	Thu Nov 05 17:03:22 2009 +0100
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Thu Nov 05 19:06:35 2009 +0100
     1.3 @@ -2420,6 +2420,11 @@
     1.4  \kern1pt'a~\textit{list}\textrm{''}\}\ \,{*}\}$
     1.5  \postw
     1.6  
     1.7 +Inductive datatypes can be registered as coinductive datatypes, given
     1.8 +appropriate coinductive constructors. However, doing so precludes
     1.9 +the use of the inductive constructors---Nitpick will generate an error if they
    1.10 +are needed.
    1.11 +
    1.12  \section{Known Bugs and Limitations}
    1.13  \label{known-bugs-and-limitations}
    1.14  
    1.15 @@ -2460,8 +2465,7 @@
    1.16  \textit{Nitpick.register\_} functions can cause havoc if used improperly.
    1.17  
    1.18  \item[$\bullet$] Although this has never been observed, arbitrary theorem
    1.19 -morphisms could possibly confuse Nitpick and lead it to generate spurious
    1.20 -counterexamples.
    1.21 +morphisms could possibly confuse Nitpick, resulting in spurious counterexamples.
    1.22  
    1.23  \item[$\bullet$] Local definitions are not supported and result in an error.
    1.24