diff options
| -rw-r--r-- | doc/refman/RefMan-int.tex | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/doc/refman/RefMan-int.tex b/doc/refman/RefMan-int.tex index 7d4c55d0c..eca3efcdd 100644 --- a/doc/refman/RefMan-int.tex +++ b/doc/refman/RefMan-int.tex @@ -125,15 +125,6 @@ documents: user can read also the tutorial on recursive types (document {\tt RecTutorial.ps}). -\item[Addendum] The fifth part (the Addendum) of the Reference Manual - is distributed as a separate document. It contains more - detailed documentation and examples about some specific aspects of the - system that may interest only certain users. It shares the indexes, - the page numbers and - the bibliography with the Reference Manual. If you see in one of the - indexes a page number that is outside the Reference Manual, it refers - to the Addendum. - \item[Installation] A text file INSTALL that comes with the sources explains how to install \Coq{}. |