diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-07-29 23:40:58 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-07-29 23:40:58 +0200 |
| commit | a96ea9283b0eb9d4259933e673001bab5515e623 (patch) | |
| tree | 9355a8635ae6f342afa5068fff5c1272b3c0d29c | |
| parent | 7a470793d2a8f0cecf9d552ee8a24af025a3475c (diff) | |
Drop paragraph mentioning Addendum as separate doc.
As suggested by @herbelin.
| -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{}. |