aboutsummaryrefslogtreecommitdiff
path: root/doc/Reference-Manual.tex
diff options
context:
space:
mode:
authormohring2004-01-06 16:52:44 +0000
committermohring2004-01-06 16:52:44 +0000
commitc1466b54d098e4e410aefacd6317bf8fa40bb63c (patch)
treee968766a88726210d0e4a8c2ed365b0366280d39 /doc/Reference-Manual.tex
parent3c94d3e2d09f6baa497aadba8f8c64bfd68a9ca9 (diff)
doc avec frames
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8469 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/Reference-Manual.tex')
-rw-r--r--doc/Reference-Manual.tex10
1 files changed, 10 insertions, 0 deletions
diff --git a/doc/Reference-Manual.tex b/doc/Reference-Manual.tex
index 2e6c458439..0b9a8cc255 100644
--- a/doc/Reference-Manual.tex
+++ b/doc/Reference-Manual.tex
@@ -10,6 +10,7 @@
\usepackage{verbatim}
\usepackage{amsmath}
\usepackage{amssymb}
+\usepackage{hevea}
% for coqide
\ifx\pdfoutput\undefined % si on est pas en pdflatex
@@ -32,13 +33,17 @@
%END LATEX
\tophtml{}
+%BEGIN LATEX
\coverpage{Reference Manual}{The Coq Development Team}
+%END LATEX
%\defaultheaders
\include{RefMan-int}% Introduction
\include{RefMan-pre}% Credits
+%BEGIN LATEX
\tableofcontents
+%END LATEX
\part{The language}
\defaultheaders
@@ -85,14 +90,19 @@
\nocite{*}
\bibliographystyle{plain}
\bibliography{biblio}
+\cutname{biblio.html}
\printindex
+\cutname{general-index.html}
\printindex[tactic]
+\cutname{tactic-index.html}
\printindex[command]
+\cutname{command-index.html}
\printindex[error]
+\cutname{error-index.html}
%BEGIN LATEX
\listoffigures