1 files changed, 0 insertions, 87 deletions
diff --git a/doc/refman/headers.sty b/doc/refman/headers.sty
deleted file mode 100644
index bc5f5c6c..00000000
--- a/doc/refman/headers.sty
+++ /dev/null
@@ -1,87 +0,0 @@
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% 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: