still some more dead code removal

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15875 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 0 insertions, 57 deletions

diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index d7b54fd0f..2c58a05e2 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -75,7 +75,6 @@
   let brackets = ref 0
   let comment_level = ref 0
   let in_proof = ref None
-  let in_emph = ref false
 
   let in_env start stop = 
     let r = ref false in
@@ -102,8 +101,6 @@
             let length_skip = 1 + String.length s1 in
               lexbuf.lex_curr_pos <- lexbuf.lex_start_pos + length_skip
 
-  let is_space = function ' ' | '\t' | '\n' | '\r' -> true | _ -> false
-
   (* saving/restoring the PP state *)
 
   type state = {
@@ -127,8 +124,6 @@
 
   let without_light = without_ref Cdglobals.light
 
-  let show_all f = without_gallina (without_light f)
-
   let begin_show () = save_state (); Cdglobals.gallina := false; Cdglobals.light := false
   let end_show () = restore_state ()
 
@@ -251,14 +246,6 @@
     with _ ->
       ()
 
-  let extract_ident_re = Str.regexp "([ \t]*\\([^ \t]+\\)[ \t]*:="
-  let extract_ident s =
-    assert (String.length s >= 3);
-    if Str.string_match extract_ident_re s 0 then
-      Str.matched_group 1 s
-    else
-      String.sub s 1 (String.length s - 3)
-
   let output_indented_keyword s lexbuf =
     let nbsp,isp = count_spaces s in
     Output.indentation nbsp;
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index d319ce72d..610fa28f7 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Filename
-open Lexing
 open Printf
 open Cdglobals
 
@@ -37,7 +35,6 @@ type index_entry =
   | Ref of coq_module * string * entry_type
   | Mod of coq_module * string
 
-let current_type : entry_type ref = ref Library
 let current_library = ref ""
   (** refers to the file being parsed *)
 
@@ -71,10 +68,6 @@ let add_ref m loc m' sp id ty =
     if Hashtbl.mem deftable idx then ()
     else Hashtbl.add deftable idx (Ref (m', full_ident sp id, ty))
 
-let add_mod m loc m' id =
-  Hashtbl.add reftable (m, loc) (Mod (m', id));
-  Hashtbl.add deftable m (Mod (m', id))
-
 let find m l = Hashtbl.find reftable (m, l)
 
 let find_string m s = Hashtbl.find deftable s
@@ -94,9 +87,6 @@ let empty_stack = []
 let module_stack = ref empty_stack
 let section_stack = ref empty_stack
 
-let init_stack () =
-  module_stack := empty_stack; section_stack := empty_stack
-
 let push st p = st := p::!st
 let pop st =
   match !st with
@@ -108,27 +98,6 @@ let head st =
     | [] -> ""
     | x::_ -> x
 
-let begin_module m = push module_stack m
-let begin_section s = push section_stack s
-
-let end_block id =
-  (** determines if it ends a module or a section and pops the stack *)
-  if ((String.compare (head !module_stack) id ) == 0) then
-    pop module_stack
-  else if ((String.compare (head !section_stack) id) == 0) then
-    pop section_stack
-  else
-    ()
-
-let make_fullid id =
-  (** prepends the current module path to an id *)
-  let path = string_of_stack !module_stack in
-    if String.length path > 0 then
-      path ^ "." ^ id
-    else
-      id
-
-
 (* Coq modules *)
 
 let split_sp s =
@@ -207,10 +176,6 @@ let sort_entries el =
 
 let display_letter c = if c = '*' then "other" else String.make 1 c
 
-let index_size = List.fold_left (fun s (_,l) -> s + List.length l) 0
-
-let hashtbl_elements h = Hashtbl.fold (fun x y l -> (x,y)::l) h []
-
 let type_name = function
   | Library ->
       let ln = !lib_name in
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 86a5b0cbe..a0f36d9a1 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -581,9 +581,6 @@ module Html = struct
     | '&' -> printf "&amp;"
     | c -> output_char c
 
-  let raw_string s =
-    for i = 0 to String.length s - 1 do char s.[i] done
-
   let escaped =
     let buff = Buffer.create 5 in
     fun s ->
@@ -944,8 +941,6 @@ module TeXmacs = struct
   let (preamble : string Queue.t) =
     in_doc := false; Queue.create ()
 
-  let push_in_preamble s = Queue.add s preamble
-
   let header () =
     output_string
       "(*i This file has been automatically generated with the command  \n";
@@ -1066,8 +1061,6 @@ module TeXmacs = struct
 
   let paragraph () = printf "\n\n"
 
-  let line_break_true () = printf "<format|line break>"
-
   let line_break () = printf "\n"
 
   let empty_line_of_code () = printf "\n"
diff --git a/tools/coqdoc/tokens.ml b/tools/coqdoc/tokens.ml
index 10a105f9b..7c6c1f092 100644
--- a/tools/coqdoc/tokens.ml
+++ b/tools/coqdoc/tokens.ml
@@ -9,8 +9,6 @@
 (* Application of printing rules based on a dictionary specific to the
    target language *)
 
-open Cdglobals
-
 (*s Dictionaries: trees annotated with string options, each node being a map
     from chars to dictionaries (the subtrees). A trie, in other words.