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

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"