Removing dead code, thanks to new OCaml warnings and a bit of scripting.

15 files changed, 5 insertions, 99 deletions

diff --git a/tactics/dn.mli b/tactics/dn.mli
index 78896ae9a..20407e9d9 100644
--- a/tactics/dn.mli
+++ b/tactics/dn.mli
@@ -36,6 +36,4 @@ sig
 
   val app : (Z.t -> unit) -> t -> unit
 
-  val skip_arg : int -> t -> (t * bool) list
-
 end
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 6c3c55efd..0ab426cd2 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -58,8 +58,6 @@ let registered_e_assumption gl =
 
 (*s Tactics handling a list of goals. *)
 
-type tactic_list = (goal list sigma) -> (goal list sigma)
-
 (* first_goal : goal list sigma -> goal sigma *)
 
 let first_goal gls =
@@ -201,10 +199,6 @@ module SearchProblem = struct
 
   let pr_ev evs ev = Printer.pr_constr_env (Evd.evar_env ev) (Evarutil.nf_evar evs ev.Evd.evar_concl)
 
-  let pr_goals gls =
-    let evars = Evarutil.nf_evar_map (Refiner.project gls) in
-      prlist (pr_ev evars) (sig_it gls)
-
   let filter_tactics glls l =
 (*     let _ = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *)
 (*     let evars = Evarutil.nf_evars (Refiner.project glls) in *)
@@ -489,8 +483,6 @@ let autounfold_tac db cls gl =
   in
   autounfold dbs  cls gl
 
-open Extraargs
-
 TACTIC EXTEND autounfold
 | [ "autounfold" hintbases(db) clause(cl) ] -> [ Proofview.V82.tactic (autounfold_tac db cl) ]
 END
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 845c4eee1..0720273bb 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -113,11 +113,6 @@ let decompose_these c l =
   general_decompose (fun (_,t) -> head_in indl t gl) c
   end
 
-let decompose_nonrec c =
-  general_decompose
-    (fun (_,t) -> is_non_recursive_type t)
-    c
-
 let decompose_and c =
   general_decompose
     (fun (_,t) -> is_record t)
diff --git a/tactics/elim.mli b/tactics/elim.mli
index b83a97bcc..b5e89de08 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -13,20 +13,11 @@ open Misctypes
 
 (** Eliminations tactics. *)
 
