Factorize the only uses of internal API in Elim for Inv.

3 files changed, 12 insertions, 22 deletions

diff --git a/tactics/elim.ml b/tactics/elim.ml
index ee249a3a11..a24e942f64 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -167,6 +167,10 @@ let introCaseAssumsThen with_evars tac ba =
     tclTHEN (intro_patterns with_evars l1) (intros_clearing l3) in
   (tclTHEN introCaseAssums (case_on_ba (tac l2) ba))
 
+let case_tac dep names tac elim ind c =
+  let case_tac = if dep then case_then_using else case_nodep_then_using in
+  case_tac names (introCaseAssumsThen false (* ApplyOn not supported by inversion *) tac) (Some elim) ind c
+
 (* The following tactic Decompose repeatedly applies the
    elimination(s) rule(s) of the types satisfying the predicate
    ``recognizer'' onto a certain hypothesis. For example :
diff --git a/tactics/elim.mli b/tactics/elim.mli
index d470309b4a..4c5cdc8a31 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -14,19 +14,9 @@ open Tactypes
 
 (** Eliminations tactics. *)
 
-type branch_args
-
-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 introCaseAssumsThen : Tactics.evars_flag ->
+val case_tac : bool -> or_and_intro_pattern option ->
   (intro_patterns -> named_context -> unit Proofview.tactic) ->
-    branch_args -> unit Proofview.tactic
+  constr -> inductive * EInstance.t -> constr * types -> unit Proofview.tactic
 
 val h_decompose       : inductive list -> constr -> unit Proofview.tactic
 val h_decompose_or    : constr -> unit Proofview.tactic
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 7a88a4b0be..f77b52b931 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -474,13 +474,12 @@ let raw_inversion inv_kind id status names =
     let (elim_predicate, args) =
       make_inv_predicate env evdref indf realargs id status concl in
     let sigma = !evdref in
-    let (cut_concl,case_tac) =
-      if status != NoDep && (local_occur_var sigma id concl) then
-        Reductionops.beta_applist sigma (elim_predicate, realargs@[c]),
-        case_then_using
+    let dep = status != NoDep && (local_occur_var sigma id concl) in
+    let cut_concl =
+      if dep then
+        Reductionops.beta_applist sigma (elim_predicate, realargs@[c])
       else
-        Reductionops.beta_applist sigma (elim_predicate, realargs),
-        case_nodep_then_using
+        Reductionops.beta_applist sigma (elim_predicate, realargs)
     in
     let refined id =
       let prf = mkApp (mkVar id, args) in
@@ -491,10 +490,7 @@ let raw_inversion inv_kind id status names =
     tclTHEN (Proofview.Unsafe.tclEVARS sigma)
       (tclTHENS
         (assert_before Anonymous cut_concl)
-        [case_tac names
-            (introCaseAssumsThen false (* ApplyOn not supported by inversion *)
-               (rewrite_equations_tac as_mode inv_kind id neqns))
-            (Some elim_predicate) ind (c,t);
+        [case_tac dep names (rewrite_equations_tac as_mode inv_kind id neqns) elim_predicate ind (c,t);
         onLastHypId (fun id -> tclTHEN (refined id) reflexivity)])
   end