Some dead code removal + cleanups

  This commit concerns about the first half of the useless code
  mentionned by Oug for coqtop (without plugins). For the moment,
  Oug is used in a mode where any elements mentionned in a .mli
  is considered to be precious. This already allows to detect and
  remove about 600 lines, and more is still to come.

  Among the interesting points, the type Entries.specification_entry
  and its constructors SPExxx were never used. Large parts of cases.ml
  (and hence subtac_cases.ml) were also useless.

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

9 files changed, 3 insertions, 139 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index e7137787be..907995c542 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -61,8 +61,6 @@ type pri_auto_tactic = {
 
 type hint_entry = global_reference option * pri_auto_tactic
 
-let pri_ord {pri=pri1} {pri=pri2} = pri1 - pri2
-
 let pri_order {pri=pri1} {pri=pri2} = pri1 <= pri2
 
 let insert v l = 
@@ -116,19 +114,6 @@ let is_transparent_gr (ids, csts) = function
   | VarRef id -> Idpred.mem id ids
   | ConstRef cst -> Cpred.mem cst csts
   | IndRef _ | ConstructRef _ -> false
-      
-let fmt_autotactic =
-  function
-  | Res_pf (c,clenv) -> (str"apply " ++ pr_lconstr c)
-  | ERes_pf (c,clenv) -> (str"eapply " ++ pr_lconstr c)
-  | Give_exact c -> (str"exact " ++ pr_lconstr c)
-  | Res_pf_THEN_trivial_fail (c,clenv) -> 
-      (str"apply " ++ pr_lconstr c ++ str" ; trivial")
-  | Unfold_nth c -> (str"unfold " ++  pr_evaluable_reference c)
-  | Extern tac -> 
-      (str "(external) " ++ Pptactic.pr_glob_tactic (Global.env()) tac)
-
-let pr_autotactic = fmt_autotactic
 
 module Hint_db = struct
 
@@ -467,7 +452,7 @@ let classify_autohint (_,((local,name,hintlist) as obj)) =
 let export_autohint ((local,name,hintlist) as obj) =
   if local then None else Some obj
 
-let (inAutoHint,outAutoHint) =
+let (inAutoHint,_) =
   declare_object {(default_object "AUTOHINT") with
                     cache_function = cache_autohint;
 		    load_function = (fun _ -> cache_autohint);
@@ -714,9 +699,6 @@ let print_searchtable () =
 
 let priority l = List.filter (fun (_,hint) -> hint.pri = 0) l
 
-let select_unfold_extern =
-  List.filter (function (_,{code = (Unfold_nth _ | Extern _)}) -> true | _ -> false)
-
 (* tell auto not to reuse already instantiated metas in unification (for
    compatibility, since otherwise, apply succeeds oftener) *)
 
@@ -1081,10 +1063,6 @@ type autoArguments =
   | UsingTDB       
   | Destructing   
 
-let keepAfter tac1 tac2 = 
-  (tclTHEN tac1 
-     (function g -> tac2 [pf_last_hyp g] g))
-
 let compileAutoArg contac = function
   | Destructing -> 
       (function g -> 
@@ -1139,8 +1117,6 @@ let search_superauto n to_add argl g =
 let superauto n to_add argl  = 
   tclTRY (tclCOMPLETE (search_superauto n to_add argl))
 
-let default_superauto g = superauto !default_search_depth [] [] g
-
 let interp_to_add gl r =
   let r = Syntax_def.locate_global_with_alias (qualid_of_reference r) in
   let id = id_of_global r in
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 68c61bca04..f916e0a3ea 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -214,7 +214,7 @@ let classify_hintrewrite (_,x) = Libobject.Substitute x
 
 
 (* Declaration of the Hint Rewrite library object *)
-let (inHintRewrite,outHintRewrite)=
+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 c28f214c74..31ffc8897c 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -60,7 +60,6 @@ let e_give_exact flags c gl =
     else exact_check 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
diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml
index 2701566edf..02dace8377 100644
--- a/tactics/decl_interp.ml
+++ b/tactics/decl_interp.ml
@@ -182,11 +182,6 @@ let interp_constr_or_thesis check_sort sigma env = function
     Thesis n -> Thesis n
   | This c -> This (interp_constr check_sort sigma env c)
 
-let type_tester_var body typ = 
-  raw_app(dummy_loc,
-       RLambda(dummy_loc,Anonymous,Explicit,typ,
-	       RSort (dummy_loc,RProp Null)),body)
-
 let abstract_one_hyp inject h raw = 
   match h with 
       Hvar (loc,(id,None)) ->  
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index 967bc88e8c..ef2f77069d 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -487,9 +487,6 @@ let thus_tac c ctyp submetas gls =
 
 (* general forward step *)
 
-
-let anon_id_base = id_of_string "__" 
-
 let mk_stat_or_thesis info gls = function  
     This c -> c
   | Thesis (For _ ) -> 
@@ -843,12 +840,6 @@ let rec constr_trees (main_ind,wft) ind =
 	  constr_trees (None,itree) ind
     | _,constrs -> main_ind,constrs
 
-let constr_args rp constr =
-  let main_ind,constrs = constr_trees rp (fst constr) in
-  let ctree = constrs.(pred (snd constr)) in
-    array_map_to_list (fun t -> main_ind,t) 
-      (snd (Rtree.dest_node ctree))
-
 let ind_args rp ind =
     let main_ind,constrs = constr_trees rp ind in
     let args ctree =     
@@ -1212,8 +1203,6 @@ let pop_one (id,stack) =
 let pop_stacks stacks =
   List.map pop_one stacks
 
-let patvar_base = id_of_string "__"
-
 let hrec_for fix_id per_info gls obj_id =
   let obj=mkVar obj_id in
   let typ=pf_get_hyp_typ gls obj_id in
@@ -1392,15 +1381,6 @@ let end_tac et2 gls =
 
 (* escape *)
 
-let rec abstract_metas n avoid head = function
-    [] -> 1,head,[]
-  | (meta,typ)::rest -> 
-      let id = next_ident_away (id_of_string "_sbgl") avoid in
-      let p,term,args = abstract_metas (succ n) (id::avoid) head rest in 
-	succ p,mkLambda(Name id,typ,subst_meta [meta,mkRel p] term),
-      (mkMeta n)::args 
-
-    
 let escape_tac gls =  tcl_erase_info gls
 
 (* General instruction engine *)
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index 35d2e13244..b37212d9d6 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -175,10 +175,6 @@ let init () = Nbtermdn.empty tactab
 let freeze () = Nbtermdn.freeze tactab
 let unfreeze fs = Nbtermdn.unfreeze fs tactab
 
-let rollback f x =
-  let fs = freeze() in 
-  try f x with e -> (unfreeze fs; raise e)
-
 let add (na,dd) =
   let pat = match dd.d_pat with
     | HypLocation(_,p,_) -> p.d_typ
@@ -202,8 +198,6 @@ let _ =
 let forward_subst_tactic = 
   ref (fun _ -> failwith "subst_tactic is not installed for DHyp")
 
-let set_extern_subst_tactic f = forward_subst_tactic := f
-
 let cache_dd (_,(_,na,dd)) =
   try 
     add (na,dd)
@@ -223,7 +217,7 @@ let subst_dd (_,subst,(local,na,dd)) =
     d_pri = dd.d_pri; 
     d_code = !forward_subst_tactic subst dd.d_code })
 
-let (inDD,outDD) =
+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);
@@ -330,7 +324,6 @@ let destructHyp discard id gls =
   let sorted_ddl = Sort.list (fun dd1 dd2 -> dd1.d_pri > dd2.d_pri) ddl in
   tclFIRST (List.map (applyDestructor (onHyp id) discard) sorted_ddl) gls
 
