Removing dead code.

16 files changed, 2 insertions, 45 deletions

diff --git a/tactics/auto.mli b/tactics/auto.mli
index ea3f0ac0da..0cc8a0b1b9 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -8,7 +8,6 @@
 
 open Names
 open Term
-open Proof_type
 open Clenv
 open Pattern
 open Evd
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 1c15fa40bf..e97a42e6e4 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -17,7 +17,6 @@ open Proof_type
 open Tacticals
 open Tacmach
 open Tactics
-open Patternops
 open Clenv
 open Typeclasses
 open Globnames
@@ -42,7 +41,7 @@ let get_typeclasses_dependency_order () = !typeclasses_dependency_order
 
 open Goptions
 
-let set_typeclasses_modulo_eta =
+let _ =
   declare_bool_option
     { optsync  = true;
       optdepr  = false;
@@ -51,7 +50,7 @@ let set_typeclasses_modulo_eta =
       optread  = get_typeclasses_modulo_eta;
       optwrite = set_typeclasses_modulo_eta; }
 
-let set_typeclasses_dependency_order =
+let _ =
   declare_bool_option
     { optsync  = true;
       optdepr  = false;
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 9ee14b801c..9b69481da9 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -9,8 +9,6 @@
 open Errors
 open Term
 open Hipattern
-open Tacmach
-open Tacticals
 open Tactics
 open Coqlib
 open Reductionops
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index 19e2f198bb..7073e8a2b8 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -8,7 +8,6 @@
 
 open Term
 open Proof_type
-open Auto
 open Evd
 open Hints
 
diff --git a/tactics/elim.ml b/tactics/elim.ml
index b7d5b1028d..3cb4fa9c4c 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -15,7 +15,6 @@ open Hipattern
 open Tacmach.New
 open Tacticals.New
 open Tactics
-open Misctypes
 open Proofview.Notations
 
 let introElimAssumsThen tac ba =
diff --git a/tactics/equality.ml b/tactics/equality.ml
index c130fa1514..ae92f4c06e 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -487,9 +487,6 @@ let apply_special_clear_request clear_flag f =
       e when catchable_exception e -> tclIDTAC
   end
 
-type delayed_open_constr_with_bindings =
-    env -> evar_map -> evar_map * constr with_bindings
-
 let general_multi_rewrite with_evars l cl tac =
   let do1 l2r f =
     Proofview.Goal.enter begin fun gl ->
@@ -1474,8 +1471,6 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
 (* then it uses the predicate "\x.phi(proj1_sig x,proj2_sig x)", and so   *)
 (* on for further iterated sigma-tuples                                   *)
 
-exception NothingToRewrite
-
 let cutSubstInConcl l2r eqn =
   Proofview.Goal.nf_enter begin fun gl ->
   let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in
@@ -1513,9 +1508,6 @@ let try_rewrite tac =
     | e when catchable_exception e ->
 	tclZEROMSG
           (strbrk "Cannot find a well-typed generalization of the goal that makes the proof progress.")
-    | NothingToRewrite ->
-	tclZEROMSG
-          (strbrk "Nothing to rewrite.")
     | e -> Proofview.tclZERO ~info e
   end
 
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 90d8a224b5..3e13ee570c 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -11,7 +11,6 @@ open Names
 open Term
 open Evd
 open Environ
-open Tacmach
 open Tacexpr
 open Ind_tables
 open Locus
diff --git a/tactics/evar_tactics.mli b/tactics/evar_tactics.mli
index 42d00e1e1a..2c4df06080 100644
--- a/tactics/evar_tactics.mli
+++ b/tactics/evar_tactics.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Tacmach
 open Names
 open Tacexpr
 open Locus
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index c200871ef6..27d25056e1 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -8,7 +8,6 @@
 
 open Names
 open Term
-open Evd
 open Coqlib
 
 (** High-order patterns *)
@@ -145,8 +144,6 @@ val is_matching_sigma : constr -> bool
 val match_eqdec : constr -> bool * constr * constr * constr * constr
 
 (** Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *)
-open Proof_type
-open Tacmach
 val dest_nf_eq : [ `NF ] Proofview.Goal.t -> constr -> (constr * constr * constr)
 
 (** Match a negation *)
diff --git a/tactics/inv.mli b/tactics/inv.mli
index b3478dda27..412f30c20d 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Loc
 open Names
 open Term
 open Misctypes
diff --git a/tactics/leminv.mli b/tactics/leminv.mli
index 47a4de444f..2f80d26fc4 100644
--- a/tactics/leminv.mli
+++ b/tactics/leminv.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Loc
 open Names
 open Term
 open Constrexpr
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
index cb20fc9308..84c0a99b18 100644
--- a/tactics/tacenv.ml
+++ b/tactics/tacenv.ml
@@ -71,7 +71,6 @@ let interp_ml_tactic s =
 (* Summary and Object declaration *)
 
 open Nametab
-open Libnames
 open Libobject
 
 let mactab =
@@ -84,7 +83,6 @@ let is_ltac_for_ml_tactic r = fst (KNmap.find r !mactab)
 
 (* Declaration of the TAC-DEFINITION object *)
 let add (kn,td) = mactab := KNmap.add kn td !mactab
-let replace (kn,td) = mactab := KNmap.add kn td !mactab
 
 let load_md i ((sp, kn), (local, id, b, t)) = match id with
 | None ->
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 59cd065d12..42e61cb57e 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -100,20 +100,11 @@ let subst_evaluable subst =
   let subst_eval_ref = subst_evaluable_reference subst in
     subst_or_var (subst_and_short_name subst_eval_ref)
 
-let subst_unfold subst (l,e) =
-  (l,subst_evaluable subst e)
-
-let subst_flag subst red =
-  { red with rConst = List.map (subst_evaluable subst) red.rConst }
-
 let subst_constr_with_occurrences subst (l,c) = (l,subst_glob_constr subst c)
 
 let subst_glob_constr_or_pattern subst (c,p) =
   (subst_glob_constr subst c,subst_pattern subst p)
 
-let subst_pattern_with_occurrences subst (l,p) =
-  (l,subst_glob_constr_or_pattern subst p)
-
 let subst_redexp subst =
   Miscops.map_red_expr_gen
     (subst_glob_constr subst)
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index cf2126f8dd..61bef41d78 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -16,7 +16,6 @@ open Context
 open Declarations
 open Tacmach
 open Clenv
-open Misctypes
 
 (************************************************************************)
 (* Tacticals re-exported from the Refiner module                        *)
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 6249bbc593..03ea89ad56 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -6,14 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Loc
 open Pp
 open Names
 open Term
 open Context
 open Tacmach
 open Proof_type
-open Clenv
 open Tacexpr
 open Locus
 open Misctypes
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 07969c7d74..6f4c94e3f8 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -765,8 +765,6 @@ let intro = intro_gen (NamingAvoid []) MoveLast false false
 let introf = intro_gen (NamingAvoid []) MoveLast true false
 let intro_avoiding l = intro_gen (NamingAvoid l) MoveLast false false
 
-let intro_then_force = intro_then_gen (NamingAvoid []) MoveLast true false
-
 let intro_move_avoid idopt avoid hto = match idopt with
   | None -> intro_gen (NamingAvoid avoid) hto true false
   | Some id -> intro_gen (NamingMustBe (dloc,id)) hto true false
@@ -2790,12 +2788,6 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
   atomize_one (List.length argl) [] []
   end
 
-let find_atomic_param_of_ind nparams indtyp =
-  let argl = snd (decompose_app indtyp) in
-  let params,args = List.chop nparams argl in
-  let test c = isVar c && not (List.exists (dependent c) params) in
-  List.map destVar (List.filter test args)
-
 (* [cook_sign] builds the lists [beforetoclear] (preceding the
    ind. var.) and [aftertoclear] (coming after the ind. var.)  of hyps
    that must be erased, the lists of hyps to be generalize [decldeps] on the