% This is coqdoc.sty, by Jean-Christophe Filliātre
% This LaTeX package is used by coqdoc (http://www.lri.fr/~filliatr/coqdoc)
%
% You can modify the following macros to customize the appearance
% of the document.

\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{coqdoc}[2002/02/11]

% % Headings
% \usepackage{fancyhdr}
% \newcommand{\coqdocleftpageheader}{\thepage\ -- \today}
% \newcommand{\coqdocrightpageheader}{\today\ -- \thepage}
% \pagestyle{fancyplain}

% %BEGIN LATEX
% \headsep 8mm
% \renewcommand{\plainheadrulewidth}{0.4pt}
% \renewcommand{\plainfootrulewidth}{0pt}
% \lhead[\coqdocleftpageheader]{\leftmark}
% \rhead[\leftmark]{\coqdocrightpageheader}
% \cfoot{}
% %END LATEX

% Hevea puts to much space with \medskip and \bigskip
%HEVEA\renewcommand{\medskip}{}
%HEVEA\renewcommand{\bigskip}{}

% own name
\newcommand{\coqdoc}{\textsf{coqdoc}}

% pretty underscores (the package fontenc causes ugly underscores)
%BEGIN LATEX
\def\_{\kern.08em\vbox{\hrule width.35em height.6pt}\kern.08em}
%END LATEX

% macro for typesetting keywords
\newcommand{\coqdockw}[1]{\texttt{#1}}

% macro for typesetting variable identifiers
\newcommand{\coqdocid}[1]{\textit{#1}}

% macro for typesetting constant identifiers
\newcommand{\coqdoccst}[1]{\textsf{#1}}

% macro for typesetting inductive type identifiers
\newcommand{\coqdocind}[1]{\textbf{\textsf{#1}}}

% macro for typesetting constructor identifiers
\newcommand{\coqdocconstr}[1]{\textsf{#1}}

% newline and indentation 
%BEGIN LATEX
\newcommand{\coqdoceol}{\setlength\parskip{0pt}\par}
\newcommand{\coqdocindent}[1]{\noindent\kern#1}
%END LATEX
%HEVEA\newcommand{\coqdoceol}{\begin{rawhtml}<BR>\end{rawhtml}}
%HEVEA\newcommand{\coqdocindent}[1]{\hspace{#1}\hspace{#1}}

% macro for typesetting the title of a module implementation
\newcommand{\coqdocmodule}[1]{\chapter{Module #1}\markboth{Module #1}{}
}

\usepackage{hyperref}
\hypersetup{colorlinks=true,linkcolor=black}
%\usepackage{color}
%\usepackage{multind}
%\newcommand{\coqdef}[3]{\hypertarget{coq:#1}{\index{coq}{#1@#2|hyperpage}#3}}

\newcommand{\coqdef}[3]{\hypertarget{coq:#1}{#3}}
\newcommand{\coqref}[2]{\hyperlink{coq:#1}{#2}}

\newcommand{\coqdocvar}[1]{{\textit{#1}}}
\newcommand{\coqdoctac}[1]{{\texttt{#1}}}

\newcommand{\identref}[2]{\hyperlink{coq:#1}{\textsf {#2}}}

\newcommand{\coqdefinition}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
\newcommand{\coqdefinitionref}[2]{\coqref{#1}{\coqdoccst{#2}}}

%\newcommand{\coqvariable}[2]{\coqdef{#1}{#2}{\coqdocid{#2}}}
%\newcommand{\coqaxiom}[2]{\coqdef{#1}{#2}{\coqdocid{#2}}}
\newcommand{\coqvariable}[2]{\coqdocid{#2}}
\newcommand{\coqaxiom}[2]{\coqdocid{#2}}

\newcommand{\coqinductive}[2]{\coqdef{#1}{#2}{\coqdocind{#2}}}
\newcommand{\coqinductiveref}[2]{\coqref{#1}{\coqdocind{#2}}}

\newcommand{\coqconstructor}[2]{\coqdef{#1}{#2}{\coqdocconstr{#2}}}
\newcommand{\coqconstructorref}[2]{\coqref{#1}{\coqdocconstr{#2}}}

\newcommand{\coqlemma}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
\newcommand{\coqlemmaref}[2]{\coqref{#1}{\coqdoccst{#2}}}

\newcommand{\coqclass}[2]{\coqdef{#1}{#2}{\coqdocind{#2}}}
\newcommand{\coqclassref}[2]{\coqref{#1}{\coqdocind{#2}}}

\newcommand{\coqinstance}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
\newcommand{\coqinstanceref}[2]{\coqref{#1}{\coqdoccst{#2}}}

\newcommand{\coqmethod}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
\newcommand{\coqmethodref}[2]{\coqref{#1}{\coqdoccst{#2}}}

\newcommand{\coqabbreviation}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
\newcommand{\coqabbreviationref}[2]{\coqref{#1}{\coqdoccst{#2}}}

\newcommand{\coqrecord}[2]{\coqdef{#1}{#2}{\coqdocind{#2}}}
\newcommand{\coqrecordref}[2]{\coqref{#1}{\coqdocind{#2}}}

\newcommand{\coqprojection}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
\newcommand{\coqprojectionref}[2]{\coqref{#1}{\coqdoccst{#2}}}

\newcommand{\coqnotationref}[2]{\coqref{#1}{\coqdockw{#2}}}

%HEVEA\newcommand{\lnot}{\coqwkw{not}}
%HEVEA\newcommand{\lor}{\coqwkw{or}}
%HEVEA\newcommand{\land}{\&}