-let cDHyp id gls = destructHyp true id gls
 let dHyp id gls = destructHyp false id gls
 
 let h_destructHyp b id =
@@ -349,8 +342,6 @@ let dConcl gls =
 
 let h_destructConcl = abstract_tactic TacDestructConcl dConcl
 
-let to2Lists (table : t) = Nbtermdn.to2lists table
-
 let rec search n =
   if n=0 then error "Search has reached zero.";
   tclFIRST
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 5e4f847fa8..09fc808c62 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -207,8 +207,6 @@ let e_possible_resolve mod_delta db_list local_db gl =
 	(fst (head_constr_bound gl)) gl)
   with Bound | Not_found -> []
 
-let assumption_tac_list id = apply_tac_list (e_give_exact_constr (mkVar id))
-
 let find_first_goal gls = 
   try first_goal gls with UserError _ -> assert false
 
@@ -324,8 +322,6 @@ let make_initial_state n gl dblist localdb =
     dblist = dblist;
     localdb = [localdb] }
 
-let debug_depth_first = Search.debug_depth_first
-
 let e_depth_search debug p db_list local_db gl =
   try
     let tac = if debug then Search.debug_depth_first else Search.depth_first in
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 99767afc07..99216a127d 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -84,11 +84,6 @@ let register_general_setoid_rewrite_clause = (:=) general_setoid_rewrite_clause
 let is_applied_setoid_relation = ref (fun _ -> false)
 let register_is_applied_setoid_relation = (:=) is_applied_setoid_relation
 
-let is_applied_relation t =
-  match kind_of_term t with
-  | App (c, args) when Array.length args >= 2 -> true
-  | _ -> false
-
 (* find_elim determines which elimination principle is necessary to
    eliminate lbeq on sort_of_gl. *)
 
@@ -230,24 +225,14 @@ let conditional_rewrite lft2rgt tac (c,bl) =
     (general_rewrite_ebindings lft2rgt all_occurrences (c,bl) false)
     [|tclIDTAC|] (tclCOMPLETE tac)
 
