Merge PR #6846: Moving code for "simple induction"/"simple destruct" to coretactics.ml4.

3 files changed, 10 insertions, 29 deletions

diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4
index 794a28dd43..ad6c6df5fa 100644
--- a/plugins/ltac/coretactics.ml4
+++ b/plugins/ltac/coretactics.ml4
@@ -239,12 +239,20 @@ END
 
 (** Simple induction / destruct *)
 
+let simple_induct h =
+  Tacticals.New.tclTHEN (Tactics.intros_until h)
+    (Tacticals.New.onLastHyp Tactics.simplest_elim)
+
 TACTIC EXTEND simple_induction
-  [ "simple" "induction" quantified_hypothesis(h) ] -> [ Tactics.simple_induct h ]
+  [ "simple" "induction" quantified_hypothesis(h) ] -> [ simple_induct h ]
 END
 
+let simple_destruct h =
+  Tacticals.New.tclTHEN (Tactics.intros_until h)
+    (Tacticals.New.onLastHyp Tactics.simplest_case)
+
 TACTIC EXTEND simple_destruct
-  [ "simple" "destruct" quantified_hypothesis(h) ] -> [ Tactics.simple_destruct h ]
+  [ "simple" "destruct" quantified_hypothesis(h) ] -> [ simple_destruct h ]
 END
 
 (** Double induction *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 7e281e2fe0..9e6580d222 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4662,30 +4662,6 @@ let destruct ev clr c l e =
   induction_gen clr false ev e
     ((Evd.empty,(c,NoBindings)),(None,l)) None
 
-(* The registered tactic, which calls the default elimination
- * if no elimination constant is provided. *)
-
-(* Induction tactics *)
-
-(* This was Induction before 6.3 (induction only in quantified premisses) *)
-let simple_induct_id s = Tacticals.New.tclTHEN (intros_until_id s) (Tacticals.New.onLastHyp simplest_elim)
-let simple_induct_nodep n = Tacticals.New.tclTHEN (intros_until_n n) (Tacticals.New.onLastHyp simplest_elim)
-
-let simple_induct = function
-  | NamedHyp id -> simple_induct_id id
-  | AnonHyp n -> simple_induct_nodep n
-
-(* Destruction tactics *)
-
-let simple_destruct_id s    =
-  (Tacticals.New.tclTHEN (intros_until_id s) (Tacticals.New.onLastHyp simplest_case))
-let simple_destruct_nodep n =
-  (Tacticals.New.tclTHEN (intros_until_n n)    (Tacticals.New.onLastHyp simplest_case))
-
-let simple_destruct = function
-  | NamedHyp id -> simple_destruct_id id
-  | AnonHyp n -> simple_destruct_nodep n
-
 (*
  *  Eliminations giving the type instead of the proof.
  * These tactics use the default elimination constant and
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 74415f8d03..100ddf17f2 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -280,8 +280,6 @@ val simplest_elim : constr -> unit Proofview.tactic
 val elim :
   evars_flag -> clear_flag -> constr with_bindings -> constr with_bindings option -> unit Proofview.tactic
 
-val simple_induct : quantified_hypothesis -> unit Proofview.tactic
-
 val induction : evars_flag -> clear_flag -> constr -> or_and_intro_pattern option ->
   constr with_bindings option -> unit Proofview.tactic
 
@@ -290,7 +288,6 @@ val induction : evars_flag -> clear_flag -> constr -> or_and_intro_pattern optio
 val general_case_analysis : evars_flag -> clear_flag -> constr with_bindings ->  unit Proofview.tactic
 val simplest_case         : constr -> unit Proofview.tactic
 
-val simple_destruct       : quantified_hypothesis -> unit Proofview.tactic
 val destruct : evars_flag -> clear_flag -> constr -> or_and_intro_pattern option ->
   constr with_bindings option -> unit Proofview.tactic