Move elim-specific code from Tacticals to Elim.

No reason to have them there.

1 files changed, 27 insertions, 1 deletions

diff --git a/tactics/elim.mli b/tactics/elim.mli
index e89855a050..319c4b5f6b 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -10,11 +10,37 @@
 
 open Names
 open EConstr
-open Tacticals
 open Tactypes
 
 (** Eliminations tactics. *)
 
+type branch_args = private {
+  ity        : Constr.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 *)
+
+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 introCaseAssumsThen : Tactics.evars_flag ->
   (intro_patterns -> branch_assumptions -> unit Proofview.tactic) ->
     branch_args -> unit Proofview.tactic