-let rewriteLR_bindings = general_rewrite_bindings true all_occurrences
-let rewriteRL_bindings = general_rewrite_bindings false all_occurrences
-
 let rewriteLR = general_rewrite true all_occurrences
 let rewriteRL = general_rewrite false all_occurrences
 
-let rewriteLRin_bindings = general_rewrite_bindings_in true all_occurrences
-let rewriteRLin_bindings = general_rewrite_bindings_in false all_occurrences
-
 let conditional_rewrite_in lft2rgt id tac (c,bl) = 
   tclTHENSFIRSTn
     (general_rewrite_ebindings_in lft2rgt all_occurrences id (c,bl) false)
     [|tclIDTAC|] (tclCOMPLETE tac)
 
-let rewriteRL_clause = function
-  | None -> rewriteRL_bindings
-  | Some id -> rewriteRLin_bindings id
-
 (* Replacing tactics *)
 
 (* eq,sym_eq : equality on Type and its symmetry theorem
@@ -973,10 +958,6 @@ let dEqThen with_evars ntac = function
 
 let dEq with_evars = dEqThen with_evars (fun x -> tclIDTAC)
 
-let rewrite_msg = function 
-  | None -> str "passed term is not a primitive equality" 
-  | Some id -> pr_id id ++ str "does not satisfy preconditions "
-
 let swap_equands gls eqn =
   let (lbeq,(t,e1,e2)) = find_eq_data_decompose eqn in 
   applist(lbeq.eq,[t;e2;e1])
@@ -986,10 +967,6 @@ let swapEquandsInConcl gls =
   let sym_equal = lbeq.sym in
   refine (applist(sym_equal,[t;e2;e1;Evarutil.mk_new_meta()])) gls
 
-let swapEquandsInHyp id gls =
-  cut_replacing id (swap_equands gls (pf_get_hyp_typ gls id))
-    (tclTHEN swapEquandsInConcl) gls
-
 (* Refine from [|- P e2] to [|- P e1] and [|- e1=e2:>t] (body is P (Rel 1)) *)
 
 let bareRevSubstInConcl lbeq body (t,e1,e2) gls =
@@ -1278,49 +1255,4 @@ let replace_multi_term dir_opt c  =
   in 
   rewrite_multi_assumption_cond cond_eq_fun 
 
-(* JF. old version 
-let rewrite_assumption_cond faildir gl =
-   let rec arec = function
-      | [] -> error "No such assumption."
-      | (id,_,t)::rest ->
-	  (try let dir = faildir t gl in
-	       general_rewrite dir (mkVar id) gl
-	   with Failure _ | UserError _  ->  arec rest)
-   in arec (pf_hyps gl)
-
-
-let rewrite_assumption_cond_in faildir hyp gl =
-   let rec arec = function
-      | [] -> error "No such assumption."
-      | (id,_,t)::rest ->
-	  (try let dir = faildir t gl in
-	       general_rewrite_in dir hyp (mkVar id) gl
-	   with Failure _ | UserError _ ->  arec rest)
-   in arec (pf_hyps gl)
-
-let replace_term_left t = rewrite_assumption_cond (cond_eq_term_left t)
-
-let replace_term_right t = rewrite_assumption_cond (cond_eq_term_right t)
-   
-let replace_term t = rewrite_assumption_cond (cond_eq_term t)
-   
-let replace_term_in_left t = rewrite_assumption_cond_in (cond_eq_term_left t)
-
-let replace_term_in_right t = rewrite_assumption_cond_in (cond_eq_term_right t)
-   
-let replace_term_in t = rewrite_assumption_cond_in (cond_eq_term t)
-*)
-
-let replace_term_left t = replace_multi_term (Some true) t Tacticals.onConcl
-
-let replace_term_right t = replace_multi_term (Some false) t Tacticals.onConcl
-
-let replace_term t = replace_multi_term None t Tacticals.onConcl
-
-let replace_term_in_left t hyp = replace_multi_term (Some true) t (Tacticals.onHyp hyp)
-
-let replace_term_in_right t hyp = replace_multi_term (Some false) t (Tacticals.onHyp hyp)
-
-let replace_term_in t hyp = replace_multi_term None t (Tacticals.onHyp hyp)
-
 let _ = Tactics.register_general_multi_rewrite general_multi_rewrite
diff --git a/tactics/equality.mli b/tactics/equality.mli
index df59867bb9..bcbe3e222d 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -32,11 +32,6 @@ val general_rewrite_bindings :
 val general_rewrite : 
   bool -> occurrences -> constr -> tactic
 
-(* Obsolete, use [general_rewrite_bindings l2r]
-[val rewriteLR_bindings       : constr with_bindings -> tactic]
-[val rewriteRL_bindings       : constr with_bindings -> tactic]
-*)
-
 (* Equivalent to [general_rewrite l2r] *)
 val rewriteLR   : constr -> tactic
 val rewriteRL   : constr  -> tactic