Move elim-specific code from Tacticals to Elim.

No reason to have them there.

1 files changed, 1 insertions, 29 deletions

diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 48a06e6e1d..bfead34b3b 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Names
-open Constr
 open EConstr
 open Evd
 open Locus
@@ -94,18 +93,6 @@ val onClauseLR : (Id.t option -> tactic) -> clause -> tactic
 
 (** {6 Elimination tacticals. } *)
 
-type branch_args = private {
-  ity        : pinductive;  (** the type we were eliminating on *)
-  branchnum  : int;         (** the branch number *)
-  nassums    : int;         (** number of assumptions/letin to be introduced *)
-  branchsign : bool list;   (** the signature of the branch.
-                                true=assumption, false=let-in *)
-  branchnames : intro_patterns}
-
-type branch_assumptions = private {
-  ba        : branch_args;       (** the branch args *)
-  assums    : named_context}   (** the list of assumptions introduced *)
-
 (** [get_and_check_or_and_pattern loc pats branchsign] returns an appropriate
    error message if |pats| <> |branchsign|; extends them if no pattern is given
    for let-ins in the case of a conjunctive pattern *)
@@ -122,7 +109,7 @@ val compute_constructor_signatures : rec_flag:bool -> inductive * 'a -> bool lis
 
 (** Useful for [as intro_pattern] modifier *)
 val compute_induction_names :
-  bool list array -> or_and_intro_pattern option -> intro_patterns array
+  bool -> bool list array -> or_and_intro_pattern option -> intro_patterns array
 
 val elimination_sort_of_goal : Goal.goal sigma -> Sorts.family
 val elimination_sort_of_hyp  : Id.t -> Goal.goal sigma -> Sorts.family
@@ -249,20 +236,5 @@ module New : sig
   val elimination_sort_of_hyp  : Id.t -> Proofview.Goal.t -> Sorts.family
   val elimination_sort_of_clause : Id.t option -> Proofview.Goal.t -> Sorts.family
 
-  val elimination_then :
-    (branch_args -> unit Proofview.tactic) ->
-    constr -> unit Proofview.tactic
-
-  val case_then_using :
-    or_and_intro_pattern option -> (branch_args -> unit Proofview.tactic) ->
-    constr option -> inductive * EInstance.t -> constr * types -> unit Proofview.tactic
-
-  val case_nodep_then_using :
-    or_and_intro_pattern option -> (branch_args -> unit Proofview.tactic) ->
-    constr option -> inductive * EInstance.t -> constr * types -> unit Proofview.tactic
-
-  val elim_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args  -> unit Proofview.tactic
-  val case_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args  -> unit Proofview.tactic
-
   val pf_constr_of_global : GlobRef.t -> constr Proofview.tactic
 end