Remove some dead-code (thanks to ocaml warnings)

 The removed code isn't used locally and isn't exported in the signature

47 files changed, 18 insertions, 341 deletions

diff --git a/interp/reserve.ml b/interp/reserve.ml
index c104d0d15..272e6c8d1 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -122,9 +122,3 @@ let revert_reserved_type t =
   with Not_found | Failure _ -> Anonymous
 
 let _ = Namegen.set_reserved_typed_name revert_reserved_type
-
-let default_env () = {
-  ninterp_var_type = Id.Map.empty;
-  ninterp_rec_vars = Id.Map.empty;
-  ninterp_only_parse = false;
-}
diff --git a/kernel/constr.ml b/kernel/constr.ml
index cf05fe013..14b4a1772 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -325,8 +325,6 @@ let map f c = match kind c with
       if tl'==tl && bl'==bl then c
       else mkCoFix (ln,(lna,tl',bl'))
 
-exception Exit of int * constr
-
 (* [map_with_binders g f n c] maps [f n] on the immediate
    subterms of [c]; it carries an extra data [n] (typically a lift
    index) which is processed by [g] (which typically add 1 to [n]) at
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 31e86e854..dbe188bd4 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -82,8 +82,6 @@ let update_case_info cache ci modlist =
   with Not_found ->
     ci
 
-let empty_modlist = (Cmap.empty, Mindmap.empty)
-
 let is_empty_modlist (cm, mm) =
   Cmap.is_empty cm && Mindmap.is_empty mm
 
diff --git a/kernel/names.ml b/kernel/names.ml
index 3de12b1bc..f4779acb6 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -431,7 +431,6 @@ module KerPair = struct
     | Dual (kn,_) -> kn
 
   let same kn = Same kn
-  let dual knu knc = Dual (knu,knc)
   let make knu knc = if knu == knc then Same knc else Dual (knu,knc)
 
   let make1 = same
@@ -726,7 +725,6 @@ let label = KerName.label
 let string_of_kn = KerName.to_string
 let pr_kn = KerName.print
 let kn_ord = KerName.compare
-let kn_equal = KerName.equal
 
 (** Compatibility layer for [Constant] *)
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index c86c13e04..a084504dc 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -23,10 +23,6 @@ open Environ
 open Entries
 open Typeops
 
-let debug = false
-let prerr_endline =
-  if debug then prerr_endline else fun _ -> ()
-
 let constrain_type env j cst1 = function
   | `None ->
       make_polymorphic_if_constant_for_ind env j, cst1
diff --git a/kernel/vars.ml b/kernel/vars.ml
index cb22a2e2f..f23d5fc2c 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -104,7 +104,7 @@ let lift n = liftn n 1
 type info = Closed | Open | Unknown
 type 'a substituend = { mutable sinfo: info; sit: 'a }
 
-let rec lift_substituend depth s =
+let lift_substituend depth s =
   match s.sinfo with
     | Closed -> s.sit
     | Open -> lift depth s.sit
diff --git a/lib/cList.ml b/lib/cList.ml
index 385c80b62..36dad3235 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -306,8 +306,6 @@ let subtract cmp l1 l2 =
 let unionq l1 l2 = union (==) l1 l2
 let subtractq l1 l2 = subtract (==) l1 l2
 
-let tabulate = init
-
 let interval n m =
   let rec interval_n (l,m) =
     if n > m then l else interval_n (m::l, pred m)
diff --git a/lib/errors.ml b/lib/errors.ml
index 9b2e9370d..9df276465 100644
--- a/lib/errors.ml
+++ b/lib/errors.ml
@@ -19,17 +19,9 @@ exception Anomaly of string option * std_ppcmds (* System errors *)
 let make_anomaly ?label pp =
   Anomaly (label, pp)
 
-let anomaly_gen label pp =
-  raise (Anomaly (label, pp))
-
-let anomaly ?loc ?label pp =
-  match loc with
+let anomaly ?loc ?label pp = match loc with
   | None -> raise (Anomaly (label, pp))
-  | Some loc ->
-    Loc.raise loc (Anomaly (label, pp))
-
-let anomalylabstrm string pps =
-  anomaly_gen (Some string) pps
+  | Some loc -> Loc.raise loc (Anomaly (label, pp))
 
 let is_anomaly = function
 | Anomaly _ -> true
@@ -106,8 +98,6 @@ let print e =
     isn't printed (used in Ltac debugging). *)
 let print_no_report e = print_gen (print_anomaly false) !handle_stack e
 
-let print_anomaly e = print_anomaly true e
-
 (** Predefined handlers **)
 
 let _ = register_handler begin function
diff --git a/lib/flags.ml b/lib/flags.ml
index 91e28132a..3118901ac 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -179,14 +179,6 @@ let is_standard_doc_url url =
   url = Coq_config.wwwrefman ||
   url = wwwcompatprefix ^ String.sub Coq_config.wwwrefman n (n'-n)
 
-(* same as in System, but copied here because of dependencies *)
-let canonical_path_name p =
-  let current = Sys.getcwd () in
-  Sys.chdir p;
-  let result = Sys.getcwd () in
-  Sys.chdir current;
-  result
-
 (* Options for changing coqlib *)
 let coqlib_spec = ref false
 let coqlib = ref "(not initialized yet)"
diff --git a/lib/genarg.ml b/lib/genarg.ml
index 306cdbed8..89b6f23de 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -154,10 +154,6 @@ let has_type (t, v) u = argument_type_eq t u
 
 let unquote x = x
 
-type an_arg_of_this_type = Obj.t
-
-let in_generic t x = (t, Obj.repr x)
-
 type ('a,'b) abstract_argument_type = argument_type
 type 'a raw_abstract_argument_type = ('a,rlevel) abstract_argument_type
 type 'a glob_abstract_argument_type = ('a,glevel) abstract_argument_type
@@ -237,7 +233,7 @@ struct
 
   (** For now, the following function is quite dummy and should only be applied
       to an extra argument type, otherwise, it will badly fail. *)
-  let rec obj t = match t with
+  let obj t = match t with
   | ExtraArgType s -> Obj.magic (get_obj0 s)
   | _ -> assert false
 
diff --git a/lib/iArray.ml b/lib/iArray.ml
index 8dbe3f6c6..3cbee45b6 100644
--- a/lib/iArray.ml
+++ b/lib/iArray.ml
@@ -452,8 +452,6 @@ struct
 
 let get = M.get
 
-let set = M.set
-
 let of_array (t : 'a array) : 'a M.t =
   let tag = Obj.tag (Obj.repr t) in
   let () = if tag = Obj.double_array_tag then
diff --git a/lib/iStream.ml b/lib/iStream.ml
index 065155f08..da54d9f7b 100644
--- a/lib/iStream.ml
+++ b/lib/iStream.ml
@@ -26,7 +26,7 @@ let rec force s = match Lazy.force s with
 
 let force s = force s; s
 
-let rec is_empty s = match Lazy.force s with
+let is_empty s = match Lazy.force s with
 | Nil -> true
 | Cons (_, _) -> false
 
diff --git a/lib/int.ml b/lib/int.ml
index 43d6d037d..1403dc510 100644
--- a/lib/int.ml
+++ b/lib/int.ml
@@ -49,7 +49,6 @@ module List = struct
 end
 
 let min (i : int) j = if i < j then i else j
-let max (i : int) j = if i > j then i else j
 
 (** Utility function *)
 let rec next from upto =
@@ -83,7 +82,7 @@ struct
 
   let reroot t = rerootk t (fun () -> ())
 
-  let rec get t i =
+  let get t i =
   let () = assert (0 <= i) in
   match !t with
   | Root a ->
diff --git a/lib/serialize.ml b/lib/serialize.ml
index 92dcca2c5..386ab8e45 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -25,10 +25,6 @@ exception Marshal_error
 
 (** Utility functions *)
 
-let rec has_flag (f : string) = function
-  | [] -> false
-  | (k, _) :: l -> CString.equal k f || has_flag f l
-
 let rec get_attr attr = function
   | [] -> raise Not_found
   | (k, v) :: l when CString.equal k attr -> v
@@ -186,13 +182,6 @@ let to_state_id xml =
 let of_edit_or_state_id = function
   | Interface.Edit id -> ["object","edit"], of_edit_id id
   | Interface.State id -> ["object","state"], of_state_id id
-let to_edit_or_state_id attrs xml =
-  try
-    let obj = get_attr "object" attrs in
-    if obj = "edit"then Interface.Edit (to_edit_id xml)
-    else if obj = "state" then Interface.State (to_state_id xml)
-    else raise Marshal_error
-  with Not_found -> raise Marshal_error
 
 let of_value f = function
 | Good x -> Element ("value", ["val", "good"], [f x])
@@ -410,7 +399,6 @@ module ReifType : sig (* {{{ *)
   type value_type
   val erase         : 'a val_t -> value_type
   val print_type    : value_type -> string
-  val same_type     : 'a val_t -> value_type -> bool
 
   val document_type_encoding : (xml -> string) -> unit
 
@@ -432,7 +420,6 @@ end = struct
   type 'a val_t = value_type
   
   let erase (x : 'a val_t) : value_type = x
-  let same_type (x : 'a val_t) (y : value_type) = Pervasives.compare (erase x) y = 0
 
   let unit_t         = Unit
   let string_t       = String
diff --git a/lib/trie.ml b/lib/trie.ml
index a4a348c19..7efce9785 100644
--- a/lib/trie.ml
+++ b/lib/trie.ml
@@ -52,8 +52,6 @@ let labels (Node (_,m)) =
   (** FIXME: this is order-dependent. Try to find a more robust presentation? *)
   List.rev (T_codom.fold (fun x _ acc -> x::acc) m [])
 
-let in_dom (Node (_,m)) lbl = T_codom.mem lbl m
-
 let is_empty_node (Node(a,b)) = (X.is_nil a) && (T_codom.is_empty b)
 
 let assure_arc m lbl =
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index ca0a432d6..ce731c1eb 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -138,7 +138,6 @@ let iter_ref () =
 let iter = function () -> (constr_of_global (delayed_force iter_ref))
 let eq = function () -> (coq_base_constant "eq")
 let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS")
-let acc_intro_generator_function = function () -> (constant ["Recdef"] "Acc_intro_generator_function")
 let le_lt_n_Sm = function () -> (coq_base_constant "le_lt_n_Sm")
 let le_trans = function () -> (coq_base_constant "le_trans")
 let le_lt_trans = function () -> (coq_base_constant "le_lt_trans")
diff --git a/plugins/nsatz/polynom.ml b/plugins/nsatz/polynom.ml
index 78883a660..8566cf0d6 100644
--- a/plugins/nsatz/polynom.ml
+++ b/plugins/nsatz/polynom.ml
@@ -163,8 +163,6 @@ let max_var l = Array.fold_right (fun p m -> max (max_var_pol2 p) m) l 0
 
 (* equality between polynomials *)
 
-exception Failed
-
 let rec equal p q =
   match (p,q) with
       (Pint a,Pint b) -> C.equal a b
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index bdc4bc0ae..a96adcdd8 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -768,10 +768,6 @@ let filter_candidates evd evk filter candidates =
       let ids = set_of_evctx (Filter.filter_list filter (evar_context evi)) in
       Some (List.filter (fun a -> Id.Set.subset (collect_vars a) ids) l)
 
-let eq_filter f1 f2 =
-  let eq_bool b1 b2 = if b1 then b2 else not b2 in
-  List.equal eq_bool f1 f2
-
 let closure_of_filter evd evk = function
   | None -> None
   | Some filter ->
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 49ce29fdf..21a418943 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -176,41 +176,6 @@ let new_meta =
 
 let mk_new_meta () = mkMeta(new_meta())
 
-(** Transfer an evar from [sigma2] to [sigma1] *)
-let transfer ev (sigma1, sigma2) =
-  let nsigma1 = Evd.add sigma1 ev (Evd.find sigma2 ev) in
-  let nsigma2 = Evd.remove sigma2 ev in
-  (nsigma1, nsigma2)
-
-let collect_evars emap c =
-  let rec collrec acc c =
-    match kind_of_term c with
-      | Evar (evk,_) ->
-	  if Evd.is_undefined emap evk then Evar.Set.add evk acc
-	  else (* No recursion on the evar instantiation *) acc
-      | _         ->
-	  fold_constr collrec acc c in
-  collrec Evar.Set.empty c
-
-let push_dependent_evars sigma emap =
-  let fold ev {evar_concl = ccl} (sigma, emap) =
-    Evar.Set.fold transfer (collect_evars emap ccl) (sigma, emap)
-  in
-  Evd.fold_undefined fold emap (sigma, emap)
-
-let push_duplicated_evars sigma emap c =
-  let rec collrec (one, evars as acc) c =
-    match kind_of_term c with
-    | Evar (evk,_) when not (Evd.mem (fst evars) evk) ->
-	if List.exists (fun ev -> Evar.equal evk ev) one then
-	  (one, transfer evk evars)
-	else
-	  (evk::one, evars)
-    | _ ->
-	fold_constr collrec acc c
-  in
-  snd (collrec ([],(sigma,emap)) c)
-
 (* The list of non-instantiated existential declarations (order is important) *)
 
 let non_instantiated sigma =
@@ -221,8 +186,6 @@ let non_instantiated sigma =
 (* Manipulating filters *)
 (************************)
 
-let extract_subfilter = List.filter_with
-
 let make_pure_subst evi args =
   snd (List.fold_right
     (fun (id,b,c) (args,l) ->
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index cf08e6787..0b6c3197d 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -492,7 +492,7 @@ let apply_subst recfun env cst_l t stack =
     | _ -> recfun cst_l (substl env t, stack)
   in aux env cst_l t stack
 
-let rec stacklam recfun env t stack =
+let stacklam recfun env t stack =
 apply_subst (fun _ -> recfun) env [] t stack
 
 let beta_applist (c,l) =
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index a6a9a75c5..b16f000d4 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -48,7 +48,7 @@ let unsatisfiable_constraints env evd ev comp =
 
 let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m))
 
-let rec unsatisfiable_exception exn =
+let unsatisfiable_exception exn =
   match exn with
   | TypeClassError (_, UnsatisfiableConstraints _) -> true
   | _ -> false
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index adb2ba0d0..520eac8ab 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -286,8 +286,6 @@ let pr_raw_alias prc prlc prtac prpat =
   pr_alias_gen (pr_raw_generic prc prlc prtac prpat pr_reference)
 let pr_glob_alias prc prlc prtac prpat =
   pr_alias_gen (pr_glb_generic prc prlc prtac prpat)
-let pr_alias prc prlc prtac prpat =
-  pr_extend_gen (pr_top_generic prc prlc prtac prpat)
 
 (**********************************************************************)
 (* The tactic printer                                                 *)
@@ -1025,9 +1023,6 @@ let pr_glob_tactic env = pr_glob_tactic_level env ltop
 
 (** Registering *)
 
-let register_uniform_printer wit pr =
-  Genprint.register_print0 wit pr pr pr
-
 let () =
   let pr_bool b = if b then str "true" else str "false" in
   let pr_unit _ = str "()" in
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 7bb1ceaa0..430dfab4d 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -130,17 +130,7 @@ let pr_search a b pr_p = match a with
   | SearchRewrite c -> str"SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b
   | SearchAbout sl -> str"Search" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b
 
-let pr_locality_full = function
-  | None -> mt ()
-  | Some true -> str "Local" ++ spc ()
-  | Some false -> str "Global "++ spc ()
-
 let pr_locality local = if local then str "Local" ++ spc () else mt ()
-let pr_non_locality local = if local then mt () else str "Global" ++ spc ()
-let pr_section_locality local =
-  if Lib.sections_are_opened () && not local then str "Global "
-  else if not (Lib.sections_are_opened ()) && local then str "Local "
-  else mt ()
 
 let pr_explanation (e,b,f) =
   let a = match e with
diff --git a/printing/printer.ml b/printing/printer.ml
index ad154ec55..080037400 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -720,11 +720,6 @@ let pr_assumptionset env s =
     ] in
     prlist_with_sep fnl (fun x -> x) (Option.List.flatten assums)
 
-open Typeclasses
-
-let pr_instance i =
-  pr_global (instance_impl i)
-
 (** Inductive declarations *)
 
 open Termops
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 1116410dc..f283d0f33 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -57,7 +57,7 @@ let is_unification_error = function
 | UnsolvableImplicit _| AbstractionOverMeta _ -> true
 | _ -> false
 
-let rec catchable_exception = function
+let catchable_exception = function
   | Errors.UserError _ | TypeError _
   | RefinerError _ | Indrec.RecursionSchemeError _
   | Nametab.GlobalizationError _
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index ca760c456..68c2ed328 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -25,9 +25,6 @@ let delete_proof = Proof_global.discard
 let delete_current_proof = Proof_global.discard_current
 let delete_all_proofs = Proof_global.discard_all
 
-let set_undo _ = ()
-let get_undo _ = None
-
 let start_proof (id : Id.t) str hyps c ?init_tac terminator =
   let goals = [ (Global.env_of_context hyps , c) ] in
   Proof_global.start_proof id str goals terminator;
@@ -132,11 +129,6 @@ let build_constant_by_tactic id sign ?(goal_kind = Global,Proof Theorem) typ tac
     delete_current_proof ();
     raise reraise
 
-let constr_of_def = function
-  | Declarations.Undef _ -> assert false
-  | Declarations.Def cs -> Mod_subst.force_constr cs
-  | Declarations.OpaqueDef lc -> Opaqueproof.force_proof lc
-
 let build_by_tactic env typ tac =
   let id = Id.of_string ("temporary_proof"^string_of_int (next())) in
   let sign = val_of_named_context (named_context env) in
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index f5431daaa..3cdecb633 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -115,32 +115,12 @@ let _ = Errors.register_handler begin function
   | NoSuchProof -> Errors.error "No such proof."
   | _ -> raise Errors.Unhandled
 end
-let extract id l =
-  let rec aux = function
-    | ({pid = id' } as np)::l when Id.equal id id' -> (np,l)
-    | np::l -> let (np', l) = aux l in (np' , np::l)
-    | [] -> raise NoSuchProof
-  in
-  let (np,l') = aux !l in
-  l := l';
-  update_proof_mode ();
-  np
 
 exception NoCurrentProof
 let _ = Errors.register_handler begin function
   | NoCurrentProof -> Errors.error "No focused proof (No proof-editing in progress)."
   | _ -> raise Errors.Unhandled
 end
-let extract_top l =
-  match !l with
-  | np::l' -> l := l' ; update_proof_mode (); np
-  | [] -> raise NoCurrentProof
-
-(* combinators for the proof_info map *)
-let add id info m =
-  m := Id.Map.add id info !m
-let remove id m =
-  m := Id.Map.remove id !m
 
 (*** Proof Global manipulation ***)
 
@@ -233,12 +213,6 @@ let activate_proof_mode mode =
 let disactivate_proof_mode mode =
   Ephemeron.iter_opt (find_proof_mode mode) (fun x -> x.reset ())
 
-exception AlreadyExists
-let _ = Errors.register_handler begin function
-  | AlreadyExists -> Errors.error "Already editing something of that name."
-  | _ -> raise Errors.Unhandled
-end
-
 (** [start_proof id str goals terminator] starts a proof of name [id]
     with goals [goals] (a list of pairs of environment and
     conclusion); [str] describes what kind of theorem/definition this
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 0635f03d0..47d63e2eb 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -121,10 +121,6 @@ val set_interp_tac :
 val set_used_variables : Names.Id.t list -> unit
 val get_used_variables : unit -> Context.section_context option
 
-val discard : Names.identifier Loc.located -> unit
-val discard_current : unit -> unit
-val discard_all : unit -> unit
-
 (**********************************************************)
 (*                                                        *)
 (*                            Proof modes                 *)
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 76af0c1e0..1365fe86e 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -223,7 +223,7 @@ let apply env t sp =
 (*** tacticals ***)
 
 
-let rec catchable_exception = function
+let catchable_exception = function
   | Proof_errors.Exception _ -> false
   | e -> Errors.noncritical e
 
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 3c3bb3970..609428792 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -98,10 +98,6 @@ let thensi_tac tac (sigr,gs) =
 
 let then_tac tac = thensf_tac [||] tac
 
-let non_existent_goal n =
-  errorlabstrm ("No such goal: "^(string_of_int n))
-    (str"Trying to apply a tactic to a non existent goal")
-
 (* [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls]
    applies the tactic [tac1] to [gls] then, applies [t1], ..., [tn] to
    the first [n] resulting subgoals, [t'1], ..., [t'm] to the last [m]
@@ -370,11 +366,6 @@ let tactic_list_tactic tac gls =
 (* Change evars *)
 let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma}
 
-(* Pretty-printers. *)
-
-let pp_info = ref (fun _ _ _ -> assert false)
-let set_info_printer f = pp_info := f
-
 (* Check that holes in arguments have been resolved *)
 
 let check_evars env sigma extsigma origsigma =
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 795582f27..45f92a97f 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -10,7 +10,6 @@ open Pp
 open Errors
 open Util
 open Names
-open Nameops
 open Namegen
 open Term
 open Vars
@@ -1420,9 +1419,6 @@ let possible_resolve dbg mod_delta db_list local_db cl =
 	(my_find_search mod_delta db_list local_db head cl)
   with Not_found -> []
 
-let dbg_case dbg id =
-  new_tclLOG dbg (fun () -> str "case " ++ pr_id id) (simplest_case (mkVar id))
-
 let extend_local_db gl decl db =
   Hint_db.add_list (make_resolve_hyp (pf_env gl) (project gl) decl) db
 
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index c33e5fb7c..6d7c797af 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -28,13 +28,9 @@ open Proofview.Notations
 
 (** Hint database named "typeclass_instances", now created directly in Auto *)
 
-let typeclasses_db = Auto.typeclasses_db
-
 let typeclasses_debug = ref false
 let typeclasses_depth = ref None
 
-exception Found of evar_map
-
 (** We transform the evars that are concerned by this resolution
     (according to predicate p) into goals.
     Invariant: function p only manipulates and returns undefined evars *)
@@ -191,13 +187,10 @@ let e_possible_resolve db_list local_db gl =
       (fst (head_constr_bound gl)) false gl
   with Bound | Not_found -> []
 
-let rec catchable = function
+let catchable = function
   | Refiner.FailError _ -> true
   | e -> Logic.catchable_exception e
 
-let nb_empty_evars s =
-  Evar.Map.cardinal (undefined_map s)
-
 let pr_ev evs ev = Printer.pr_constr_env (Goal.V82.env evs ev) (Evarutil.nf_evar evs (Goal.V82.concl evs ev))
 
 let pr_depth l = prlist_with_sep (fun () -> str ".") int (List.rev l)
@@ -316,15 +309,6 @@ let normevars_tac : atac =
     let info' = { info with auto_last_tac = lazy (str"normevars") } in
       sk {it = [gl', info']; sigma = sigma';} fk }
 
-(* Ordering of states is lexicographic on the number of remaining goals. *)
-let compare (pri, _, _, res) (pri', _, _, res') =
-  let nbgoals s =
-    List.length (sig_it s) + nb_empty_evars (sig_sig s)
-  in
-  let pri = pri - pri' in
-    if not (Int.equal pri 0) then pri
-    else nbgoals res - nbgoals res'
-
 let or_tac (x : 'a tac) (y : 'a tac) : 'a tac =
   { skft = fun sk fk gls -> x.skft sk (fun () -> y.skft sk fk gls) gls }
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 2854d1019..ff94937db 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -256,7 +256,6 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim =
 *)
 
 let (forward_general_rewrite_clause, general_rewrite_clause) = Hook.make ()
-let (forward_is_applied_rewrite_relation, is_applied_rewrite_relation) = Hook.make ()
 
 (* Do we have a JMeq instance on twice the same domains ? *)
 
diff --git a/tactics/equality.mli b/tactics/equality.mli
index e8b142d89..681b366db 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -9,7 +9,6 @@
 (*i*)
 open Names
 open Term
-open Context
 open Evd
 open Environ
 open Tacmach
@@ -43,9 +42,8 @@ val rewriteRL : ?tac:(unit Proofview.tactic * conditions) -> constr  -> unit Pro
 (* Warning: old [general_rewrite_in] is now [general_rewrite_bindings_in] *)
 
 val general_rewrite_clause :
-  (Id.t option -> orientation ->
-    occurrences -> constr with_bindings -> new_goals:constr list -> unit Proofview.tactic) Hook.t
-val is_applied_rewrite_relation : (env -> evar_map -> rel_context -> constr -> constr option) Hook.t
+  (Id.t option -> orientation -> occurrences -> constr with_bindings ->
+   new_goals:constr list -> unit Proofview.tactic) Hook.t
 
 val general_rewrite_ebindings_clause : Id.t option ->
   orientation -> occurrences -> freeze_evars_flag -> dep_proof_flag ->
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 79a1a41c8..ae73d7a41 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -18,7 +18,6 @@ open Reduction
 open Tacticals
 open Tacmach
 open Tactics
-open Patternops
 open Clenv
 open Typeclasses
 open Typeclasses_errors
@@ -127,10 +126,6 @@ let new_cstr_evar (evd,cstrs) env t =
   let evd', t = Evarutil.new_evar evd env t in
     (evd', Evar.Set.add (fst (destEvar t)) cstrs), t
 
-let new_goal_evar (evd,cstrs) env t =
-  let evd', t = Evarutil.new_evar evd env t in
-    (evd', cstrs), t
-
 (** Building or looking up instances. *)
 
 let proper_proof env evars carrier relation x =
@@ -225,9 +220,6 @@ let is_applied_rewrite_relation env sigma rels t =
 	  with e when Errors.noncritical e -> None)
   | _ -> None
 
-let _ =
-  Hook.set Equality.is_applied_rewrite_relation is_applied_rewrite_relation
-
 let rec decompose_app_rel env evd t =
   match kind_of_term t with
   | App (f, args) ->
@@ -541,10 +533,6 @@ type 'a pure_strategy = 'a -> Environ.env -> Id.t list -> constr -> types ->
 
 type strategy = unit pure_strategy
 
-let get_rew_rel r = match r.rew_prf with
-  | RewPrf (rel, prf) -> rel
-  | RewCast c -> mkApp (Coqlib.build_coq_eq (), [| r.rew_car; r.rew_from; r.rew_to |])
-
 let get_rew_prf r = match r.rew_prf with
   | RewPrf (rel, prf) -> rel, prf
   | RewCast c ->
@@ -717,12 +705,6 @@ let fold_match ?(force=false) env sigma c =
   in
     sk, (if exists then env else reset_env env), app, eff
 
-let fold_match_tac c gl =
-  let _, _, c', eff = fold_match ~force:true (pf_env gl) (project gl) c in
-   tclTHEN (Tactics.emit_side_effects eff)
-    (change (Some (snd (pattern_of_constr (project gl) c))) c' onConcl) gl
-
-
 let unfold_match env sigma sk app =
   match kind_of_term app with
   | App (f', args) when eq_constr f' (mkConst sk) ->
@@ -1044,23 +1026,6 @@ module Strategies =
 	      state, Info { rew_car = ty; rew_from = t; rew_to = t';
 			   rew_prf = RewCast ckind; rew_evars = evars }
 
-    let fold c : 'a pure_strategy =
-      fun state env avoid t ty cstr evars ->
-(* 	let sigma, (c,_) = Tacinterp.interp_open_constr_with_bindings is env (goalevars evars) c in *)
-	let sigma, c = Constrintern.interp_open_constr (goalevars evars) env c in
-	let unfolded =
-	  try Tacred.try_red_product env sigma c
-	  with e when Errors.noncritical e ->
-            error "fold: the term is not unfoldable !"
-	in
-	  try
-	    let sigma = Unification.w_unify env sigma CONV ~flags:Unification.elim_flags unfolded t in
-	    let c' = Evarutil.nf_evar sigma c in
-	      state, Info { rew_car = ty; rew_from = t; rew_to = c';
-			   rew_prf = RewCast DEFAULTcast;
-			   rew_evars = sigma, cstrevars evars }
-	  with e when Errors.noncritical e -> state, Fail
-
     let fold_glob c : 'a pure_strategy =
       fun state env avoid t ty cstr evars ->
 (* 	let sigma, (c,_) = Tacinterp.interp_open_constr_with_bindings is env (goalevars evars) c in *)
@@ -1115,10 +1080,6 @@ let solve_constraints env evars =
 let nf_zeta =
   Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
 
-let map_rewprf f = function
-  | RewPrf (rel, prf) -> RewPrf (f rel, f prf)
-  | RewCast c -> RewCast c
-
 exception RewriteFailure of std_ppcmds
 
 type result = (evar_map * constr option * types) rewrite_result
@@ -1215,8 +1176,6 @@ let cl_rewrite_clause_tac ?abs strat clause gl =
 let bind_gl_info f =
   bind concl (fun c -> bind env (fun v -> bind defs (fun ev -> f c v ev)))
 
-let fail l s = Refiner.tclFAIL l s
-
 let new_refine c : Goal.subgoals Goal.sensitive =
   let refable = Goal.Refinable.make
     (fun handle -> Goal.Refinable.constr_of_open_constr handle true c)
@@ -1329,14 +1288,6 @@ let cl_rewrite_clause_strat strat clause =
 let cl_rewrite_clause l left2right occs clause gl =
   cl_rewrite_clause_strat (rewrite_with left2right (general_rewrite_unif_flags ()) l occs) clause gl
 
-
-let occurrences_of = function
-  | n::_ as nl when n < 0 -> (false,List.map abs nl)
-  | nl ->
-      if List.exists (fun n -> n < 0) nl then
-	error "Illegal negative occurrence number.";
-      (true,nl)
-
 let apply_glob_constr c l2r occs = fun () env avoid t ty cstr evars ->
   let evd, c = (Pretyping.understand_tcc (goalevars evars) env c) in
     apply_lemma l2r (general_rewrite_unif_flags ()) (c, NoBindings)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 60564dbdb..830fbd2d4 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -423,7 +423,7 @@ let rec intropattern_ids (loc,pat) = match pat with
   | IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _
   | IntroForthcoming _ -> []
 
-let rec extract_ids ids lfun =
+let extract_ids ids lfun =
   let fold id v accu =
     let v = Value.normalize v in
     if has_type v (topwit wit_intro_pattern) then
diff --git a/tactics/tacticMatching.ml b/tactics/tacticMatching.ml
index 85108f8ed..b11841a65 100644
--- a/tactics/tacticMatching.ml
+++ b/tactics/tacticMatching.ml
@@ -215,9 +215,6 @@ module PatternMatching (E:StaticEnvironment) = struct
   (** Declares a substitution. *)
   let put_subst subst : unit m = put subst empty_context_subst empty_term_subst
 
-  (** Declares a context substitution. *)
-  let put_context context : unit m = put empty_subst context empty_term_subst
-
   (** Declares a term substitution. *)
   let put_terms terms : unit m = put empty_subst empty_context_subst terms
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index fda84e6f5..cb7a7b0d9 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -67,14 +67,11 @@ let typ_of = Retyping.get_type_of
 (* Option for 8.2 compatibility *)
 open Goptions
 let dependent_propositions_elimination = ref true
-let tactic_compat_context = ref false
 
 let use_dependent_propositions_elimination () =
   !dependent_propositions_elimination
   && Flags.version_strictly_greater Flags.V8_2
 
-let use_tactic_context_compat () = !tactic_compat_context
-
 let _ =
   declare_bool_option
     { optsync  = true;
@@ -172,7 +169,6 @@ let internal_cut_rev_gen b d t gl =
   with Evarutil.ClearDependencyError (id,err) ->
     error_clear_dependency (pf_env gl) id err
 
-let internal_cut_rev = internal_cut_rev_gen false
 let internal_cut_rev_replace = internal_cut_rev_gen true
 
 (* Moving hypotheses *)
@@ -348,7 +344,6 @@ let change chg c cls gl =
     cls gl
 
 (* Pour usage interne (le niveau User est pris en compte par reduce) *)
-let try_red_in_concl    = reduct_in_concl (try_red_product,REVERTcast)
 let red_in_concl        = reduct_in_concl (red_product,REVERTcast)
 let red_in_hyp          = reduct_in_hyp   red_product
 let red_option          = reduct_option   (red_product,REVERTcast)
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 580e37cdc..10c3092b4 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -57,7 +57,7 @@ let wrap_vernac_error exn strm =
   let e = EvaluatedError (hov 0 (str "Error:" ++ spc () ++ strm), None) in
   Exninfo.copy exn e
 
-let rec process_vernac_interp_error exn = match exn with
+let process_vernac_interp_error exn = match exn with
   | Univ.UniverseInconsistency (o,u,v,p) ->
     let pr_rel r =
       match r with
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 4d8a6d5d7..6c447e886 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -62,8 +62,6 @@ let existing_instance glob g pri =
 let mismatched_params env n m = mismatched_ctx_inst env Parameters n m
 let mismatched_props env n m = mismatched_ctx_inst env Properties n m
 
-type binder_list = (Id.t Loc.located * bool * constr_expr) list
-
 (* Declare everything in the parameters as implicit, and the class instance as well *)
 
 let type_ctx_instance evars env ctx inst subst =
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 29a1b3cf2..d4d40339c 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -416,9 +416,6 @@ type one_inductive_impls =
   Impargs.manual_explicitation list (* for inds *)*
   Impargs.manual_explicitation list list (* for constrs *)
 
-type one_inductive_expr =
-  lident * local_binder list * constr_expr option * constructor_expr list
-
 let do_mutual_inductive indl finite =
   let indl,coes,ntns = extract_mutual_inductive_declaration_components indl in
   (* Interpret the types *)
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 3bcf935cc..b930c4eec 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -250,7 +250,7 @@ let set_prompt prompt =
 
 (* The following exceptions need not be located. *)
 
-let rec locate_exn = function
+let locate_exn = function
   | Out_of_memory | Stack_overflow | Sys.Break -> false
   | _ -> true
 
@@ -325,12 +325,14 @@ let do_vernac () =
     exit the loop are Drop and Quit. Any other exception there indicates
     an issue with [print_toplevel_error] above. *)
 
+(*
 let feed_emacs = function
   | { Interface.id = Interface.State id;
       Interface.content = Interface.GlobRef (_,a,_,c,_) }  -> 
     prerr_endline ("<info>" ^"<id>"^Stateid.to_string id ^"</id>"
 		   ^a^" "^c^ "</info>")
   | _  -> ()
+*)
 
 let rec loop () =
   Sys.catch_break true;
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 303b3f8d6..b2f752dce 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -489,16 +489,6 @@ let explain_evar_kind env evi = function
   | Evar_kinds.MatchingVar _ ->
       assert false
 
-let explain_not_clean env sigma ev t k =
-  let t = Evarutil.nf_evar sigma t in
-  let env = make_all_name_different env in
-  let id = Evd.string_of_existential ev in
-  let var = pr_lconstr_env env t in
-  str "Tried to instantiate " ++ explain_evar_kind env None k ++
-  str " (" ++ str id ++ str ")" ++ spc () ++
-  str "with a term using variable " ++ var ++ spc () ++
-  str "which is not in its scope."
-
 let explain_unsolvability = function
   | None -> mt()
   | Some (SeveralInstancesFound n) ->
@@ -824,9 +814,6 @@ let explain_no_instance env (_,id) l =
   str "applied to arguments" ++ spc () ++
     pr_sequence (pr_lconstr_env env) l
 
-let is_goal_evar evi =
-  match evi.evar_source with (_, Evar_kinds.GoalEvar) -> true | _ -> false
-
 let pr_constraints printenv env evd evars cstrs =
   let (ev, evi) = Evar.Map.choose evars in
     if Evar.Map.for_all (fun ev' evi' ->
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 70410fc40..1b97a69ba 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -278,8 +278,6 @@ let set_options options =
   in
   List.iter iter options
 
-let mkcases s = Vernacentries.make_cases s
-
 let about () = {
   Interface.coqtop_version = Coq_config.version;
   Interface.protocol_version = Serialize.protocol_version;
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 43a0a43b4..761f9c214 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -104,11 +104,6 @@ let cons_production_parameter l = function
   | GramTerminal _ -> l
   | GramNonTerminal (_,_,_,ido) -> Option.List.cons ido l
 
-let rec tactic_notation_key = function
-  | GramTerminal id :: _ -> id
-  | _ :: l -> tactic_notation_key l
-  | [] -> "terminal_free_notation"
-
 let add_tactic_notation (local,n,prods,e) =
   let prods = List.map (interp_prod_item n) prods in
   let tags = make_tags prods in
@@ -404,9 +399,6 @@ let error_not_same_scope x y =
 (**********************************************************************)
 (* Build pretty-printing rules                                        *)
 
-type printing_precedence = int * parenRelation
-type parsing_precedence = int option
-
 let prec_assoc = function
   | RightA -> (L,E)
   | LeftA -> (E,L)
@@ -452,10 +444,6 @@ let is_operator s =
    s.[0] == '-' || s.[0] == '/' || s.[0] == '<' || s.[0] == '>' ||
    s.[0] == '@' || s.[0] == '\\' || s.[0] == '&' || s.[0] == '~' || s.[0] == '$')
 
-let is_prod_ident = function
-  | Terminal s when is_letter s.[0] || s.[0] == '_' -> true
-  | _ -> false
-
 let is_non_terminal = function
   | NonTerminal _ | SProdList _ -> true
   | _ -> false
diff --git a/toplevel/search.ml b/toplevel/search.ml
index 72528675c..38717850c 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -49,13 +49,6 @@ let iter_constructors indsp fn env nconstr =
     fn (ConstructRef (indsp, i)) env typ
   done
 
-let rec head_const c = match kind_of_term c with
-  | Prod (_,_,d) -> head_const d
-  | LetIn (_,_,_,d) -> head_const d
-  | App (f,_)   -> head_const f
-  | Cast (d,_,_)   -> head_const d
-  | _            -> c
-
 (* General search over declarations *)
 let iter_declarations (fn : global_reference -> env -> constr -> unit) =
   let env = Global.env () in
@@ -87,17 +80,6 @@ let iter_declarations (fn : global_reference -> env -> constr -> unit) =
 
 let generic_search = iter_declarations
 
-(* Fine Search. By Yves Bertot. *)
-
-let rec head c =
-  let c = strip_outer_cast c in
-  match kind_of_term c with
-  | Prod (_,_,c) -> head c
-  | LetIn (_,_,_,c) -> head c
-  | _              -> c
-
-let xor a b = (a || b) && (not (a && b))
-
 (** Standard display *)
 
 let plain_display accu ref a c =
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 667a60058..4ea9c2236 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -19,8 +19,6 @@ open Vernacexpr
    Use the module Coqtoplevel, which catches these exceptions
    (the exceptions are explained only at the toplevel). *)
 
-exception HasNotFailed
-
 (* The navigation vernac commands will be handled separately *)
 
 let rec is_navigation_vernac = function
@@ -43,30 +41,6 @@ let is_reset = function
   | VernacResetInitial | VernacResetName _ -> true
   | _ -> false
 
-(* For coqtop -time, we display the position in the file,
-   and a glimpse of the executed command *)
-
-let display_cmd_header loc com =
-  let shorten s =
-    try (String.sub s 0 30)^"..." with Invalid_argument _ -> s in
-  let noblank s =
-    for i = 0 to String.length s - 1 do
-      match s.[i] with
-	| ' ' | '\n' | '\t' | '\r' -> s.[i] <- '~'
-	| _ -> ()
-    done;
-    s
-  in
-  let (start,stop) = Loc.unloc loc in
-  let safe_pr_vernac x =
-    try Ppvernac.pr_vernac x
-    with e when Errors.noncritical e -> str (Printexc.to_string e) in
-  let cmd = noblank (shorten (string_of_ppcmds (safe_pr_vernac com)))
-  in
-  Pp.pp (str "Chars " ++ int start ++ str " - " ++ int stop ++
-	 str (" ["^cmd^"] "));
-  Pp.flush_all ()
-
 (* When doing Load on a file, two behaviors are possible:
 
    - either the history stack is grown by only one command,