-val introElimAssumsThen :
-  (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic
-
 val introCaseAssumsThen :
   (intro_pattern_expr Loc.located list -> branch_assumptions -> unit Proofview.tactic) ->
     branch_args -> unit Proofview.tactic
 
-val general_decompose : (Id.t * constr -> bool) -> constr -> unit Proofview.tactic
-val decompose_nonrec  : constr -> unit Proofview.tactic
-val decompose_and     : constr -> unit Proofview.tactic
-val decompose_or      : constr -> unit Proofview.tactic
 val h_decompose       : inductive list -> constr -> unit Proofview.tactic
 val h_decompose_or    : constr -> unit Proofview.tactic
 val h_decompose_and   : constr -> unit Proofview.tactic
-
-val double_ind : quantified_hypothesis -> quantified_hypothesis -> unit Proofview.tactic
 val h_double_induction : quantified_hypothesis -> quantified_hypothesis-> unit Proofview.tactic
diff --git a/tactics/equality.ml b/tactics/equality.ml
index a480f6de6..71b3c0045 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -563,12 +563,8 @@ let multi_replace clause c2 c1 unsafe try_prove_eq_opt =
 
 let replace c2 c1 = multi_replace onConcl c2 c1 false None
 
-let replace_in id c2 c1 = multi_replace (onHyp id) c2 c1 false None
-
 let replace_by c2 c1 tac = multi_replace onConcl c2 c1 false (Some tac)
 
-let replace_in_by id c2 c1 tac = multi_replace (onHyp id) c2 c1 false (Some tac)
-
 let replace_in_clause_maybe_by c2 c1 cl tac_opt =
   multi_replace cl c2 c1 false tac_opt
 
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 5ea0f9333..b59b4bbe0 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -69,13 +69,10 @@ val general_multi_multi_rewrite :
 
 val replace_in_clause_maybe_by : constr -> constr -> clause -> unit Proofview.tactic option -> unit Proofview.tactic
 val replace    : constr -> constr -> unit Proofview.tactic
-val replace_in : Id.t -> constr -> constr -> unit Proofview.tactic
 val replace_by : constr -> constr -> unit Proofview.tactic -> unit Proofview.tactic
-val replace_in_by : Id.t -> constr -> constr -> unit Proofview.tactic -> unit Proofview.tactic
 
 val discr        : evars_flag -> constr with_bindings -> unit Proofview.tactic
 val discrConcl   : unit Proofview.tactic
-val discrClause  : evars_flag -> clause -> unit Proofview.tactic
 val discrHyp     : Id.t -> unit Proofview.tactic
 val discrEverywhere : evars_flag -> unit Proofview.tactic
 val discr_tac    : evars_flag ->
@@ -101,9 +98,6 @@ val cutRewriteInConcl : bool -> constr -> unit Proofview.tactic
 val rewriteInHyp : bool -> constr -> Id.t -> unit Proofview.tactic
 val rewriteInConcl : bool -> constr -> unit Proofview.tactic
 
-(* Expect the proof of an equality; fails with raw internal errors *)
-val substClause : bool -> constr -> Id.t option -> unit Proofview.tactic
-
 val discriminable : env -> evar_map -> constr -> constr -> bool
 val injectable : env -> evar_map -> constr -> constr -> bool
 
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index 6cc0af2c6..89aaee485 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -18,6 +18,7 @@ open Inductiveops
 open ConstrMatching
 open Coqlib
 open Declarations
+open Tacmach.New
 
 (* I implemented the following functions which test whether a term t
    is an inductive but non-recursive type, a general conjuction, a
@@ -396,10 +397,10 @@ let find_eq_data eqn = (* fails with PatternMatchingFailure *)
 
 let extract_eq_args gl = function
   | MonomorphicLeibnizEq (e1,e2) ->
-      let t = Tacmach.New.pf_type_of gl e1 in (t,e1,e2)
+      let t = pf_type_of gl e1 in (t,e1,e2)
   | PolymorphicLeibnizEq (t,e1,e2) -> (t,e1,e2)
   | HeterogenousEq (t1,e1,t2,e2) ->
-      if Tacmach.New.pf_conv_x gl t1 t2 then (t1,e1,e2)
+      if pf_conv_x gl t1 t2 then (t1,e1,e2)
       else raise PatternMatchingFailure
 
 let find_eq_data_decompose gl eqn =
@@ -418,13 +419,11 @@ let find_this_eq_data_decompose gl eqn =
       error "Don't know what to do with JMeq on arguments not of same type." in
   (lbeq,eq_args)
 
-open Tacmach
-
 let match_eq_nf gls eqn eq_pat =
-  match Id.Map.bindings (Tacmach.New.pf_matches gls (Lazy.force eq_pat) eqn) with
+  match Id.Map.bindings (pf_matches gls (Lazy.force eq_pat) eqn) with
     | [(m1,t);(m2,x);(m3,y)] ->
         assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3);
-	(t,Tacmach.New.pf_whd_betadeltaiota gls x,Tacmach.New.pf_whd_betadeltaiota gls y)
+	(t,pf_whd_betadeltaiota gls x,pf_whd_betadeltaiota gls y)
     | _ -> anomaly ~label:"match_eq" (Pp.str "an eq pattern should match 3 terms")
 
 let dest_nf_eq gls eqn =
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 5667e7015..acd959e1d 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -21,7 +21,6 @@ open Inductiveops
 open Printer
 open Retyping
 open Tacmach.New
-open Clenv
 open Tacticals.New
 open Tactics
 open Elim
@@ -32,24 +31,6 @@ open Proofview.Notations
 
 let clear hyps = Proofview.V82.tactic (clear hyps)
 
-let collect_meta_variables c =
-  let rec collrec acc c = match kind_of_term c with
-    | Meta mv -> mv::acc
-    | _ -> fold_constr collrec acc c
-  in
-  collrec [] c
-
-let check_no_metas clenv ccl =
-  if occur_meta ccl then
-    let metas = List.filter (fun m -> not (Evd.meta_defined clenv.evd m))
-      (collect_meta_variables ccl) in
-    let metas = List.map (Evd.meta_name clenv.evd) metas in
-    let opts = match metas with [_] -> " " | _ -> "s " in
-    errorlabstrm "inversion"
-      (str ("Cannot find an instantiation for variable"^opts) ++
-	 prlist_with_sep pr_comma pr_name metas
-	 (* ajouter "in " ++ pr_lconstr ccl mais il faut le bon contexte *))
-
 let var_occurs_in_pf gl id =
   let env = Proofview.Goal.env gl in
   occur_var env id (Proofview.Goal.concl gl) ||
@@ -518,13 +499,11 @@ open Tacexpr
 
 let inv k = inv_gen false k NoDep
 
-let half_inv_tac id  = inv SimpleInversion None (NamedHyp id)
 let inv_tac id       = inv FullInversion None (NamedHyp id)
 let inv_clear_tac id = inv FullInversionClear None (NamedHyp id)
 
 let dinv k c = inv_gen false k (Dep c)
 
-let half_dinv_tac id  = dinv SimpleInversion None None (NamedHyp id)
 let dinv_tac id       = dinv FullInversion None None (NamedHyp id)
 let dinv_clear_tac id = dinv FullInversionClear None None (NamedHyp id)
 
diff --git a/tactics/inv.mli b/tactics/inv.mli
index f5820c33c..615ceaab5 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.mli
@@ -14,13 +14,6 @@ open Tacexpr
 
 type inversion_status = Dep of constr option | NoDep
 
-val inv_gen :
-  bool -> inversion_kind -> inversion_status ->
-    intro_pattern_expr located option -> quantified_hypothesis -> unit Proofview.tactic
-val invIn_gen :
-  inversion_kind -> intro_pattern_expr located option -> Id.t list ->
-    quantified_hypothesis -> unit Proofview.tactic
-
 val inv_clause :
   inversion_kind -> intro_pattern_expr located option -> Id.t list ->
     quantified_hypothesis -> unit Proofview.tactic
@@ -31,9 +24,7 @@ val inv : inversion_kind -> intro_pattern_expr located option ->
 val dinv : inversion_kind -> constr option ->
   intro_pattern_expr located option -> quantified_hypothesis -> unit Proofview.tactic
 
-val half_inv_tac : Id.t -> unit Proofview.tactic
 val inv_tac : Id.t -> unit Proofview.tactic
 val inv_clear_tac : Id.t -> unit Proofview.tactic
-val half_dinv_tac : Id.t -> unit Proofview.tactic
 val dinv_tac : Id.t -> unit Proofview.tactic
 val dinv_clear_tac : Id.t -> unit Proofview.tactic
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 2e55869de..5e5de2589 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -22,7 +22,6 @@ open Entries
 open Inductiveops
 open Environ
 open Tacmach.New
-open Pfedit
 open Clenv
 open Declare
 open Tacticals.New
diff --git a/tactics/leminv.mli b/tactics/leminv.mli
index 76223abed..6d8d07da6 100644
--- a/tactics/leminv.mli
+++ b/tactics/leminv.mli
@@ -12,9 +12,6 @@ open Term
 open Constrexpr
 open Misctypes
 
-val lemInv_gen : quantified_hypothesis -> constr -> unit Proofview.tactic
-val lemInvIn_gen : quantified_hypothesis -> constr -> Id.t list -> unit Proofview.tactic
-
 val lemInv_clause :
   quantified_hypothesis -> constr -> Id.t list -> unit Proofview.tactic
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index f1b52ebc7..bd33e5146 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -63,13 +63,6 @@ let tclIFTHENTRYELSEMUST = Refiner.tclIFTHENTRYELSEMUST
 
 let tclTHENSEQ       = tclTHENLIST
 
-(* Experimental *)
-
-let rec tclFIRST_PROGRESS_ON tac = function
-  | []    -> tclFAIL 0 (str "No applicable tactic")
-  | [a]   -> tac a (* so that returned failure is the one from last item *)
-  | a::tl -> tclORELSE (tac a) (tclFIRST_PROGRESS_ON tac tl)
-
 (************************************************************************)
 (* Tacticals applying on hypotheses                                     *)
 (************************************************************************)
@@ -126,9 +119,6 @@ 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 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 onClause tac cl gls =
   let hyps () = pf_ids_of_hyps gls in
   tclMAP tac (Locusops.simple_clause_of hyps cl) gls
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 2944ff690..fcc23df22 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -58,8 +58,6 @@ val tclIFTHENSELSE       : tactic -> tactic list -> tactic -> tactic
 val tclIFTHENSVELSE      : tactic -> tactic array -> tactic -> tactic
 val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic
 
-val tclFIRST_PROGRESS_ON : ('a -> tactic) -> 'a list -> tactic
-
 (** {6 Tacticals applying to hypotheses } *)
 
 val onNthHypId       : int -> (Id.t -> tactic) -> tactic
@@ -94,9 +92,6 @@ val onHyps      : (goal sigma -> named_context) ->
    goal; in particular, it can abstractly refer to the set of
    hypotheses independently of the effective contents of the current goal *)
 
-val tryAllHyps          : (Id.t -> tactic) -> tactic
-val tryAllHypsAndConcl  : (Id.t option -> tactic) -> tactic
-
 val onAllHyps           : (Id.t -> tactic) -> tactic
 val onAllHypsAndConcl   : (Id.t option -> tactic) -> tactic
 
@@ -200,7 +195,6 @@ module New : sig
 
   val tclTRY : unit tactic -> unit tactic
   val tclFIRST : unit tactic list -> unit tactic
-  val tclFIRST_PROGRESS_ON : ('a -> unit tactic) -> 'a list -> unit tactic
   val tclIFTHENELSE : unit tactic -> unit tactic -> unit tactic -> unit tactic
   val tclIFTHENSVELSE : unit tactic -> unit tactic array -> unit tactic -> unit tactic
   val tclIFTHENTRYELSEMUST : unit tactic -> unit tactic -> unit tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index be5b0de3a..ab1af8c3e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -490,8 +490,6 @@ let rec intros_using = function
 
 let intros = Tacticals.New.tclREPEAT intro
 
-let intro_erasing id = tclTHEN (thin [id]) (introduction id)
-
 let intro_forthcoming_then_gen loc name_flag move_flag dep_flag tac =
   let rec aux ids =
     Proofview.tclORELSE
@@ -932,9 +930,6 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags) id i elimclause
       (str "Nothing to rewrite in " ++ pr_id id ++ str".");
   clenv_refine_in with_evars id elimclause'' gl
 
-let general_elim_in with_evars id =
-  general_elim_clause (elimination_in_clause_scheme with_evars id)
-
 (* Apply a tactic below the products of the conclusion of a lemma *)
 
 type conjunction_status =
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 0e92e7eb9..5b7ad1f88 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -64,7 +64,6 @@ val intro_using          : Id.t -> unit Proofview.tactic
 val intro_mustbe_force   : Id.t -> unit Proofview.tactic
 val intro_then           : (Id.t -> unit Proofview.tactic) -> unit Proofview.tactic
 val intros_using         : Id.t list -> unit Proofview.tactic
-val intro_erasing        : Id.t -> tactic
 val intros_replacing     : Id.t list -> unit Proofview.tactic
 
 val intros               : unit Proofview.tactic
@@ -256,8 +255,6 @@ val general_elim_clause_gen : (int -> Clenv.clausenv -> 'a -> tactic) ->
 
 val general_elim  : evars_flag ->
   constr with_bindings -> eliminator -> tactic
-val general_elim_in : evars_flag -> Id.t ->
-  constr with_bindings -> eliminator -> tactic
 
 val default_elim  : evars_flag -> constr with_bindings -> unit Proofview.tactic
 val simplest_elim : constr -> unit Proofview.tactic
@@ -328,7 +325,6 @@ val setoid_symmetry : unit Proofview.tactic Hook.t
 val symmetry_red                : bool -> unit Proofview.tactic
 val symmetry                    : unit Proofview.tactic
 val setoid_symmetry_in : (Id.t -> unit Proofview.tactic) Hook.t
-val symmetry_in                 : Id.t -> unit Proofview.tactic
 val intros_symmetry             : clause -> unit Proofview.tactic
 
 val setoid_transitivity : (constr option -> unit Proofview.tactic) Hook.t