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, 0 insertions, 131 deletions

diff --git a/doc/refman/headers.tex b/doc/refman/headers.tex
deleted file mode 100644
index bb84fb4796..0000000000
--- a/doc/refman/headers.tex
+++ /dev/null
@@ -1,131 +0,0 @@
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% File title.tex
-% Pretty Headers
-% And commands for multiple indexes
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\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}}
-%BEGIN LATEX
-\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}
-%END LATEX
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% 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}}}
-\makeatother
-
-% The following code creates another command \@indexlabel, which,
-% along with Hevea's \@currentlabel serves to store the current values
-% of counters. However, \@currentlabel keeps the value of counters
-% incremented by \refstepcounter (see the definition of
-% \refstepcounter in latexcommon.hva), which includes chapter and
-% section counters, as well as theorems, \items, etc. On the other
-% hand, \@indexlabel keeps only the values of sectioning counters.
-% This is done by redefining the sectioning commands.
-%HEVEA \newcommand{\@indexlabel}{}
-%HEVEA \let\oldchapter=\chapter
-%HEVEA \let\oldsection=\section
-%HEVEA \let\oldsubsection=\subsection
-%HEVEA \let\oldsubsubsection=\subsubsection
-%HEVEA \let\oldparagraph=\paragraph
-%HEVEA \let\oldsubparagraph=\subparagraph
-%HEVEA \renewcommand{\chapter}[1]{\oldchapter{#1}\let\@indexlabel=\@currentlabel}
-%HEVEA \renewcommand{\section}[1]{\oldsection{#1}\let\@indexlabel=\@currentlabel}
-%HEVEA \renewcommand{\subsection}[1]{\oldsubsection{#1}\let\@indexlabel=\@currentlabel}
-%HEVEA \renewcommand{\subsubsection}[1]{\oldsubsubsection{#1}\let\@indexlabel=\@currentlabel}
-%HEVEA \renewcommand{\paragraph}[1]{\oldparagraph{#1}\let\@indexlabel=\@currentlabel}
-%HEVEA \renewcommand{\subparagraph}[1]{\oldsubparagraph{#1}\let\@indexlabel=\@currentlabel}
-% The only difference of the following command with the original one
-% defined in index.hva is that the latter uses \@currentlabel instead
-% of \@indexlabel
-% Also, for some reason, the following command produces an error if
-% not given on one line. Need to submit to Hevea developers.
-%HEVEA \renewcommand{\index}[2][default]{\if@refs\sbox{\@indexbox}{\@indexwrite[#1]{#2}{\@indexlabel}}\@locname{\usebox{\@indexbox}}{}\fi}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% For the Addendum table of contents
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\newcommand{\aauthor}[1]{{\LARGE \bf #1} \bigskip \bigskip \bigskip}
-\makeatletter
-%BEGIN LATEX
-\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}}
-%END LATEX
-%HEVEA \newcommand{\atableofcontents}{}
-%HEVEA \newcommand{\achapter}[1]{\chapter{#1}}
-%HEVEA \newcommand{\asection}{\section}
-%HEVEA \newcommand{\asubsection}{\subsection}
-%HEVEA \newcommand{\asubsubsection}{\subsubsection}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% Reference-Manual.sh is generated to cut the Postscript
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%\@starttoc{sh}
-%BEGIN LATEX
-\newwrite\RefManCut@out%
-\immediate\openout\RefManCut@out\jobname.sh
-\newcommand{\RefManCutCommand}[1]{%
-\immediate\write\RefManCut@out{#1}}
-\newcommand{\RefManCutClose}{%
-\immediate\closeout\RefManCut@out}
-%END LATEX
-
-
-
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "Reference-Manual"
-%%% End: