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

10 files changed, 118 insertions, 79 deletions

diff --git a/doc/refman/AddRefMan-pre.tex b/doc/refman/AddRefMan-pre.tex
index 5312b8fc2..15776690c 100644
--- a/doc/refman/AddRefMan-pre.tex
+++ b/doc/refman/AddRefMan-pre.tex
@@ -1,6 +1,8 @@
 %\coverpage{Addendum to the Reference Manual}{\ }
 %\addcontentsline{toc}{part}{Additional documentation}
+%BEGIN LATEX
 \setheaders{Presentation of the Addendum}
+%END LATEX
 \chapter*{Presentation of the Addendum}
 
 Here you will find several pieces of additional documentation for the
diff --git a/doc/refman/Cases.tex b/doc/refman/Cases.tex
index c8eb76c27..345608c6f 100644
--- a/doc/refman/Cases.tex
+++ b/doc/refman/Cases.tex
@@ -1,4 +1,7 @@
-\achapter{Extended pattern-matching}\defaultheaders
+\achapter{Extended pattern-matching}
+%BEGIN LATEX
+\defaultheaders
+%END LATEX
 \aauthor{Cristina Cornes and Hugo Herbelin}
 
 \label{Mult-match-full}
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index f66953b8e..f9dee72ed 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -598,7 +598,8 @@ Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false)
 
 The second subcase is only relevant for annotated inductive types such
 as the equality predicate (see section~\ref{Equality}), the order
-predicate on natural numbers (see section~\ref{le}) or the type of
+predicate on natural numbers % (see section~\ref{le}) % undefined reference
+or the type of
 lists of a given length (see section~\ref{listn}). In this configuration,
 the type of each branch can depend on the type dependencies specific
 to the branch and the whole pattern-matching expression has a type
diff --git a/doc/refman/RefMan-int.tex b/doc/refman/RefMan-int.tex
index b1f4b26b8..c93d7217f 100644
--- a/doc/refman/RefMan-int.tex
+++ b/doc/refman/RefMan-int.tex
@@ -1,4 +1,6 @@
+%BEGIN LATEX
 \setheaders{Introduction}
+%END LATEX
 \chapter*{Introduction}
 
 This document is the Reference Manual of version \coqversion{} of the \Coq\ 
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index cac79625a..0beabc991 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -1,4 +1,6 @@
+%BEGIN LATEX
 \setheaders{Credits}
+%END LATEX
 \chapter*{Credits}
 %\addcontentsline{toc}{section}{Credits}
 
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index 134641596..34399196b 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -1,9 +1,9 @@
-\RequirePackage{ifpdf}
-\ifpdf
-  \documentclass[11pt,a4paper,pdftex]{book}
-\else
+%\RequirePackage{ifpdf}
+%\ifpdf
+%  \documentclass[11pt,a4paper,pdftex]{book}
+%\else
   \documentclass[11pt,a4paper]{book}
-\fi
+%\fi
 
 \usepackage[latin1]{inputenc}
 \usepackage[T1]{fontenc}
@@ -14,8 +14,8 @@
 \usepackage{amssymb}
 \usepackage{alltt}
 \usepackage{hevea}
-
 \usepackage{ifpdf}
+\usepackage{headers} % in this directory
 
 % for coqide
 \ifpdf   % si on est pas en pdflatex
@@ -25,12 +25,11 @@
 \fi
 
 
-%\includeonly{RefMan-gal.v,RefMan-ltac.v,RefMan-lib.v,Cases.v}
+%\includeonly{Setoid}
 
 \input{../common/version.tex}
 \input{../common/macros.tex}% extension .tex pour htmlgen
 \input{../common/title.tex}% extension .tex pour htmlgen
-\input{./headers.tex}% extension .tex pour htmlgen
 
 \begin{document}
 %BEGIN LATEX
@@ -56,7 +55,9 @@
 %END LATEX
 
 \part{The language}
+%BEGIN LATEX
 \defaultheaders
+%END LATEX
 \include{RefMan-gal.v}% Gallina
 \include{RefMan-ext.v}% Gallina extensions
 \include{RefMan-lib.v}% The coq library
diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex
index 64aefee1f..9063591b6 100644
--- a/doc/refman/Setoid.tex
+++ b/doc/refman/Setoid.tex
@@ -139,13 +139,13 @@ A parametric relation
 can be declared with the following command
 
 \comindex{Add Relation}
-\begin{verse}
+\begin{quote}
   \texttt{Add Relation} \textit{A Aeq}\\
   ~\zeroone{\texttt{reflexivity proved by} \textit{refl}}\\
   ~\zeroone{\texttt{symmetry proved by} \textit{sym}}\\
   ~\zeroone{\texttt{transitivity proved by} \textit{trans}}\\
   \texttt{~as} \textit{id}.
-\end{verse}
+\end{quote}
 after having required the \texttt{Setoid} module with the
 \texttt{Require Setoid} command.
 
@@ -182,14 +182,14 @@ that are syntactic compositions of parametric morphism instances declared with
 the following command.
 
 \comindex{Add Morphism}
-\begin{verse}
+\begin{quote}
   \texttt{Add Morphism} \textit{f}\\
   \texttt{~with signature} \textit{sig}\\
   \texttt{~as id}.\\
   \texttt{Proof}\\
   ~\ldots\\
   \texttt{Qed}
-\end{verse}
+\end{quote}
 
 The command declares \textit{f} as a parametric morphism of signature
 \textit{sig}. The identifier \textit{id} gives a unique name to the morphism
