1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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:
|
