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


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

% 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{\coqdocvar}[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}}

% macro for typesetting tactic identifiers
\newcommand{\coqdoctac}[1]{\texttt{#1}}


% Environment encompassing code fragments
% !!! CAUTION: This environment may have empty contents
\newenvironment{coqdoccode}{}{}

% Environment for comments
\newenvironment{coqdoccomment}{\tt(*}{*)}

% newline and indentation 
%BEGIN LATEX
% Base indentation length
\newlength{\coqdocbaseindent}
\setlength{\coqdocbaseindent}{0em}

% Beginning of a line without any Coq indentation
\newcommand{\coqdocnoindent}{\noindent\kern\coqdocbaseindent}
% Beginning of a line with a given Coq indentation
\newcommand{\coqdocindent}[1]{\noindent\kern\coqdocbaseindent\noindent\kern#1}
% End-of-the-line
\newcommand{\coqdoceol}{\hspace*{\fill}\setlength\parskip{0pt}\par}
% Empty lines (in code only)
\newcommand{\coqdocemptyline}{\vskip 0.4em plus 0.1em minus 0.1em}

% macro for typesetting the title of a module implementation
\newcommand{\coqdocmodule}[1]{\chapter{Module #1}\markboth{Module #1}{}
}
\usepackage{ifpdf}
\ifpdf
  \RequirePackage{hyperref}
  \hypersetup{raiselinks=true,colorlinks=true,linkcolor=black}

  % To do indexing, use something like:
  % \usepackage{multind}
  % \newcommand{\coqdef}[3]{\hypertarget{coq:#1}{\index{coq}{#1@#2|hyperpage}#3}}

  \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 \texorpdfstring{\coqdoccst}{}{#2}}}}
\else
  \newcommand{\coqdef}[3]{#3}
  \newcommand{\coqref}[2]{#2}
  \newcommand{\texorpdfstring}[2]{#1}
  \newcommand{\identref}[2]{\textsf{#2}}
  \newcommand{\coqlibrary}[2]{\cleardoublepage\chapter{Library \coqdoccst{#2}}}
\fi
\usepackage{xr}

\newif\if@coqdoccolors
  \@coqdoccolorsfalse

\DeclareOption{color}{\@coqdoccolorstrue}
\ProcessOptions

\if@coqdoccolors
\RequirePackage{xcolor}
\definecolor{varpurple}{rgb}{0.4,0,0.4}
\definecolor{constrmaroon}{rgb}{0.6,0,0}
\definecolor{defgreen}{rgb}{0,0.4,0}
\definecolor{indblue}{rgb}{0,0,0.8}
\definecolor{kwred}{rgb}{0.8,0.1,0.1}

\def\coqdocvarcolor{varpurple}
\def\coqdockwcolor{kwred}
\def\coqdoccstcolor{defgreen}
\def\coqdocindcolor{indblue}
\def\coqdocconstrcolor{constrmaroon}
\def\coqdocmodcolor{defgreen}
\def\coqdocaxcolor{varpurple}
\def\coqdoctaccolor{black}

\def\coqdockw#1{{\color{\coqdockwcolor}{\texttt{#1}}}}
\def\coqdocvar#1{{\color{\coqdocvarcolor}{\textit{#1}}}}
\def\coqdoccst#1{{\color{\coqdoccstcolor}{\textrm{#1}}}}
\def\coqdocind#1{{\color{\coqdocindcolor}{\textsf{#1}}}}
\def\coqdocconstr#1{{\color{\coqdocconstrcolor}{\textsf{#1}}}}
\def\coqdocmod#1{{{\color{\coqdocmodcolor}{\textsc{\textsf{#1}}}}}}
\def\coqdocax#1{{{\color{\coqdocaxcolor}{\textsl{\textrm{#1}}}}}}
\def\coqdoctac#1{{\color{\coqdoctaccolor}{\texttt{#1}}}}
\fi

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

\newcommand{\coqvariable}[2]{\coqdocvar{#2}}
\newcommand{\coqvariableref}[2]{\coqref{#1}{\coqdocvar{#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{sec:#1}{#2}{\coqdoccst{#2}}}
\newcommand{\coqsectionref}[2]{\coqref{sec:#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{mod:#1}{#2}{\coqdocmod{#2}}}
\newcommand{\coqmoduleref}[2]{\coqref{mod:#1}{\coqdocmod{#2}}}

\endinput