diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-26 14:33:18 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-26 14:33:18 +0000 |
| commit | cde1310d3fe879b8f1c71118fa1cdd936560a64b (patch) | |
| tree | 28a37d9b7f590e8b289048b0bc9a86a56a1f9821 /tools/coqdoc/output.ml | |
| parent | 20ba5a3934067925fb08d6d464ebe5102d358d41 (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/coqdoc/output.ml')
| -rw-r--r-- | tools/coqdoc/output.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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" |