From cde1310d3fe879b8f1c71118fa1cdd936560a64b Mon Sep 17 00:00:00 2001
From: msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sun, 26 Oct 2008 14:33:18 +0000
Subject: 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
---
 tools/coqdoc/coqdoc.sty | 21 +++++++++------------
 tools/coqdoc/output.ml  |  6 +++---
 2 files changed, 12 insertions(+), 15 deletions(-)

(limited to 'tools/coqdoc')

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"
 
-- 
cgit v1.2.3