From 30455aa6d2c1a069abbab7092aeb6096ce84446f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 27 Feb 2018 05:59:53 +0100
Subject: Moving code for "simple induction"/"simple destruct" to
 coretactics.ml4.

---
 plugins/ltac/coretactics.ml4 | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

(limited to 'plugins')

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 *)
-- 
cgit v1.2.3