From e3eedfd7b585f2ab71c6c5750dcefa4d8ecb6f38 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Mon, 31 Mar 2014 18:13:33 +0200
Subject: Removing dead code in Tactics.

---
 tactics/tactics.mli | 16 ----------------
 1 file changed, 16 deletions(-)

(limited to 'tactics/tactics.mli')

diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index e07518aba..9e10de8dd 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -26,7 +26,6 @@ open Locus
 
 (** {6 General functions. } *)
 
-val string_of_inductive : constr -> string
 val head_constr       : constr -> constr * constr list
 val head_constr_bound : constr -> constr * constr list
 val is_quantified_hypothesis : Id.t -> goal sigma -> bool
@@ -75,7 +74,6 @@ val intros               : unit Proofview.tactic
 val depth_of_quantified_hypothesis :
   bool -> quantified_hypothesis -> goal sigma -> int
 
-val intros_until_n_wored : int -> unit Proofview.tactic
 val intros_until         : quantified_hypothesis -> unit Proofview.tactic
 
 val intros_clearing      : bool list -> unit Proofview.tactic
@@ -159,7 +157,6 @@ val unfold_constr     : global_reference -> tactic
 val clear         : Id.t list -> tactic
 val clear_body    : Id.t list -> tactic
 val keep          : Id.t list -> tactic
-val clear_if_overwritten : constr -> intro_pattern_expr located list -> tactic
 
 val specialize    : int option -> constr with_bindings -> tactic
 
@@ -190,8 +187,6 @@ val apply_in :
     constr with_bindings located list ->
     intro_pattern_expr located option -> unit Proofview.tactic
 
-val simple_apply_in : Id.t -> constr -> unit Proofview.tactic
-
 (** {6 Elimination tactics. } *)
 
 
@@ -243,7 +238,6 @@ type elim_scheme = {
 
 
 val compute_elim_sig : ?elimc: constr with_bindings -> types -> elim_scheme
-val rebuild_elimtype_from_scheme: elim_scheme -> types
 
 (** elim principle with the index of its inductive arg *)
 type eliminator = {
@@ -304,16 +298,6 @@ val induction_destruct : rec_flag -> evars_flag ->
 val case_type         : constr  -> tactic
 val elim_type         : constr  -> tactic
 
-(** {6 Some eliminations which are frequently used. } *)
-
-val impE : Id.t -> unit Proofview.tactic
-val andE : Id.t -> unit Proofview.tactic
-val orE  : Id.t -> unit Proofview.tactic
-val dImp : clause -> unit Proofview.tactic
-val dAnd : clause -> unit Proofview.tactic
-val dorE : bool -> clause -> unit Proofview.tactic
-
-
 (** {6 Introduction tactics. } *)
 
 val constructor_tac      : evars_flag -> int option -> int ->
-- 
cgit v1.2.3