From b01fb0118f701f7aec83a04039a280238c866be0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 5 Nov 2020 16:16:31 +0100
Subject: Dead code in coqdoc.

---
 tools/coqdoc/output.ml  | 17 -----------------
 tools/coqdoc/output.mli |  3 ---
 2 files changed, 20 deletions(-)

(limited to 'tools')

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