Eliminated warning messages from Hevea. Most warning messages were

from commands about headers; where appropriate, surrounded those by
%BEGIN LATEX ... %END LATEX. Removed some \newcommands that were
ignored. Removed redefinitions of \land, \lor, \lnot: there are nicely
handled by Hevea.

Split headers.tex file into headers.sty (for LaTeX) and headers.hva
(for Hevea). This allowed removing comments like %BEGIN LATEX and %HEVEA
and also commands \makeatletter, \makeatother.


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

1 files changed, 87 insertions, 0 deletions

diff --git a/doc/refman/headers.sty b/doc/refman/headers.sty
new file mode 100644
index 0000000000..bc5f5c6c3f
--- /dev/null
+++ b/doc/refman/headers.sty
@@ -0,0 +1,87 @@
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% File headers.sty
+% Commands for pretty headers, multiple indexes, and the appendix.
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\usepackage{fancyhdr}
+
+\setlength{\headheight}{14pt}
+
+\pagestyle{fancyplain}
+
+\newcommand{\coqfooter}{\tiny Coq Reference Manual, V\coqversion{}, \today}
+
+\cfoot{}
+\lfoot[{\coqfooter}]{}
+\rfoot[]{{\coqfooter}}
+
+\newcommand{\setheaders}[1]{\rhead[\fancyplain{}{\textbf{#1}}]{\fancyplain{}{\thepage}}\lhead[\fancyplain{}{\thepage}]{\fancyplain{}{\textbf{#1}}}}
+\newcommand{\defaultheaders}{\rhead[\fancyplain{}{\leftmark}]{\fancyplain{}{\thepage}}\lhead[\fancyplain{}{\thepage}]{\fancyplain{}{\rightmark}}}
+
+\renewcommand{\chaptermark}[1]{\markboth{{\bf \thechapter~#1}}{}}
+\renewcommand{\sectionmark}[1]{\markright{\thesection~#1}}
+\renewcommand{\contentsname}{%
+\protect\setheaders{Table of contents}Table of contents}
+\renewcommand{\bibname}{\protect\setheaders{Bibliography}%
+\protect\RefManCutCommand{BEGINBIBLIO=\thepage}%
+\protect\addcontentsline{toc}{chapter}{Bibliography}Bibliography}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Commands for indexes
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\usepackage{index}
+\makeindex
+\newindex{tactic}{tacidx}{tacind}{%
+\protect\setheaders{Tactics Index}%
+\protect\addcontentsline{toc}{chapter}{Tactics Index}Tactics Index}
+
+\newindex{command}{comidx}{comind}{%
+\protect\setheaders{Vernacular Commands Index}%
+\protect\addcontentsline{toc}{chapter}{Vernacular Commands Index}%
+Vernacular Commands Index}
+
+\newindex{error}{erridx}{errind}{%
+\protect\setheaders{Index of Error Messages}%
+\protect\addcontentsline{toc}{chapter}{Index of Error Messages}Index of Error Messages}
+
+\renewindex{default}{idx}{ind}{%
+\protect\addcontentsline{toc}{chapter}{Global Index}%
+\protect\setheaders{Global Index}Global Index}
+
+\newcommand{\tacindex}[1]{%
+\index{#1@\texttt{#1}}\index[tactic]{#1@\texttt{#1}}}
+\newcommand{\comindex}[1]{%
+\index{#1@\texttt{#1}}\index[command]{#1@\texttt{#1}}}
+\newcommand{\errindex}[1]{\texttt{#1}\index[error]{#1}}
+\newcommand{\errindexbis}[2]{\texttt{#1}\index[error]{#2}}
+\newcommand{\ttindex}[1]{\index{#1@\texttt{#1}}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% For the Addendum table of contents
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\newcommand{\aauthor}[1]{{\LARGE \bf #1} \bigskip \bigskip \bigskip}
+\newcommand{\atableofcontents}{\section*{Contents}\@starttoc{atoc}}
+\newcommand{\achapter}[1]{
+  \chapter{#1}\addcontentsline{atoc}{chapter}{#1}}
+\newcommand{\asection}[1]{
+  \section{#1}\addcontentsline{atoc}{section}{#1}}
+\newcommand{\asubsection}[1]{
+  \subsection{#1}\addcontentsline{atoc}{subsection}{#1}}
+\newcommand{\asubsubsection}[1]{
+  \subsubsection{#1}\addcontentsline{atoc}{subsubsection}{#1}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Reference-Manual.sh is generated to cut the Postscript
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%\@starttoc{sh}
+\newwrite\RefManCut@out%
+\immediate\openout\RefManCut@out\jobname.sh
+\newcommand{\RefManCutCommand}[1]{%
+\immediate\write\RefManCut@out{#1}}
+\newcommand{\RefManCutClose}{%
+\immediate\closeout\RefManCut@out}
+
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "Reference-Manual"
+%%% End: