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

diff --git a/doc/refman/headers.hva b/doc/refman/headers.hva
new file mode 100644
index 0000000000..d0675ec178
--- /dev/null
+++ b/doc/refman/headers.hva
@@ -0,0 +1,72 @@
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% File headers.hva
+% Hevea version of headers.sty
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Commands for indexes
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\usepackage{index}
+\makeindex
+\newindex{tactic}{tacidx}{tacind}{%
+\protect\addcontentsline{toc}{chapter}{Tactics Index}Tactics Index}
+
+\newindex{command}{comidx}{comind}{%
+\protect\addcontentsline{toc}{chapter}{Vernacular Commands Index}%
+Vernacular Commands Index}
+
+\newindex{error}{erridx}{errind}{%
+\protect\addcontentsline{toc}{chapter}{Index of Error Messages}Index of Error Messages}
+
+\renewindex{default}{idx}{ind}{%
+\protect\addcontentsline{toc}{chapter}{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}}}
+
+% 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.
+\newcommand{\@indexlabel}{}
+\let\oldchapter=\chapter
+\let\oldsection=\section
+\let\oldsubsection=\subsection
+\let\oldsubsubsection=\subsubsection
+\let\oldparagraph=\paragraph
+\let\oldsubparagraph=\subparagraph
+\renewcommand{\chapter}[1]{\oldchapter{#1}\let\@indexlabel=\@currentlabel}
+\renewcommand{\section}[1]{\oldsection{#1}\let\@indexlabel=\@currentlabel}
+\renewcommand{\subsection}[1]{\oldsubsection{#1}\let\@indexlabel=\@currentlabel}
+\renewcommand{\subsubsection}[1]{\oldsubsubsection{#1}\let\@indexlabel=\@currentlabel}
+\renewcommand{\paragraph}[1]{\oldparagraph{#1}\let\@indexlabel=\@currentlabel}
+\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
+\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}  % 3 \bigskip's that were here originally
+						    % may be good for LaTeX but too much for HTML    
+\newcommand{\atableofcontents}{}
+\newcommand{\achapter}[1]{\chapter{#1}}
+\newcommand{\asection}{\section}
+\newcommand{\asubsection}{\subsection}
+\newcommand{\asubsubsection}{\subsubsection}