aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-10-26 14:33:18 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-10-26 14:33:18 +0000
commitcde1310d3fe879b8f1c71118fa1cdd936560a64b (patch)
tree28a37d9b7f590e8b289048b0bc9a86a56a1f9821 /tools
parent20ba5a3934067925fb08d6d464ebe5102d358d41 (diff)
Stop using a coqdocdoc env which prevents use of environments inside
comments that go across code and doc (e.g. for beamer frames), it was unused anyway. Add "do" and "repeat" as tactic identifiers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11507 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
-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"