diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-03-31 18:13:33 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-03-31 19:02:38 +0200 |
| commit | e3eedfd7b585f2ab71c6c5750dcefa4d8ecb6f38 (patch) | |
| tree | aac63216c443c71443fc85e97c3b6e8a42de4391 /tactics/tactics.mli | |
| parent | 863b9a54e58b9548dd4691d3864b3e6cda9e63a0 (diff) | |
Removing dead code in Tactics.
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 16 |
1 files changed, 0 insertions, 16 deletions
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 -> |