diff options
| -rw-r--r-- | doc/AddRefMan-pre.tex | 6 | ||||
| -rw-r--r-- | doc/Makefile | 4 | ||||
| -rw-r--r-- | doc/Reference-Manual.tex | 4 |
3 files changed, 7 insertions, 7 deletions
diff --git a/doc/AddRefMan-pre.tex b/doc/AddRefMan-pre.tex index 4e1f652f5b..5312b8fc2f 100644 --- a/doc/AddRefMan-pre.tex +++ b/doc/AddRefMan-pre.tex @@ -1,7 +1,7 @@ -%\coverpage{Addenddum to the Reference Manual}{\ } -\addcontentsline{toc}{part}{Additional documentation} +%\coverpage{Addendum to the Reference Manual}{\ } +%\addcontentsline{toc}{part}{Additional documentation} \setheaders{Presentation of the Addendum} -\section*{Presentation of the Addendum} +\chapter*{Presentation of the Addendum} Here you will find several pieces of additional documentation for the \Coq\ Reference Manual. Each of this chapters is concentrated on a diff --git a/doc/Makefile b/doc/Makefile index dd57e853bf..8ab4bf199c 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -153,8 +153,6 @@ doc-html.tar.gz: all-html - $(MKDIR) coq-docs-html rm -rf coq-docs-html/* cp Tutorial.v.html coq-docs-html/tutorial.html -# cp Changes.v.html coq-docs-html/changes.html -# cp Library.html coq-docs-html/library.html cp Reference-Manual.html coq-docs-html (cd coq-docs-html;\ htmlsplit -N -T "The Coq Proof Assistant Reference Manual"\ @@ -168,8 +166,6 @@ html-www: all-html - $(MKDIR) www rm -rf www/* cp Tutorial.v.html www/tutorial.html -# cp Changes.v.html www/changes.html -# cp Library.html www/library.html cp Reference-Manual.html www (cd www;\ htmlsplit -N -T "The Coq Proof Assistant Reference Manual"\ diff --git a/doc/Reference-Manual.tex b/doc/Reference-Manual.tex index a32b27e3fe..a46f71631b 100644 --- a/doc/Reference-Manual.tex +++ b/doc/Reference-Manual.tex @@ -65,6 +65,10 @@ \include{RefMan-uti}% utilities (gallina, do_Makefile, etc) \include{RefMan-ide}% Coq IDE +%BEGIN LATEX +\RefManCutCommand{BEGINADDENDUM=\thepage} +%END LATEX +\part{Addendum to the Reference Manual} \include{AddRefMan-pre}% \include{Cases.v}% \include{Coercion.v}% |