diff options
author | mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-01-06 13:51:59 +0000 |
---|---|---|
committer | mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-01-06 13:51:59 +0000 |
commit | adfe3fb388239e4985b65f9864bba9ce894c29e0 (patch) | |
tree | 05e10a2e26b68b6c282db33707822868374f184b | |
parent | a75c981d46c9483c07397035cb55bd23a65863b3 (diff) |
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8467 85f007b7-540e-0410-9357-904b9bb8a0f7
-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 4e1f652f5..5312b8fc2 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 dd57e853b..8ab4bf199 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 a32b27e3f..a46f71631 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}% |