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

% These are the real macros used by coqdoc, their typesetting is 
% based on the above macros by default.

\newcommand{\coqdoclibrary}[1]{\coqdoccst{#1}}
\newcommand{\coqdocinductive}[1]{\coqdocind{#1}}
\newcommand{\coqdocdefinition}[1]{\coqdoccst{#1}}
\newcommand{\coqdocvariable}[1]{\coqdocvar{#1}}
\newcommand{\coqdocbinder}[1]{\coqdocvar{#1}}
\newcommand{\coqdocconstructor}[1]{\coqdocconstr{#1}}
\newcommand{\coqdoclemma}[1]{\coqdoccst{#1}}
\newcommand{\coqdocclass}[1]{\coqdocind{#1}}
\newcommand{\coqdocinstance}[1]{\coqdoccst{#1}}
\newcommand{\coqdocmethod}[1]{\coqdoccst{#1}}
\newcommand{\coqdocabbreviation}[1]{\coqdoccst{#1}}
\newcommand{\coqdocrecord}[1]{\coqdocind{#1}}
\newcommand{\coqdocprojection}[1]{\coqdoccst{#1}}
\newcommand{\coqdocnotation}[1]{\coqdockw{#1}}
\newcommand{\coqdocsection}[1]{\coqdoccst{#1}}
\newcommand{\coqdocaxiom}[1]{\coqdocax{#1}}
\newcommand{\coqdocmodule}[1]{\coqdocmod{#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 Rocq indentation
\newcommand{\coqdocnoindent}{\noindent\kern\coqdocbaseindent}
% Beginning of a line with a given Rocq 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}

\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{\coqexternalref}[3]{\href{#1.html\##2}{#3}}

  \newcommand{\identref}[2]{\hyperlink{coq:#1}{\textsf {#2}}}
  \newcommand{\coqlibrary}[3]{\cleardoublepage\phantomsection
    \hypertarget{coq:#1}{\chapter{#2\texorpdfstring{\coqdoccst}{}{#3}}}}
\else
  \newcommand{\coqdef}[3]{#3}
  \newcommand{\coqref}[2]{#2}
  \newcommand{\coqexternalref}[3]{#3}
  \newcommand{\texorpdfstring}[2]{#1}
  \newcommand{\identref}[2]{\textsf{#2}}
  \newcommand{\coqlibrary}[3]{\cleardoublepage\chapter{#2\coqdoccst{#3}}}
\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

\endinput