Removing simple induction / destruct from the AST.

8 files changed, 10 insertions, 17 deletions

diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 67331727a6..6483f66a3d 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -357,9 +357,6 @@ let rec mlexpr_of_atomic_tactic = function
       >>
 
   (* Derived basic tactics *)
-  | Tacexpr.TacSimpleInductionDestruct (isrec,h) ->
-      <:expr< Tacexpr.TacSimpleInductionDestruct $mlexpr_of_bool isrec$
-                  $mlexpr_of_quantified_hypothesis h$ >>
   | Tacexpr.TacInductionDestruct (isrec,ev,l) ->
       <:expr< Tacexpr.TacInductionDestruct $mlexpr_of_bool isrec$ $mlexpr_of_bool ev$
 	$mlexpr_of_triple
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 88e5c36961..8e5b51b873 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -130,7 +130,6 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
       intro_pattern_expr located option
 
   (* Derived basic tactics *)
-  | TacSimpleInductionDestruct of rec_flag * quantified_hypothesis
   | TacInductionDestruct of
       rec_flag * evars_flag * ('trm,'nam) induction_clause_list
   | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index b9eaf53ee5..a29c782c5b 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -608,16 +608,12 @@ GEXTEND Gram
       | IDENT "generalize"; IDENT "dependent"; c = constr -> TacGeneralizeDep c
 
       (* Derived basic tactics *)
-      | IDENT "simple"; IDENT"induction"; h = quantified_hypothesis ->
-          TacSimpleInductionDestruct (true,h)
       | IDENT "induction"; ic = induction_clause_list ->
 	  TacInductionDestruct (true,false,ic)
       | IDENT "einduction"; ic = induction_clause_list ->
 	  TacInductionDestruct(true,true,ic)
       | IDENT "double"; IDENT "induction"; h1 = quantified_hypothesis;
 	  h2 = quantified_hypothesis -> TacDoubleInduction (h1,h2)
-      | IDENT "simple"; IDENT "destruct"; h = quantified_hypothesis ->
-          TacSimpleInductionDestruct (false,h)
       | IDENT "destruct"; icl = induction_clause_list ->
 	  TacInductionDestruct(false,false,icl)
       | IDENT "edestruct";  icl = induction_clause_list ->
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index cdcff9bb2c..42a7e894a1 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -721,9 +721,6 @@ and pr_atom1 = function
 	     ++ str "in" ++ pr_hyp_location pr_ident (id,[],(hloc,ref None)))
 *)
   (* Derived basic tactics *)
-  | TacSimpleInductionDestruct (isrec,h) ->
-      hov 1 (str "simple " ++ str (if isrec then "induction" else "destruct")
-             ++ pr_arg pr_quantified_hypothesis h)
   | TacInductionDestruct (isrec,ev,(l,el,cl)) ->
       hov 1 (str (with_evars ev (if isrec then "induction" else "destruct")) ++
              spc () ++
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index 1965072743..179d3622f2 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -175,3 +175,13 @@ END
 TACTIC EXTEND intros_until
   [ "intros" "until" quantified_hypothesis(h) ] -> [ Tactics.intros_until h ]
 END
+
+(** Simple induction / destruct *)
+
+TACTIC EXTEND simple_induction
+  [ "simple" "induction" quantified_hypothesis(h) ] -> [ Tactics.simple_induct h ]
+END
+
+TACTIC EXTEND simple_destruct
+  [ "simple" "destruct" quantified_hypothesis(h) ] -> [ Tactics.simple_destruct h ]
+END
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 6c9e202895..04fd28b309 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -495,8 +495,6 @@ let rec intern_atomic lf ist x =
         List.map (intern_constr ist) lems,l)
 
   (* Derived basic tactics *)
-  | TacSimpleInductionDestruct (isrec,h) ->
-      TacSimpleInductionDestruct (isrec,intern_quantified_hypothesis ist h)
   | TacInductionDestruct (ev,isrec,(l,el,cls)) ->
       TacInductionDestruct (ev,isrec,(List.map (fun (c,(ipato,ipats)) ->
 	      (intern_induction_arg ist c,
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 2bb8ab8406..4372f87a4b 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1688,9 +1688,6 @@ and interp_atomic ist tac : unit Proofview.tactic =
       end
 
   (* Derived basic tactics *)
-  | TacSimpleInductionDestruct (isrec,h) ->
-      let h = interp_quantified_hypothesis ist h in
-      if isrec then Tactics.simple_induct h else Tactics.simple_destruct h
   | TacInductionDestruct (isrec,ev,(l,el,cls)) ->
       (* spiwack: some unknown part of destruct needs the goal to be
          prenormalised. *)
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index d8ff931d39..93c6edfe65 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -162,7 +162,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacAuto (d,n,lems,l) -> TacAuto (d,n,List.map (subst_glob_constr subst) lems,l)
 
   (* Derived basic tactics *)
-  | TacSimpleInductionDestruct (isrec,h) as x -> x
   | TacInductionDestruct (isrec,ev,(l,el,cls)) ->
       let l' = List.map (fun (c,ids) -> subst_induction_arg subst c, ids) l in
       let el' = Option.map (subst_glob_with_bindings subst) el in