From 0256a92eb0d0265750bd38a85dce4f9487aefe5b Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sat, 6 Oct 2012 10:08:51 +0000
Subject: still some more dead code removal

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15875 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 checker/check_stat.ml                         |  5 ----
 checker/checker.ml                            |  1 -
 checker/closure.ml                            |  1 -
 checker/declarations.ml                       |  3 +--
 checker/mod_checking.ml                       |  1 -
 checker/modops.ml                             |  2 --
 checker/reduction.ml                          |  1 -
 checker/subtyping.ml                          |  3 ---
 checker/term.ml                               |  3 +--
 checker/typeops.ml                            |  2 +-
 checker/validate.ml                           |  2 +-
 dev/top_printers.ml                           |  8 ------
 parsing/lexer.ml4                             |  1 -
 plugins/funind/functional_principles_types.ml | 19 ---------------
 plugins/micromega/csdpcert.ml                 |  3 +--
 plugins/micromega/sos_lib.ml                  |  4 +--
 plugins/xml/xmlcommand.ml                     |  6 -----
 printing/pptactic.ml                          | 12 ---------
 printing/ppvernac.ml                          |  4 ---
 proofs/proof_global.ml                        |  9 -------
 proofs/proof_type.ml                          |  1 -
 tactics/auto.ml                               |  2 --
 tactics/elim.ml                               |  1 -
 tactics/hiddentac.ml                          |  2 --
 tools/coqdoc/cpretty.mll                      | 13 ----------
 tools/coqdoc/index.ml                         | 35 ---------------------------
 tools/coqdoc/output.ml                        |  7 ------
 tools/coqdoc/tokens.ml                        |  2 --
 tools/coqwc.mll                               |  1 -
 tools/gallina_lexer.mll                       |  1 -
 toplevel/metasyntax.ml                        |  1 -
 toplevel/toplevel.ml                          |  7 ------
 32 files changed, 7 insertions(+), 156 deletions(-)

diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index 0e7aec1a8..3176a4307 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -7,12 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
-open Util
-open System
-open Flags
 open Names
-open Term
 open Declarations
 open Environ
 
diff --git a/checker/checker.ml b/checker/checker.ml
index ea2e3892f..8389803fc 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -12,7 +12,6 @@ open Util
 open System
 open Flags
 open Names
-open Term
 open Check
 
 let () = at_exit flush_all
diff --git a/checker/closure.ml b/checker/closure.ml
index f86aa82eb..c515bdb24 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
 open Util
 open Pp
 open Term
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 8b146d18b..df0134e02 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -1,4 +1,3 @@
-open Errors
 open Util
 open Names
 open Term
@@ -111,7 +110,7 @@ let map_mp mp1 mp2 = add_mp mp1 mp2 empty_subst
 let mp_in_delta mp =
   Deltamap.mem_mp mp
 
-let rec find_prefix resolve mp =
+let find_prefix resolve mp =
   let rec sub_mp = function
     | MPdot(mp,l) as mp_sup ->
 	(try Deltamap.find_mp mp_sup resolve
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index a51b66ce0..7dfa29e16 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -4,7 +4,6 @@ open Errors
 open Util
 open Names
 open Term
-open Inductive
 open Reduction
 open Typeops
 open Indtypes
diff --git a/checker/modops.ml b/checker/modops.ml
index 9d5829605..1c4a2916e 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -11,10 +11,8 @@ open Errors
 open Util
 open Pp
 open Names
-open Univ
 open Term
 open Declarations
-open Environ
 (*i*)
 
 let error_not_a_constant l =
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 195f7d423..c2d5c261c 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -8,7 +8,6 @@
 
 open Errors
 open Util
-open Names
 open Term
 open Univ
 open Closure
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 7d2ced7fd..390c2b9e7 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -18,9 +18,6 @@ open Reduction
 open Inductive
 open Modops
 (*i*)
-open Pp
-
-
 
 (* This local type is used to subtype a constant with a constructor or
    an inductive type. It can also be useful to allow reorderings in
diff --git a/checker/term.ml b/checker/term.ml
index b41bebca2..0c3fc741d 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -10,7 +10,6 @@
 
 open Errors
 open Util
-open Pp
 open Names
 open Univ
 open Esubst
@@ -134,7 +133,7 @@ let rec strip_outer_cast c = match c with
   | Cast (c,_,_) -> strip_outer_cast c
   | _ -> c
 
-let rec collapse_appl c = match c with
+let collapse_appl c = match c with
   | App (f,cl) ->
       let rec collapse_rec f cl2 =
         match (strip_outer_cast f) with
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 91f58a04a..ad05f96b7 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -75,7 +75,7 @@ let judge_of_variable env id =
 (* Checks if a context of variable can be instantiated by the
    variables of the current env *)
 (* TODO: check order? *)
-let rec check_hyps_inclusion env sign =
+let check_hyps_inclusion env sign =
   fold_named_context
     (fun (id,_,ty1) () ->
       let ty2 = named_type id env in
diff --git a/checker/validate.ml b/checker/validate.ml
index 2f46695cd..eeff9d1cd 100644
--- a/checker/validate.ml
+++ b/checker/validate.ml
@@ -164,7 +164,7 @@ let val_set ?(name="Set.t") f =
 		     vset;ext "bal" val_int|]|])
 
 (* Maps *)
