diff options
| -rw-r--r-- | grammar/q_coqast.ml4 | 3 | ||||
| -rw-r--r-- | intf/tacexpr.mli | 1 | ||||
| -rw-r--r-- | parsing/g_tactic.ml4 | 4 | ||||
| -rw-r--r-- | printing/pptactic.ml | 3 | ||||
| -rw-r--r-- | tactics/coretactics.ml4 | 10 | ||||
| -rw-r--r-- | tactics/tacintern.ml | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 3 | ||||
| -rw-r--r-- | tactics/tacsubst.ml | 1 |
8 files changed, 10 insertions, 17 deletions
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 index 67331727a..6483f66a3 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 88e5c3696..8e5b51b87 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 b9eaf53ee..a29c782c5 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 cdcff9bb2..42a7e894a 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 196507274..179d3622f 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 6c9e20289..04fd28b30 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 2bb8ab840..4372f87a4 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 d8ff931d3..93c6edfe6 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 |