diff options
| author | Hugo Herbelin | 2020-11-05 16:16:31 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-14 21:54:08 +0100 |
| commit | b01fb0118f701f7aec83a04039a280238c866be0 (patch) | |
| tree | f4c6b8cbed16b2110f958a7a4e1cfc52f896197d /tools | |
| parent | a9e3dbd470079b1088bd686344bc54b2d086e3eb (diff) | |
Dead code in coqdoc.
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coqdoc/output.ml | 17 | ||||
| -rw-r--r-- | tools/coqdoc/output.mli | 3 |
2 files changed, 0 insertions, 20 deletions
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 32cf05e1eb..a6165918f9 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -479,10 +479,6 @@ module Latex = struct let end_coq () = printf "\\end{coqdoccode}\n" - let start_code () = end_doc (); start_coq () - - let end_code () = end_coq (); start_doc () - let section_kind = function | 1 -> "\\section{" | 2 -> "\\subsection{" @@ -754,10 +750,6 @@ module Html = struct let end_comment () = printf "*)</span>" - let start_code () = end_doc (); start_coq () - - let end_code () = end_coq (); start_doc () - let start_inline_coq () = if !inline_notmono then printf "<span class=\"inlinecodenm\">" else printf "<span class=\"inlinecode\">" @@ -1069,9 +1061,6 @@ module TeXmacs = struct let start_comment () = () let end_comment () = () - let start_code () = in_doc := true; printf "<\\code>\n" - let end_code () = in_doc := false; printf "\n</code>" - let section_kind = function | 1 -> "section" | 2 -> "subsection" @@ -1181,9 +1170,6 @@ module Raw = struct let start_coq () = () let end_coq () = () - let start_code () = end_doc (); start_coq () - let end_code () = end_coq (); start_doc () - let section_kind = function | 1 -> "* " @@ -1240,9 +1226,6 @@ let end_comment = select Latex.end_comment Html.end_comment TeXmacs.end_comment let start_coq = select Latex.start_coq Html.start_coq TeXmacs.start_coq Raw.start_coq let end_coq = select Latex.end_coq Html.end_coq TeXmacs.end_coq Raw.end_coq -let start_code = select Latex.start_code Html.start_code TeXmacs.start_code Raw.start_code -let end_code = select Latex.end_code Html.end_code TeXmacs.end_code Raw.end_code - let start_inline_coq = select Latex.start_inline_coq Html.start_inline_coq TeXmacs.start_inline_coq Raw.start_inline_coq let end_inline_coq = diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli index b7a8d4d858..4088fdabf7 100644 --- a/tools/coqdoc/output.mli +++ b/tools/coqdoc/output.mli @@ -41,9 +41,6 @@ val end_comment : unit -> unit val start_coq : unit -> unit val end_coq : unit -> unit -val start_code : unit -> unit -val end_code : unit -> unit - val start_inline_coq : unit -> unit val end_inline_coq : unit -> unit |