Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
tree: 3d4b56b9bd
Fetching contributors…

Cannot retrieve contributors at this time

198 lines (149 sloc) 6.582 kb
% 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}{}{}
% 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
Jump to Line
Something went wrong with that request. Please try again.