doc-src/Nitpick/nitpick.tex
changeset 33570 da0fea4b6e36
parent 33555 75ce0f60617a
child 33572 e1e77265fb1d
     1.1 --- a/doc-src/Nitpick/nitpick.tex	Thu Nov 05 11:58:36 2009 +0100
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Thu Nov 05 17:00:28 2009 +0100
     1.3 @@ -2459,6 +2459,10 @@
     1.4  \item[$\bullet$] The \textit{nitpick\_} attributes and the
     1.5  \textit{Nitpick.register\_} functions can cause havoc if used improperly.
     1.6  
     1.7 +\item[$\bullet$] Although this has never been observed, arbitrary theorem
     1.8 +morphisms could possibly confuse Nitpick and lead it to generate spurious
     1.9 +counterexamples.
    1.10 +
    1.11  \item[$\bullet$] Local definitions are not supported and result in an error.
    1.12  
    1.13  \item[$\bullet$] All constants and types whose names start with