aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-01-06 13:51:59 +0000
committerGravatar mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-01-06 13:51:59 +0000
commitadfe3fb388239e4985b65f9864bba9ce894c29e0 (patch)
tree05e10a2e26b68b6c282db33707822868374f184b
parenta75c981d46c9483c07397035cb55bd23a65863b3 (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.tex6
-rw-r--r--doc/Makefile4
-rw-r--r--doc/Reference-Manual.tex4
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}%