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

1 files changed, 0 insertions, 42 deletions

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)