Cleaned doc/common/title.tex file. Increased the space under headers

in the reference manual.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9758 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 27 insertions, 16 deletions

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 8fdb8d8df7..f0db1a0fb2 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -251,7 +251,7 @@ Definition not (b:bool) :=
   end.
 \end{coq_example}
 
-can be alternatively written
+\noindent can be alternatively written
 
 \begin{coq_eval}
 Reset not.
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index 0beabc991f..1ea680741c 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -589,6 +589,7 @@ Coq-Club mailing list and bug-tracker systems, especially user groups
 from INRIA Rocquencourt, Radbout University, University of
 Pennsylvania and Yale University.
 
+\enlargethispage{\baselineskip}
 \begin{flushright}
 Palaiseau, July 2006\\
 Hugo Herbelin
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 8331defbb5..63f61ea8bb 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3299,14 +3299,14 @@ The tactic {\tt exists (n // m)} did not fail. The hole was solved by
 The {\tt Scheme} command is a high-level tool for generating
 automatically (possibly mutual) induction principles for given types
 and sorts.  Its syntax follows the schema:
-\begin{tabbing}
+\begin{quote}
 {\tt Scheme {\ident$_1$} := Induction for \ident'$_1$ Sort {\sort$_1$} \\
   with\\
-  \mbox{}\hspace{0.1cm} \dots\ \\
+  \mbox{}\hspace{0.1cm} \dots\\
         with {\ident$_m$} := Induction for {\ident'$_m$} Sort
         {\sort$_m$}}
-\end{tabbing}
-\ident'$_1$ \dots\ \ident'$_m$ are different inductive type
+\end{quote}
+where \ident'$_1$ \dots\ \ident'$_m$ are different inductive type
 identifiers belonging to the same package of mutual inductive
 definitions. This command generates {\ident$_1$}\dots{} {\ident$_m$}
 to be mutually recursive definitions. Each term {\ident$_i$} proves a
@@ -3353,14 +3353,14 @@ The {\tt Functional Scheme} command is a high-level experimental
 tool for generating automatically induction principles
 corresponding to (possibly mutually recursive) functions.  Its
 syntax follows the schema:
-\begin{tabbing}
+\begin{quote}
 {\tt Functional Scheme {\ident$_1$} := Induction for \ident'$_1$ Sort {\sort$_1$} \\
   with\\
   \mbox{}\hspace{0.1cm} \dots\ \\
         with {\ident$_m$} := Induction for {\ident'$_m$} Sort
         {\sort$_m$}}
-\end{tabbing}  
-\ident'$_1$ \dots\ \ident'$_m$ are different mutually defined function
+\end{quote}  
+where \ident'$_1$ \dots\ \ident'$_m$ are different mutually defined function
 names (they must be in the same order as when they were defined).
 This command generates the induction principles
 \ident$_1$\dots\ident$_m$, following the recursive structure and case
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index 34399196be..62c640b23f 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -15,6 +15,7 @@
 \usepackage{alltt}
 \usepackage{hevea}
 \usepackage{ifpdf}
+\usepackage[headings]{fullpage}
 \usepackage{headers} % in this directory
 
 % for coqide
@@ -30,20 +31,29 @@
 \input{../common/version.tex}
 \input{../common/macros.tex}% extension .tex pour htmlgen
 \input{../common/title.tex}% extension .tex pour htmlgen
-
+%\input{headers}
+
+\usepackage[linktocpage,colorlinks]{hyperref}
+% The manual advises to load hyperref package last to be able to redefine
+% necessary commands.
+% The above should work for both latex and pdflatex. Even if PDF is produced
+% through DVI and PS using dvips and ps2pdf, hyperlinks should still work.
+% linktocpage option makes page numbers, not section names, to be links in
+% the table of contents.
+% colorlinks option colors the links instead of using boxes.
 \begin{document}
 %BEGIN LATEX
 \sloppy\hbadness=5000
 %END LATEX
 
-\tophtml{}
 %BEGIN LATEX
-\coverpage{Reference Manual}{The Coq Development Team}
-  {This material may be distributed only subject to the terms and
-   conditions set forth in the Open Publication License, v1.0 or later
-   (the latest version is presently available at
-   \ahrefurl{http://www.opencontent.org/openpub}).
-   Options A and B of the licence are {\em not} elected.}
+\coverpage{Reference Manual}
+{The Coq Development Team}
+{This material may be distributed only subject to the terms and
+conditions set forth in the Open Publication License, v1.0 or later
+(the latest version is presently available at
+\url{http://www.opencontent.org/openpub}).
+Options A and B of the licence are {\em not} elected.}
 %END LATEX
 
 %\defaultheaders