-let rec val_map ?(name="Map.t") fk fv =
+let val_map ?(name="Map.t") fk fv =
   val_rec_sum name 1
     (fun vmap ->
        [|[|vmap; ext "key" fk; ext "value" fv;
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 8e7a92a8f..20e0fff55 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -8,25 +8,19 @@
 
 (* Printers for the ocaml toplevel. *)
 
-open System
-open Errors
 open Util
 open Pp
 open Names
 open Libnames
 open Globnames
 open Nameops
-open Sign
 open Univ
 open Environ
 open Printer
 open Term
-open Termops
-open Cerrors
 open Evd
 open Goptions
 open Genarg
-open Mod_subst
 open Clenv
 
 let _ = Constrextern.print_evar_arguments := true
@@ -411,7 +405,6 @@ END
 open Pcoq
 open Genarg
 open Egramml
-open Egramcoq
 
 let _ =
   try
@@ -449,7 +442,6 @@ let _ =
 
 (* Setting printer of unbound global reference *)
 open Names
-open Nameops
 open Libnames
 
 let encode_path loc prefix mpdir suffix id =
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index ca5c20c71..3071e0eb4 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -541,7 +541,6 @@ let current_location_table = ref (loct_create ())
 type location_table = (int, CompatLoc.t) Hashtbl.t
 let location_table () = !current_location_table
 let restore_location_table t = current_location_table := t
-let location_function n = loct_func !current_location_table n
 
 (** {6 The lexer of Coq} *)
 
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index a14b47393..533fbfaaa 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -15,25 +15,6 @@ open Misctypes
 exception Toberemoved_with_rel of int*constr
 exception Toberemoved
 
-
-let pr_elim_scheme el =
-  let env = Global.env () in
-  let msg = str "params := " ++ Printer.pr_rel_context env el.params in
-  let env = Environ.push_rel_context el.params env in
-  let msg = msg ++ fnl () ++ str "predicates := "++ Printer.pr_rel_context env el.predicates in
-  let env = Environ.push_rel_context el.predicates env in
-  let msg = msg ++ fnl () ++ str "branches := " ++ Printer.pr_rel_context env el.branches in
-  let env = Environ.push_rel_context el.branches env in
-  let msg = msg ++ fnl () ++ str "args := " ++ Printer.pr_rel_context env el.args in
-  let env = Environ.push_rel_context el.args env in
-  msg ++ fnl () ++ str "concl := " ++ pr_lconstr_env env el.concl
-
-
-let observe s =
-  if do_observe ()
-  then Pp.msg_debug s
-
-
 let pr_elim_scheme el =
   let env = Global.env () in
   let msg = str "params := " ++ Printer.pr_rel_context env el.params in
diff --git a/plugins/micromega/csdpcert.ml b/plugins/micromega/csdpcert.ml
index e416c514c..f848591cc 100644
--- a/plugins/micromega/csdpcert.ml
+++ b/plugins/micromega/csdpcert.ml
@@ -12,7 +12,6 @@
 (*                                                                      *)
 (************************************************************************)
 
-open Big_int
 open Num
 open Sos
 open Sos_types
@@ -60,7 +59,7 @@ open Mutils
 
 
 
-let rec canonical_sum_to_string = function s -> failwith "not implemented"
+let canonical_sum_to_string = function s -> failwith "not implemented"
 
 let print_canonical_sum m = Format.print_string (canonical_sum_to_string m)
 
diff --git a/plugins/micromega/sos_lib.ml b/plugins/micromega/sos_lib.ml
index e592611ac..41cbeda3f 100644
--- a/plugins/micromega/sos_lib.ml
+++ b/plugins/micromega/sos_lib.ml
@@ -6,7 +6,7 @@
 (*   independent bits                                                        *)
 (* - Frédéric Besson (fbesson@irisa.fr) is using it to feed  micromega       *)
 (* ========================================================================= *)
-open Sos_types
+
 open Num
 
 let debugging = ref false;;
@@ -546,7 +546,7 @@ let fix err prs input =
   try prs input
   with Noparse -> failwith (err ^ " expected");;
 
-let rec listof prs sep err =
+let listof prs sep err =
   prs ++ many (sep ++ fix err prs >> snd) >> (fun (h,t) -> h::t);;
 
 let possibly prs input =
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 0673e79fb..8259266af 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -108,12 +108,6 @@ let types_filename_of_filename =
   | None   -> None
 ;;
 
-let prooftree_filename_of_filename =
- function
-    Some f -> Some (f ^ ".proof_tree")
-  | None   -> None
-;;
-
 let theory_filename xml_library_root =
  let module N = Names in
   match xml_library_root with
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 48a59be05..2ec66bb34 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -980,15 +980,6 @@ let strip_prod_binders_glob_constr n (ty,_) =
         | _ -> error "Cannot translate fix tactic: not enough products" in
   strip_ty [] n ty
 
-let strip_prod_binders_constr n ty =
-  let rec strip_ty acc n ty =
-    if n=0 then (List.rev acc, ty) else
-      match Term.kind_of_term ty with
-          Term.Prod(na,a,b) ->
-            strip_ty (([Loc.ghost,na],a)::acc) (n-1) b
-        | _ -> error "Cannot translate fix tactic: not enough products" in
-  strip_ty [] n ty
-
 let drop_env f _env = f
 
 let pr_constr_or_lconstr_pattern_expr b =
@@ -1030,9 +1021,6 @@ let rec glob_printers =
 and pr_glob_tactic_level env n (t:glob_tactic_expr) =
   fst (make_pr_tac glob_printers env) n t
 
-let pr_constr_or_lconstr_pattern b =
-  if b then pr_lconstr_pattern else pr_constr_pattern
-
 let pr_raw_tactic env = pr_raw_tactic_level env ltop
 let pr_glob_tactic env = pr_glob_tactic_level env ltop
 
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 3553373fb..686d2ae2d 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -175,10 +175,6 @@ let pr_set_option a b =
 
 let pr_topcmd _ = str"(* <Warning> : No printer for toplevel commands *)"
 
-let pr_destruct_location = function
-  | Tacexpr.ConclLocation ()  -> str"Conclusion"
-  | Tacexpr.HypLocation b -> if b then str"Discardable Hypothesis" else str"Hypothesis"
-
 let pr_opt_hintbases l = match l with
   | [] -> mt()
   | _ as z -> str":" ++ spc() ++ prlist_with_sep sep str z
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 178c2ab2d..25ed1f3e8 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -125,15 +125,6 @@ let find_top l =
   | np::_ -> np
   | [] -> raise NoCurrentProof
 
-let rotate_top l1 l2 =
-  let np = extract_top l1 in
-  push np l2
-
-let rotate_find id l1 l2 =
-  let np = extract id l1 in
-  push np l2
-
-
 (* combinators for the proof_info map *)
 let add id info m =
   m := Idmap.add id info !m
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index e09d72e47..b7237f1fc 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -12,7 +12,6 @@ open Names
 open Term
 open Tacexpr
 open Glob_term
-open Genarg
 open Nametab
 open Pattern
 open Misctypes
diff --git a/tactics/auto.ml b/tactics/auto.ml
index d773d2092..47b89e9af 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -1430,6 +1430,4 @@ let gen_auto ?(debug=Off) n lems dbnames =
   | None -> full_auto ~debug n lems
   | Some l -> auto ~debug n lems l
 
-let inj_or_var = Option.map (fun n -> ArgArg n)
-
 let h_auto ?(debug=Off) n lems l = gen_auto ~debug n lems l
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 685a70bad..88348206b 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -16,7 +16,6 @@ open Hipattern
 open Tacmach
 open Tacticals
 open Tactics
-open Tacexpr
 open Misctypes
 
 let introElimAssumsThen tac ba =
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index fc0f24fcd..e61922d07 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Refiner
-open Tacexpr
 open Tactics
 open Util
 open Locus
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.
 
diff --git a/tools/coqwc.mll b/tools/coqwc.mll
index a5376ec44..50f989e7c 100644
--- a/tools/coqwc.mll
+++ b/tools/coqwc.mll
@@ -15,7 +15,6 @@
 (*i*){
 open Printf
 open Lexing
-open Filename
 (*i*)
 
 (*s Command-line options. *)
diff --git a/tools/gallina_lexer.mll b/tools/gallina_lexer.mll
index cfbfac98f..5d8a1d209 100644
--- a/tools/gallina_lexer.mll
+++ b/tools/gallina_lexer.mll
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 {
- open Lexing
 
  let chan_out = ref stdout
 
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index a67400788..e7c19fbb2 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -8,7 +8,6 @@
 
 open Pp
 open Flags
-open Compat
 open Errors
 open Util
 open Names
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 7e301ba0e..ec390683f 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -182,13 +182,6 @@ let print_location_in_file s inlibrary fname loc =
         (close_in ic;
          hov 1 (errstrm ++ spc() ++ str"(invalid location):") ++ fnl ())
 
-let print_command_location ib dloc =
-  match dloc with
-    | Some (bp,ep) ->
-        (str"Error during interpretation of command:" ++ fnl () ++
-           str(String.sub ib.str (bp-ib.start) (ep-bp)) ++ fnl ())
-    | None -> (mt ())
-
 let valid_loc dloc loc =
   loc <> Loc.ghost
   & match dloc with
-- 
cgit v1.2.3