%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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: