% 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 module identifiers
\newcommand{\coqdocmod}[1]{\textsc{\textsf{#1}}}

% macro for typesetting module constant identifiers (e.g. Parameters in
% module types)
\newcommand{\coqdocax}[1]{\textsl{\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{ifpdf}
\ifpdf
  \usepackage[pdftex]{hyperref}
  \hypersetup{raiselinks=true,colorlinks=true,linkcolor=black}
  \usepackage[all]{hypcap}

  \newcommand{\coqdef}[3]{\phantomsection\hypertarget{coq:#1}{#3}}
  \newcommand{\coqref}[2]{\hyperlink{coq:#1}{#2}}
  \newcommand{\identref}[2]{\hyperlink{coq:#1}{\textsf {#2}}}
  \newcommand{\coqlibrary}[2]{\cleardoublepage\phantomsection
    \hypertarget{coq:#1}{\chapter{Library \coqdoccst{#2}}}}
\else
  \newcommand{\coqdef}[3]{#3}
  \newcommand{\coqref}[2]{#2}
  \newcommand{\identref}[2]{\textsf {#2}}
  \newcommand{\coqlibrary}[2]{\cleardoublepage\chapter{Library \coqdoccst{#2}}}
\fi
\usepackage{xr}

%\usepackage{color}
%\usepackage{multind}
%\newcommand{\coqdef}[3]{\hypertarget{coq:#1}{\index{coq}{#1@#2|hyperpage}#3}}

  

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


\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{\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}}}

\newcommand{\coqsection}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
\newcommand{\coqsectionref}[2]{\coqref{#1}{\coqdoccst{#2}}}

%\newcommand{\coqlibrary}[2]{\chapter{Library \coqdoccst{#2}}\label{coq:#1}}
  
%\newcommand{\coqlibraryref}[2]{\ref{coq:#1}}

\newcommand{\coqlibraryref}[2]{\coqref{#1}{\coqdoccst{#2}}}

\newcommand{\coqaxiom}[2]{\coqdef{#1}{#2}{\coqdocax{#2}}}
\newcommand{\coqaxiomref}[2]{\coqref{#1}{\coqdocax{#2}}}

\newcommand{\coqmodule}[2]{\coqdef{#1}{#2}{\coqdocmod{#2}}}
\newcommand{\coqmoduleref}[2]{\coqref{#1}{\coqdocmod{#2}}}


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