diff options
| -rw-r--r-- | tools/coqdoc/coqdoc.sty | 21 | ||||
| -rw-r--r-- | tools/coqdoc/output.ml | 6 |
2 files changed, 12 insertions, 15 deletions
diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty index 0674c8b15..7380deb60 100644 --- a/tools/coqdoc/coqdoc.sty +++ b/tools/coqdoc/coqdoc.sty @@ -67,11 +67,8 @@ % Environment encompassing code fragments +% !!! CAUTION: This environment may have empty contents \newenvironment{coqdoccode}{}{} -% Environment encompassing documentation fragments -\newenvironment{coqdocdoc}{}{} - -% !!! CAUTION: These environments may have empty contents % newline and indentation %BEGIN LATEX @@ -93,9 +90,9 @@ } \usepackage{ifpdf} \ifpdf - \usepackage[pdftex]{hyperref} + \RequirePackage{hyperref} \hypersetup{raiselinks=true,colorlinks=true,linkcolor=black} - \usepackage[all]{hypcap} + \RequirePackage{hypcap} % To do indexing, use something like: % \usepackage{multind} @@ -135,7 +132,7 @@ \def\coqdocconstrcolor{constrmaroon} \def\coqdocmodcolor{defgreen} \def\coqdocaxcolor{varpurple} -\def\coqdoctaccolor{kwred} +\def\coqdoctaccolor{black} \def\coqdockw#1{{\color{\coqdockwcolor}{\texttt{#1}}}} \def\coqdocvar#1{{\color{\coqdocvarcolor}{\textit{#1}}}} @@ -144,7 +141,7 @@ \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{kw}}}} +\def\coqdoctac#1{{\color{\coqdoctaccolor}{\texttt{#1}}}} \fi \newcommand{\coqdefinition}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}} @@ -181,8 +178,8 @@ \newcommand{\coqnotationref}[2]{\coqref{#1}{\coqdockw{#2}}} -\newcommand{\coqsection}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}} -\newcommand{\coqsectionref}[2]{\coqref{#1}{\coqdoccst{#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}} @@ -193,7 +190,7 @@ \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}}} +\newcommand{\coqmodule}[2]{\coqdef{mod:#1}{#2}{\coqdocmod{#2}}} +\newcommand{\coqmoduleref}[2]{\coqref{mod:#1}{\coqdocmod{#2}}} \endinput diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 0d5b5e2a5..70f9a849f 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -66,7 +66,7 @@ let is_tactic = "elimtype"; "progress"; "setoid_rewrite"; "destruct"; "destruction"; "destruct_call"; "dependent"; "elim"; "extensionality"; "f_equal"; "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega"; - "set"; "assert"; + "set"; "assert"; "do"; "repeat"; "cut"; "assumption"; "exact"; "split"; "subst"; "try"; "discriminate"; "simpl"; "unfold"; "red"; "compute"; "at"; "in"; "by"; "reflexivity"; "symmetry"; "transitivity"; @@ -306,9 +306,9 @@ module Latex = struct let stop_item () = reach_item_level 0 - let start_doc () = printf "\\begin{coqdocdoc}\n" + let start_doc () = () - let end_doc () = stop_item (); printf "\\end{coqdocdoc}\n" + let end_doc () = stop_item () let start_coq () = printf "\\begin{coqdoccode}\n" |