@@ -361,12 +361,12 @@ set of alternative new goals. To force one particular choice, the user
 can switch to the following alternative syntax for rewriting:
 
 \comindex{setoid\_rewrite}
-\begin{verse}
+\begin{quote}
   \texttt{setoid\_rewrite} \zeroone{\textit{orientation}} \textit{term}
   \zeroone{\texttt{in} \textit{ident}}\\
   \texttt{~generate side conditions}
   \textit{term}$_1$ \ldots \textit{term}$_n$\\
-\end{verse}
+\end{quote}
 Up to the \texttt{generate side conditions} part, the syntax is 
 equivalent to the
 one of the \texttt{rewrite} tactic. Additionally, the user can specify a list
@@ -460,41 +460,41 @@ the prefixed tactics it is possible to pass additional arguments such as
 \texttt{generate side conditions} or \texttt{using relation}.
 
 \comindex{setoid\_reflexivity}
-\begin{verse}
+\begin{quote}
   \texttt{setoid\_reflexivity}
-\end{verse}
+\end{quote}
 
 \comindex{setoid\_symmetry}
-\begin{verse}
+\begin{quote}
   \texttt{setoid\_symmetry}
   \zeroone{\texttt{in} \textit{ident}}\\
-\end{verse}
+\end{quote}
 
 \comindex{setoid\_transitivity}
-\begin{verse}
+\begin{quote}
   \texttt{setoid\_transitivity}
-\end{verse}
+\end{quote}
 
 \comindex{setoid\_rewrite}
-\begin{verse}
+\begin{quote}
   \texttt{setoid\_rewrite} \zeroone{\textit{orientation}} \textit{term}\\
   ~\zeroone{\texttt{in} \textit{ident}}\\
   ~\zeroone{\texttt{generate side conditions}
   \textit{term}$_1$ \ldots \textit{term}$_n$}\\
-\end{verse}
+\end{quote}
 
 The \texttt{generate side conditions} argument cannot be passed to the
 unprefixed form.
 
 \comindex{setoid\_replace}
-\begin{verse}
+\begin{quote}
   \texttt{setoid\_replace} \textit{term} \texttt{with} \textit{term}
   ~\zeroone{\texttt{in} \textit{ident}}\\
   ~\zeroone{\texttt{using relation} \textit{term}}\\
   ~\zeroone{\texttt{generate side conditions}
   \textit{term}$_1$ \ldots \textit{term}$_n$}\\
   ~\zeroone{\texttt{by} \textit{tactic}}
-\end{verse}
+\end{quote}
 
 The  \texttt{generate  side  conditions} and  \texttt{using  relation}
 arguments cannot be passed to the unprefixed form. The latter argument
@@ -521,9 +521,9 @@ Due to backward compatibility reasons, the following syntax for the
 declaration of setoids and morphisms is also accepted.
 
 \comindex{Add Setoid}
-\begin{verse}
+\begin{quote}
   \texttt{Add Setoid} \textit{A Aeq ST} \texttt{as} \textit{ident}
-\end{verse}
+\end{quote}
 where \textit{Aeq} is a congruence relation without parameters,
 \textit{A} is its carrier and \textit{ST} is an object of type
 \verb|(Setoid_Theory A Aeq)| (i.e. a record packing together the reflexivity,
@@ -531,12 +531,12 @@ symmetry and transitivity lemmas). Notice that the syntax is not completely
 backward compatible since the identifier was not required.
 
 \comindex{Add Morphism}
-\begin{verse}
+\begin{quote}
   \texttt{Add Morphism} \textit{ f }:\textit{ ident}.\\
   Proof.\\
   \ldots\\
   Qed.
-\end{verse}
+\end{quote}
 
 The latter command is restricted to the declaration of morphisms without
 parameters. It is not fully backward compatible since the property the user
diff --git a/doc/refman/coqdoc.tex b/doc/refman/coqdoc.tex
index f2630da07..48e91fcd2 100644
--- a/doc/refman/coqdoc.tex
+++ b/doc/refman/coqdoc.tex
@@ -6,9 +6,9 @@
 \newcommand{\texmacs}{\TeX{}macs}
 \newcommand{\monurl}[1]{#1}
 %HEVEA\renewcommand{\monurl}[1]{\ahref{#1}{#1}}
-%HEVEA\newcommand{\lnot}{not}
-%HEVEA\newcommand{\lor}{or}
-%HEVEA\newcommand{\land}{\&}
+%\newcommand{\lnot}{not} % Hevea handles these symbols nicely
+%\newcommand{\lor}{or}
+%\newcommand{\land}{\&}
 %%% attention : -- dans un argument de \texttt est affiché comme un
 %%% seul - d'où l'utilisation de la macro suivante
 \newcommand{\mm}{\symbol{45}\symbol{45}}
diff --git a/doc/refman/headers.hva b/doc/refman/headers.hva
new file mode 100644
index 000000000..d0675ec17
--- /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}
diff --git a/doc/refman/headers.tex b/doc/refman/headers.sty
index bb84fb479..bc5f5c6c3 100644
--- a/doc/refman/headers.tex
+++ b/doc/refman/headers.sty
@@ -1,7 +1,6 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% File title.tex
-% Pretty Headers
-% And commands for multiple indexes
+% File headers.sty
+% Commands for pretty headers, multiple indexes, and the appendix.
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \usepackage{fancyhdr}
 
@@ -20,13 +19,11 @@
 
 \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
@@ -57,42 +54,11 @@ Vernacular Commands Index}
 \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}}
@@ -102,27 +68,17 @@ Vernacular Commands Index}
   \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: