diff options
| author | Pierre-Marie Pédrot | 2014-08-07 01:43:37 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-08-07 01:45:24 +0200 |
| commit | 876f202985d5bd463bd5b44c195b239bcfedad7c (patch) | |
| tree | e6fe3f6003e21ab642f2ab03d060f77503c1fd7a /tactics | |
| parent | 27a7d7133f83cb95eff90df4338a47b0d6681aa0 (diff) | |
Removing simple induction / destruct from the AST.
Diffstat (limited to 'tactics')
| -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 |
4 files changed, 10 insertions, 6 deletions
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 |