Some dead code removal, thanks to Oug analyzer

 In particular, the unused lib/tlm.ml and lib/gset.ml are removed

 In addition, to simplify code, Libobject.record_object returning only the
 ('a->obj) function, which is enough almost all the time.
 Use Libobject.record_object_full if you really need also the (obj->'a).

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

16 files changed, 12 insertions, 344 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index fbdf8683e..17a2ea174 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -487,17 +487,7 @@ let subst_autohint (subst,(local,name,hintlist as obj)) =
 let classify_autohint ((local,name,hintlist) as obj) =
   if local or hintlist = (AddTactic []) then Dispose else Substitute obj
 
-let discharge_autohint (_,(local,name,hintlist as obj)) =
-  if local then None else
-    match hintlist with
-    | CreateDB _ ->
-	(* We assume that the transparent state is either empty or full *)
-	Some obj
-    | AddTransparency _ | AddTactic _ ->
-	(* Needs the adequate code here to support Global Hints in sections *)
-	None
-
-let (inAutoHint,_) =
+let inAutoHint =
   declare_object {(default_object "AUTOHINT") with
                     cache_function = cache_autohint;
 		    load_function = (fun _ -> cache_autohint);
@@ -953,8 +943,6 @@ let gen_trivial lems = function
   | None -> full_trivial lems
   | Some l -> trivial lems l
 
-let inj_open c = (Evd.empty,c)
-
 let h_trivial lems l =
   Refiner.abstract_tactic (TacTrivial (lems,l))
     (gen_trivial lems l)
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index c49787356..fb5b2f527 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -223,7 +223,7 @@ let classify_hintrewrite x = Libobject.Substitute x
 
 
 (* Declaration of the Hint Rewrite library object *)
-let (inHintRewrite,_)=
+let inHintRewrite =
   Libobject.declare_object {(Libobject.default_object "HINT_REWRITE") with
     Libobject.cache_function = cache_hintrewrite;
     Libobject.load_function = (fun _ -> cache_hintrewrite);
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index cb52ec5b9..36fa43ff2 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -45,18 +45,6 @@ let _ = Auto.auto_init := (fun () ->
 
 exception Found of evar_map
 
-let is_dependent ev evm =
-  Evd.fold (fun ev' evi dep ->
-    if ev = ev' then dep
-    else dep || occur_evar ev evi.evar_concl)
-    evm false
-
-let evar_filter evi =
-  let hyps' = evar_filtered_context evi in
-    { evi with 
-      evar_hyps = Environ.val_of_named_context hyps';
-      evar_filter = List.map (fun _ -> true) hyps' }
-
 let evars_to_goals p evm =
   let goals, evm' =
     Evd.fold
@@ -86,8 +74,6 @@ let e_give_exact flags c gl =
   let t1 = (pf_type_of gl c) in
     tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) gl
 
-let assumption flags id = e_give_exact flags (mkVar id)
-
 open Unification
 
 let auto_unif_flags = {
@@ -210,9 +196,6 @@ let rec catchable = function
   | Loc.Exc_located (_, e) -> catchable e
   | e -> Logic.catchable_exception e
 
-let is_ground gl =
-  Evarutil.is_ground_term (project gl) (pf_concl gl)
-
 let nb_empty_evars s =
   Evd.fold (fun ev evi acc -> if evi.evar_body = Evar_empty then succ acc else acc) s 0
 
@@ -296,10 +279,6 @@ let normevars_tac : atac =
   (*     in {it = gls'; sigma = s}) *)
 
 
-let id_tac : atac =
-  { skft = fun sk fk {it = gl; sigma = s} ->
-    sk {it = [gl]; sigma = s} fk }
-
 (* Ordering of states is lexicographic on the number of remaining goals. *)
 let compare (pri, _, _, res) (pri', _, _, res') =
   let nbgoals s =
@@ -312,16 +291,6 @@ let compare (pri, _, _, res) (pri', _, _, 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 }
 
-let solve_tac (x : 'a tac) : 'a tac =
-  { skft = fun sk fk gls -> x.skft (fun ({it = gls},_ as res) fk -> 
-    if gls = [] then sk res fk else fk ()) fk gls }
-
-let solve_unif_tac : atac =
-  { skft = fun sk fk {it = gl; sigma = s} -> 
-    try let s' = Evarconv.consider_remaining_unif_problems (Global.env ()) s in
-	  normevars_tac.skft sk fk ({it=gl; sigma=s'})
-    with _ -> fk () }
-
 let hints_tac hints =
   { skft = fun sk fk {it = gl,info; sigma = s} ->
     let possible_resolve (lgls as res, pri, b, pp) =
@@ -387,17 +356,6 @@ let evars_of_term c =
     | _ -> fold_constr evrec acc c
   in evrec Intset.empty c
 
-exception Found_evar of int
-
-let occur_evars evars c =
-  try
-    let rec evrec c =
-      match kind_of_term c with
-      | Evar (n, _) -> if Intset.mem n evars then raise (Found_evar n) else ()
-      | _ -> iter_constr evrec c
-    in evrec c; false
-  with Found_evar _ -> true
-
 let dependent only_classes evd oev concl =
   let concl_evars = Intset.union (evars_of_term concl)
     (Option.cata Intset.singleton Intset.empty oev)
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index f6f12b91b..d9addd1f0 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -220,7 +220,7 @@ let subst_dd (subst,(local,na,dd)) =
     d_pri = dd.d_pri;
     d_code = !forward_subst_tactic subst dd.d_code })
 
-let (inDD,_) =
+let inDD =
   declare_object {(default_object "DESTRUCT-HYP-CONCL-DATA") with
                     cache_function = cache_dd;
 		    open_function = (fun i o -> if i=1 then cache_dd o);
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index d2e45475e..fab8d2d45 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -410,19 +410,6 @@ let autounfold db cls gl =
     | OnConcl occs -> tac occs None)
     cls gl
 
-let autosimpl db cl =
-  let unfold_of_elts constr (b, elts) =
-    if not b then
-      List.map (fun c -> all_occurrences, constr c) elts
-    else []
-  in
-  let unfolds = List.concat (List.map (fun dbname ->
-    let db = searchtable_map dbname in
-    let (ids, csts) = Hint_db.transparent_state db in
-      unfold_of_elts (fun x -> EvalConstRef x) (Cpred.elements csts) @
-      unfold_of_elts (fun x -> EvalVarRef x) (Idpred.elements ids)) db)
-  in unfold_option unfolds cl
-
 open Extraargs
 
 TACTIC EXTEND autounfold
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 1a78a509f..1ff8800f1 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -109,12 +109,6 @@ let head_in gls indl t =
     in List.mem ity indl
   with Not_found -> false
 
-let inductive_of = function
-  | IndRef ity -> ity
-  | r ->
-      errorlabstrm "Decompose"
-        (Printer.pr_global r ++ str " is not an inductive type.")
-
 let decompose_these c l gls =
   let indl = (*List.map inductive_of*) l in
   general_decompose (fun (_,t) -> head_in gls indl t) c gls
@@ -134,8 +128,6 @@ let decompose_or c gls =
     (fun (_,t) -> is_disjunction t)
     c gls
 
-let inj_open c = (Evd.empty,c)
-
 let h_decompose l c =
   Refiner.abstract_tactic (TacDecompose (l,c)) (decompose_these c l)
 
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index fbf36c1c3..4fbe361e0 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -46,10 +46,6 @@ let optimize_non_type_induction_scheme kind dep sort ind =
 let build_induction_scheme_in_type dep sort ind =
   build_induction_scheme (Global.env()) Evd.empty ind dep sort
 
-let rect_scheme_kind_from_type =
-  declare_individual_scheme_object "_rect_nodep"
-    (build_induction_scheme_in_type false InType)
-
 let rect_scheme_kind_from_prop =
   declare_individual_scheme_object "_rect" ~aux:"_rect_from_prop"
     (build_induction_scheme_in_type false InType)
@@ -58,14 +54,6 @@ let rect_dep_scheme_kind_from_type =
   declare_individual_scheme_object "_rect" ~aux:"_rect_from_type"
     (build_induction_scheme_in_type true InType)
 
-let rect_dep_scheme_kind_from_prop =
-  declare_individual_scheme_object "_rect_dep"
-    (build_induction_scheme_in_type true InType)
-
-let ind_scheme_kind_from_type =
-  declare_individual_scheme_object "_ind_nodep"
-  (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InProp)
-
 let ind_scheme_kind_from_prop =
   declare_individual_scheme_object "_ind" ~aux:"_ind_from_prop"
   (optimize_non_type_induction_scheme rect_scheme_kind_from_prop false InProp)
@@ -74,14 +62,6 @@ let ind_dep_scheme_kind_from_type =
   declare_individual_scheme_object "_ind" ~aux:"_ind_from_type"
   (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_type true InProp)
 
-let ind_dep_scheme_kind_from_prop =
-  declare_individual_scheme_object "_ind_dep"
-  (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_prop true InProp)
-
-let rec_scheme_kind_from_type =
-  declare_individual_scheme_object "_rec_nodep"
-  (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InSet)
-
 let rec_scheme_kind_from_prop =
   declare_individual_scheme_object "_rec" ~aux:"_rec_from_prop"
   (optimize_non_type_induction_scheme rect_scheme_kind_from_prop false InSet)
@@ -90,10 +70,6 @@ let rec_dep_scheme_kind_from_type =
   declare_individual_scheme_object "_rec" ~aux:"_rec_from_type"
   (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_type true InSet)
 
-let rec_dep_scheme_kind_from_prop =
-  declare_individual_scheme_object "_rec_dep"
-  (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_prop true InSet)
-
 (* Case analysis *)
 
 let build_case_analysis_scheme_in_type dep sort ind =
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 3bf6c5824..49ff459c6 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -432,7 +432,7 @@ let cache_transitivity_lemma (_,(left,lem)) =
 
 let subst_transitivity_lemma (subst,(b,ref)) = (b,subst_mps subst ref)
 
-let (inTransitivity,_) =
+let inTransitivity =
   declare_object {(default_object "TRANSITIVITY-STEPS") with
     cache_function = cache_transitivity_lemma;
     open_function = (fun i o -> if i=1 then cache_transitivity_lemma o);
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 23d555f8d..c31980158 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -34,8 +34,6 @@ open Vernacexpr
 open Safe_typing
 open Decl_kinds
 
-let not_work_message = "tactic fails to build the inversion lemma, may be because the predicate has arguments that depend on other arguments"
-
 let no_inductive_inconstr env constr =
   (str "Cannot recognize an inductive predicate in " ++
      pr_lconstr_env env constr ++
@@ -86,18 +84,6 @@ let no_inductive_inconstr env constr =
 
  *)
 
-let thin_ids env (hyps,vars) =
-  fst
-    (List.fold_left
-       (fun ((ids,globs) as sofar) (id,c,a) ->
-          if List.mem id globs then
-	    match c with
-	      | None -> (id::ids,(global_vars env a)@globs)
-	      | Some body ->
-                  (id::ids,(global_vars env body)@(global_vars env a)@globs)
-          else sofar)
-       ([],vars) hyps)
-
 (* returns the sub_signature of sign corresponding to those identifiers that
  * are not global. *)
 (*
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index f79bfa0ff..3bed376ff 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -71,28 +71,20 @@ let try_find_reference dir s =
   constr_of_global (try_find_global_reference dir s)
 
 let gen_constant dir s = Coqlib.gen_constant "rewrite" dir s
-let coq_proj1 = lazy(gen_constant ["Init"; "Logic"] "proj1")
-let coq_proj2 = lazy(gen_constant ["Init"; "Logic"] "proj2")
 let coq_eq = lazy(gen_constant ["Init"; "Logic"] "eq")
-let coq_eq_rect = lazy (gen_constant ["Init"; "Logic"] "eq_rect")
 let coq_f_equal = lazy (gen_constant ["Init"; "Logic"] "f_equal")
-let iff = lazy (gen_constant ["Init"; "Logic"] "iff")
 let coq_all = lazy (gen_constant ["Init"; "Logic"] "all")
 let impl = lazy (gen_constant ["Program"; "Basics"] "impl")
 let arrow = lazy (gen_constant ["Program"; "Basics"] "arrow")
-let coq_id = lazy (gen_constant ["Init"; "Datatypes"] "id")
 
 let reflexive_type = lazy (try_find_reference ["Classes"; "RelationClasses"] "Reflexive")
-let reflexive_proof_global = lazy (try_find_global_reference ["Classes"; "RelationClasses"] "reflexivity")
 let reflexive_proof = lazy (try_find_reference ["Classes"; "RelationClasses"] "reflexivity")
 
 let symmetric_type = lazy (try_find_reference ["Classes"; "RelationClasses"] "Symmetric")
 let symmetric_proof = lazy (try_find_reference ["Classes"; "RelationClasses"] "symmetry")
-let symmetric_proof_global = lazy (try_find_global_reference ["Classes"; "RelationClasses"] "symmetry")
 
 let transitive_type = lazy (try_find_reference ["Classes"; "RelationClasses"] "Transitive")
 let transitive_proof = lazy (try_find_reference ["Classes"; "RelationClasses"] "transitivity")
-let transitive_proof_global = lazy (try_find_global_reference ["Classes"; "RelationClasses"] "transitivity")
 
 let coq_inverse = lazy (gen_constant (* ["Classes"; "RelationClasses"] "inverse" *)
 			   ["Program"; "Basics"] "flip")
@@ -100,18 +92,14 @@ let coq_inverse = lazy (gen_constant (* ["Classes"; "RelationClasses"] "inverse"
 let inverse car rel = mkApp (Lazy.force coq_inverse, [| car ; car; mkProp; rel |])
 (* let inverse car rel = mkApp (Lazy.force coq_inverse, [| car ; car; new_Type (); rel |]) *)
 
-let complement = lazy (gen_constant ["Classes"; "RelationClasses"] "complement")
 let forall_relation = lazy (gen_constant ["Classes"; "Morphisms"] "forall_relation")
 let pointwise_relation = lazy (gen_constant ["Classes"; "Morphisms"] "pointwise_relation")
 
-let respectful_dep = lazy (gen_constant ["Classes"; "Morphisms"] "respectful_dep")
 let respectful = lazy (gen_constant ["Classes"; "Morphisms"] "respectful")
 
-let equivalence = lazy (gen_constant ["Classes"; "RelationClasses"] "Equivalence")
 let default_relation = lazy (gen_constant ["Classes"; "SetoidTactics"] "DefaultRelation")
 
 let subrelation = lazy (gen_constant ["Classes"; "RelationClasses"] "subrelation")
-let is_subrelation = lazy (gen_constant ["Classes"; "RelationClasses"] "is_subrelation")
 let do_subrelation = lazy (gen_constant ["Classes"; "Morphisms"] "do_subrelation")
 let apply_subrelation = lazy (gen_constant ["Classes"; "Morphisms"] "apply_subrelation")
 
@@ -119,25 +107,13 @@ let coq_relation = lazy (gen_constant ["Relations";"Relation_Definitions"] "rela
 let mk_relation a = mkApp (Lazy.force coq_relation, [| a |])
 (* let mk_relation a = mkProd (Anonymous, a, mkProd (Anonymous, a, new_Type ())) *)
 
-let coq_relationT = lazy (gen_constant ["Classes";"Relations"] "relationT")
-
-let setoid_refl_proj = lazy (gen_constant ["Classes"; "SetoidClass"] "Equivalence_Reflexive")
-
-let setoid_equiv = lazy (gen_constant ["Classes"; "SetoidClass"] "equiv")
-let setoid_proper = lazy (gen_constant ["Classes"; "SetoidClass"] "setoid_proper")
-let setoid_refl_proj = lazy (gen_constant ["Classes"; "SetoidClass"] "Equivalence_Reflexive")
-
 let rewrite_relation_class = lazy (gen_constant ["Classes"; "RelationClasses"] "RewriteRelation")
-let rewrite_relation = lazy (gen_constant ["Classes"; "RelationClasses"] "rewrite_relation")
 
 let arrow_morphism a b =
   if isprop a && isprop b then
     Lazy.force impl
   else Lazy.force arrow
 
-let setoid_refl pars x =
-  applistc (Lazy.force setoid_refl_proj) (pars @ [x])
-
 let proper_type = lazy (constr_of_global (Lazy.force proper_class).cl_impl)
 
 let proper_proxy_type = lazy (constr_of_global (Lazy.force proper_proxy_class).cl_impl)
@@ -165,10 +141,6 @@ let split_head = function
     hd :: tl -> hd, tl
   | [] -> assert(false)
 
-let new_goal_evar (goal,cstr) env t =
-  let goal', t = Evarutil.new_evar goal env t in
-    (goal', cstr), t
-
 let new_cstr_evar (goal,cstr) env t =
   let cstr', t = Evarutil.new_evar cstr env t in
     (goal, cstr'), t
@@ -311,15 +283,6 @@ let rewrite2_unif_flags = {
   Unification.modulo_eta = true
 }
 
-let setoid_rewrite_unif_flags = {
-  Unification.modulo_conv_on_closed_terms = Some conv_transparent_state;
-  Unification.use_metas_eagerly = true;
-  Unification.modulo_delta = conv_transparent_state;
-  Unification.resolve_evars = true;
-  Unification.use_evars_pattern_unification = true;
-  Unification.modulo_eta = true
-}
-
 let convertible env evd x y =
   Reductionops.is_conv env evd x y
 
@@ -385,11 +348,6 @@ let unfold_impl t =
 	mkProd (Anonymous, a, lift 1 b)
     | _ -> assert false
 
-let unfold_id t =
-  match kind_of_term t with
-    | App (id, [| a; b |]) (* when eq_constr id (Lazy.force coq_id) *) -> b
-    | _ -> assert false
-
 let unfold_all t =
   match kind_of_term t with
     | App (id, [| a; b |]) (* when eq_constr id (Lazy.force coq_all) *) ->
@@ -398,9 +356,6 @@ let unfold_all t =
 	  | _ -> assert false)
     | _ -> assert false
 
-let decomp_prod env evm n c =
-  snd (Reductionops.splay_prod_n env evm n c)
-
 let rec decomp_pointwise n c =
   if n = 0 then c
   else
@@ -1099,11 +1054,8 @@ let occurrences_of = function
 	error "Illegal negative occurrence number.";
       (true,nl)
 
-let pr_gen_strategy pr_id = Pp.mt ()
-let pr_loc_strategy _ _ _ = Pp.mt ()
 let pr_strategy _ _ _ (s : strategy) = Pp.str "<strategy>"
 
-let intern_strategy ist gl c = c
 let interp_strategy ist gl c = c
 let glob_strategy ist l = l
 let subst_strategy evm l = l
@@ -1119,7 +1071,7 @@ let interp_constr_list env sigma =
 
 open Pcoq
 
-let (wit_strategy, globwit_strategy, rawwit_strategy) =
+let _ =
   (Genarg.create_arg "strategy" :
       ((strategy, Genarg.tlevel) Genarg.abstract_argument_type *
 	  (strategy, Genarg.glevel) Genarg.abstract_argument_type *
@@ -1216,10 +1168,6 @@ let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
 let anew_instance binders instance fields =
   new_instance binders instance (CRecord (dummy_loc,None,fields)) ~generalize:false None
 
-let require_library dirpath =
-  let qualid = (dummy_loc, Libnames.qualid_of_dirpath (Libnames.dirpath_of_string dirpath)) in
-    Library.require_library [qualid] (Some false)
-
 let declare_instance_refl binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive"
   in anew_instance binders instance
@@ -1235,8 +1183,6 @@ let declare_instance_trans binders a aeq n lemma =
   in anew_instance binders instance
        [(Ident (dummy_loc,id_of_string "transitivity"),lemma)]
 
-let constr_tac = Tacinterp.interp (Tacexpr.TacAtom (dummy_loc, Tacexpr.TacAnyConstructor (false,None)))
-
 let declare_relation ?(binders=[]) a aeq n refl symm trans =
   init_setoid ();
   let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation"
@@ -1281,10 +1227,11 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans =
 
 type 'a binders_argtype = (local_binder list, 'a) Genarg.abstract_argument_type
 
-let (wit_binders : Genarg.tlevel binders_argtype),
-  (globwit_binders : Genarg.glevel binders_argtype),
-  (rawwit_binders : Genarg.rlevel binders_argtype) =
-  Genarg.create_arg "binders"
+let _, _, rawwit_binders =
+ (Genarg.create_arg "binders" :
+    Genarg.tlevel binders_argtype *
+    Genarg.glevel binders_argtype *
+    Genarg.rlevel binders_argtype)
 
 open Pcoq.Constr
 
@@ -1355,9 +1302,6 @@ VERNAC COMMAND EXTEND AddParametricRelation3
       [ declare_relation ~binders:b a aeq n None None (Some lemma3) ]
 END
 
-let mk_qualid s =
-  Libnames.Qualid (dummy_loc, Libnames.qualid_of_string s)
-
 let cHole = CHole (dummy_loc, None)
 
 open Entries
@@ -1599,15 +1543,6 @@ let general_s_rewrite_clause x =
 
 let _ = Equality.register_general_rewrite_clause general_s_rewrite_clause
 
-let is_loaded d =
-  let d' = List.map id_of_string d in
-  let dir = make_dirpath (List.rev d') in
-    Library.library_is_loaded dir
-
-let try_loaded f gl =
-  if is_loaded ["Coq";"Classes";"RelationClasses"] then f gl
-  else tclFAIL 0 (str"You need to require Coq.Classes.RelationClasses first") gl
-
 (** [setoid_]{reflexivity,symmetry,transitivity} tactics *)
 
 let not_declared env ty rel =
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index f067141a8..a2caec7c5 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -65,11 +65,6 @@ let skip_metaid = function
   | AI x -> x
   | MetaId (loc,_) -> error_syntactic_metavariables_not_allowed loc
 
-type ltac_type =
-  | LtacFun of ltac_type
-  | LtacBasic
-  | LtacTactic
-
 (* Values for interpretation *)
 type value =
   | VRTactic of (goal list sigma) (* For Match results *)
@@ -160,22 +155,6 @@ let valueOut = function
 
 (* To embed constr *)
 let constrIn t = CDynamic (dummy_loc,constr_in t)
-let constrOut = function
-  | CDynamic (_,d) ->
-    if (Dyn.tag d) = "constr" then
-      constr_out d
-    else
-      anomalylabstrm "constrOut" (str "Dynamic tag should be constr")
-  | ast ->
-    anomalylabstrm "constrOut" (str "Not a Dynamic ast")
-
-(* Globalizes the identifier *)
-let find_reference env qid =
-  (* We first look for a variable of the current proof *)
-  match repr_qualid qid with
-    | (d,id) when repr_dirpath d = [] & List.mem id (ids_of_context env)
-	-> VarRef id
-    | _ -> Nametab.locate qid
 
 (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *)
 let atomic_mactab = ref Idmap.empty
@@ -346,10 +325,6 @@ let intern_name l ist = function
   | Anonymous -> Anonymous
   | Name id -> Name (intern_ident l ist id)
 
-let vars_of_ist (lfun,_,_,env) =
-  List.fold_left (fun s id -> Idset.add id s)
-    (vars_of_env env) lfun
-
 let strict_check = ref false
 
 let adjust_loc loc = if !strict_check then dloc else loc
@@ -519,12 +494,6 @@ let intern_bindings ist = function
 let intern_constr_with_bindings ist (c,bl) =
   (intern_constr ist c, intern_bindings ist bl)
 
-let intern_clause_pattern ist (l,occl) =
-  let rec check = function
-    | (hyp,l) :: rest -> (intern_hyp ist (skip_metaid hyp),l)::(check rest)
-    | [] -> []
-  in (l,check occl)
-
   (* TODO: catch ltac vars *)
 let intern_induction_arg ist = function
   | ElimOnConstr c -> ElimOnConstr (intern_constr_with_bindings ist c)
@@ -994,14 +963,6 @@ and intern_genarg ist x =
 (***************************************************************************)
 (* Evaluation/interpretation *)
 
-let constr_to_id loc = function
-  | VConstr ([],c) when isVar c -> destVar c
-  | _ -> invalid_arg_loc (loc, "Not an identifier")
-
-let constr_to_qid loc c =
-  try shortest_qualid_of_global Idset.empty (global_of_constr c)
-  with _ -> invalid_arg_loc (loc, "Not a global reference")
-
 let is_variable env id =
   List.mem id (ids_of_named_context (Environ.named_context env))
 
@@ -1149,16 +1110,6 @@ let interp_hyp_list_as_list ist gl (loc,id as x) =
 let interp_hyp_list ist gl l =
   List.flatten (List.map (interp_hyp_list_as_list ist gl) l)
 
-let interp_clause_pattern ist gl (l,occl) =
-  let rec check acc = function
-    | (hyp,l) :: rest ->
-	let hyp = interp_hyp ist gl hyp in
-	if List.mem hyp acc then
-	  error ("Hypothesis "^(string_of_id hyp)^" occurs twice.");
-	(hyp,l)::(check (hyp::acc) rest)
-    | [] -> []
-  in (l,check [] occl)
-
 let interp_move_location ist gl = function
   | MoveAfter id -> MoveAfter (interp_hyp ist gl id)
   | MoveBefore id -> MoveBefore (interp_hyp ist gl id)
@@ -1396,8 +1347,6 @@ let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l =
 let interp_constr_list ist env sigma c =
   snd (interp_constr_in_compound_list (fun x -> x) (fun x -> x) (fun ist env sigma c -> (Evd.empty, interp_constr ist env sigma c)) ist env sigma c)
 
-let inj_open c = (Evd.empty,c)
-
 let interp_open_constr_list =
   interp_constr_in_compound_list (fun x -> x) (fun x -> x)
     (interp_open_constr None)
@@ -2888,11 +2837,6 @@ and subst_genarg subst (x:glob_generic_argument) =
 (***************************************************************************)
 (* Tactic registration *)
 
-(* For bad tactic calls *)
-let bad_tactic_args s =
-  anomalylabstrm s
-    (str "Tactic " ++ str s ++ str " called with bad arguments")
-
 (* Declaration of the TAC-DEFINITION object *)
 let add (kn,td) = mactab := Gmap.add kn td !mactab
 let replace (kn,td) = mactab := Gmap.add kn td (Gmap.remove kn !mactab)
@@ -2937,7 +2881,7 @@ let subst_md (subst,(local,defs)) =
 let classify_md (local,defs as o) =
   if local then Dispose else Substitute o
 
-let (inMD,outMD) =
+let inMD =
   declare_object {(default_object "TAC-DEFINITION") with
      cache_function  = cache_md;
      load_function   = load_md;
diff --git a/tactics/tactic_option.ml b/tactics/tactic_option.ml
index d0fa46c7a..1310fe7f9 100644
--- a/tactics/tactic_option.ml
+++ b/tactics/tactic_option.ml
@@ -25,7 +25,7 @@ let declare_tactic_option ?(default=Tacexpr.TacId []) name =
   let subst (s, (local, tac)) =
     (local, Tacinterp.subst_tactic s tac)
   in
-  let input, _output = 
+  let input =
     declare_object
       { (default_object name) with
 	cache_function = cache;
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 1108a7f2d..dc013fda6 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -171,12 +171,9 @@ let fullGoal gl = None :: List.map Option.make (pf_ids_of_hyps gl)
 
 let onAllHyps tac gl = tclMAP tac (pf_ids_of_hyps gl) gl
 let onAllHypsAndConcl tac gl = tclMAP tac (fullGoal gl) gl
-let onAllHypsAndConclLR tac gl = tclMAP tac (List.rev (fullGoal gl)) gl
 
 let tryAllHyps tac gl = tclFIRST_PROGRESS_ON tac (pf_ids_of_hyps gl) gl
 let tryAllHypsAndConcl tac gl = tclFIRST_PROGRESS_ON tac (fullGoal gl) gl
-let tryAllHypsAndConclLR tac gl =
-  tclFIRST_PROGRESS_ON tac (List.rev (fullGoal gl)) gl
 
 let onClause tac cl gls = tclMAP tac (simple_clause_of cl gls) gls
 let onClauseLR tac cl gls = tclMAP tac (List.rev (simple_clause_of cl gls)) gls
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 98904a59c..b030a09c3 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -117,7 +117,6 @@ val tryAllHypsAndConcl  : (identifier option -> tactic) -> tactic
 
 val onAllHyps           : (identifier -> tactic) -> tactic
 val onAllHypsAndConcl   : (identifier option -> tactic) -> tactic
-val onAllHypsAndConclLR : (identifier option -> tactic) -> tactic
 
 val onClause   : (identifier option -> tactic) -> clause -> tactic
 val onClauseLR : (identifier option -> tactic) -> clause -> tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 4a3001065..3876c6b35 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -75,21 +75,6 @@ let _ =
       optread  = (fun () -> !dependent_propositions_elimination) ;
       optwrite = (fun b -> dependent_propositions_elimination := b) }
 
-let apply_in_side_conditions_come_first = ref true
-
-let use_apply_in_side_conditions_come_first () =
-  !apply_in_side_conditions_come_first
-  && Flags.version_strictly_greater Flags.V8_2
-
-let _ =
-  declare_bool_option
-    { optsync  = true;
-      optname  = "apply-in side-conditions coming first";
-      optkey   = ["Side";"Conditions";"First";"For";"apply";"in"];
-      optread  = (fun () -> !dependent_propositions_elimination) ;
-      optwrite = (fun b -> dependent_propositions_elimination := b) }
-
-
 (*********************************************)
 (*                 Tactics                   *)
 (*********************************************)
@@ -163,7 +148,6 @@ let internal_cut_rev_replace = internal_cut_rev_gen true
 (* Moving hypotheses *)
 let move_hyp        = Tacmach.move_hyp
 
-let order_hyps      = Tacmach.order_hyps
 
 (* Renaming hypotheses *)
 let rename_hyp      = Tacmach.rename_hyp
@@ -340,16 +324,6 @@ let unfold_in_hyp   loccname = reduct_in_hyp   (unfoldn loccname)
 let unfold_option   loccname = reduct_option (unfoldn loccname,DEFAULTcast)
 let pattern_option l = reduct_option (pattern_occs l,DEFAULTcast)
 
-(* A function which reduces accordingly to a reduction expression,
-   as the command Eval does. *)
-
-let checking_fun = function
-  (* Expansion is not necessarily well-typed: e.g. expansion of t into x is
-     not well-typed in [H:(P t); x:=t |- G] because x is defined after H *)
-  | Fold _ -> with_check
-  | Pattern _ -> with_check
-  | _ -> (fun x -> x)
-
 (* The main reduction function *)
 
 let reduction_clause redexp cl =
@@ -455,7 +429,6 @@ let intro_using id = intro_gen dloc (IntroBasedOn (id,[])) no_move false false
 let intro = intro_gen dloc (IntroAvoid []) no_move false false
 let introf = intro_gen dloc (IntroAvoid []) no_move true false
 let intro_avoiding l = intro_gen dloc (IntroAvoid l) no_move false false
-let introf_move_name destopt = intro_gen dloc (IntroAvoid []) destopt true false
 
 (**** Multiple introduction tactics ****)
 
@@ -2164,23 +2137,6 @@ let make_up_names n ind_opt cname =
       else avoid in
   id_of_string base, hyprecname, avoid
 
-let is_indhyp p n t =
-  let l, c = decompose_prod t in
-  let c,_ = decompose_app c in
-  let p = p + List.length l in
-  match kind_of_term c with
-    | Rel k when p < k & k <= p + n -> true
-    | _ -> false
-
-let chop_context n l =
-  let rec chop_aux acc = function
-    | n, (_,Some _,_ as h :: t) -> chop_aux (h::acc) (n, t)
-    | 0, l2 -> (List.rev acc, l2)
-    | n, (h::t) -> chop_aux (h::acc) (n-1, t)
-    | _, [] -> anomaly "chop_context"
-  in
-  chop_aux [] (n,l)
-
 let error_ind_scheme s =
   let s = if s <> "" then s^" " else s in
   error ("Cannot recognize "^s^"an induction scheme.")
@@ -2213,8 +2169,6 @@ let lift_togethern n l =
       l ([], n)
   in l'
 
-let lift_together l = lift_togethern 0 l
-
 let lift_list l = List.map (lift 1) l
 
 let ids_of_constr ?(all=false) vars c =
@@ -2277,17 +2231,6 @@ let make_abstract_generalize gl id concl dep ctx body c eqs args refls =
   let appeqs = mkApp (instc, Array.of_list refls) in
     (* Finaly, apply the reflexivity proof for the original hyp, to get a term of type gl again. *)
     mkApp (appeqs, abshypt)
-      
-let deps_of_var id env =
-  Environ.fold_named_context
-    (fun _ (n,b,t) (acc : Idset.t) -> 
-      if Option.cata (occur_var env id) false b || occur_var env id t then
-	Idset.add n acc
-      else acc)
-    env ~init:Idset.empty
-    
-let idset_of_list =
-  List.fold_left (fun s x -> Idset.add x s) Idset.empty
 
 let hyps_of_vars env sign nogen hyps =
   if Idset.is_empty hyps then [] 
@@ -2491,33 +2434,6 @@ let occur_rel n c =
   let res = not (noccurn n c) in
   res
 
-let list_filter_firsts f l =
-  let rec list_filter_firsts_aux f acc l =
-    match l with
-      | e::l' when f e -> list_filter_firsts_aux f (acc@[e]) l'
-      | _ -> acc,l
-  in
-  list_filter_firsts_aux f [] l
-
-let count_rels_from n c =
-  let rels = free_rels c in
-  let cpt,rg = ref 0, ref n in
-  while Intset.mem !rg rels do
-    cpt:= !cpt+1; rg:= !rg+1;
-  done;
-  !cpt
-
-let count_nonfree_rels_from n c =
-  let rels = free_rels c in
-  if Intset.exists (fun x -> x >= n) rels then
-    let cpt,rg = ref 0, ref n in
-    while not (Intset.mem !rg rels) do
-      cpt:= !cpt+1; rg:= !rg+1;
-    done;
-    !cpt
-  else raise Not_found
-
-
 (* cuts a list in two parts, first of size n. Size must be greater than n *)
 let cut_list n l =
   let rec cut_list_aux acc n l =
@@ -3023,14 +2939,6 @@ let induction_without_atomization isrec with_evars elim names lid gl =
   then error "Not the right number of induction arguments."
   else induction_from_context_l with_evars elim_info lid names gl
 
-let enforce_eq_name id gl = function
-  | (b,(loc,IntroAnonymous)) ->
-      (b,(loc,IntroIdentifier (fresh_id [id] (add_prefix "Heq" id) gl)))
-  | (b,(loc,IntroFresh heq_base)) ->
-      (b,(loc,IntroIdentifier (fresh_id [id] heq_base gl)))
-  | x ->
-      x
-
 let has_selected_occurrences = function
   | None -> false
   | Some cls ->
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index ea9906d8d..b493d989b 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -266,8 +266,6 @@ let t_reduction_not = tacticIn reduction_not
 let intuition_gen tac =
   interp (tacticIn (tauto_intuit t_reduction_not tac))
 
-let simplif_gen = interp (tacticIn simplif)
-
 let tauto_intuitionistic g =
   try intuition_gen <:tactic<fail>> g
   with