aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--tools/coqdoc/coqdoc.sty21
-rw-r--r--tools/coqdoc/output.ml6
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"