diff options
| author | Pierre-Marie Pédrot | 2014-05-21 20:45:10 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-05-21 22:02:11 +0200 |
| commit | cfd8ec82784a5c893b63f3c82736eb76fe487ad7 (patch) | |
| tree | 6023b404ea2bab422eebae013b564dccd97da57f /tactics | |
| parent | 3f6c0abc4d434d14d47681e4142ff7b927294f64 (diff) | |
Removing decompose record / sum from the tactic AST.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/extratactics.ml4 | 11 | ||||
| -rw-r--r-- | tactics/tacintern.ml | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 4 | ||||
| -rw-r--r-- | tactics/tacsubst.ml | 2 |
4 files changed, 11 insertions, 8 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index f6483e2b3d..da1475d7b3 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -179,6 +179,17 @@ TACTIC EXTEND cut_rewrite END (**********************************************************************) +(* Decompose *) + +TACTIC EXTEND decompose_sum +| [ "decompose" "sum" constr(c) ] -> [ Elim.h_decompose_or c ] +END + +TACTIC EXTEND decompose_record +| [ "decompose" "record" constr(c) ] -> [ Elim.h_decompose_and c ] +END + +(**********************************************************************) (* Contradiction *) open Contradiction diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 9f911564a3..0bb86cbf7d 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -506,8 +506,6 @@ let rec intern_atomic lf ist x = let h1 = intern_quantified_hypothesis ist h1 in let h2 = intern_quantified_hypothesis ist h2 in TacDoubleInduction (h1,h2) - | TacDecomposeAnd c -> TacDecomposeAnd (intern_constr ist c) - | TacDecomposeOr c -> TacDecomposeOr (intern_constr ist c) | TacDecompose (l,c) -> let l = List.map (intern_inductive ist) l in TacDecompose (l,intern_constr ist c) | TacSpecialize (n,l) -> TacSpecialize (n,intern_constr_with_bindings ist l) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 734d5b8949..ec8cb59ea5 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1628,10 +1628,6 @@ and interp_atomic ist tac = let h1 = interp_quantified_hypothesis ist h1 in let h2 = interp_quantified_hypothesis ist h2 in Elim.h_double_induction h1 h2 - | TacDecomposeAnd c -> - new_interp_constr ist c Elim.h_decompose_and - | TacDecomposeOr c -> - new_interp_constr ist c Elim.h_decompose_or | TacDecompose (l,c) -> (new_interp_constr ist c) begin fun c -> let l = List.map (interp_inductive ist) l in diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index bea77a0b06..1ed6b6c27c 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -166,8 +166,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with let el' = Option.map (subst_glob_with_bindings subst) el in TacInductionDestruct (isrec,ev,(l',el',cls)) | TacDoubleInduction (h1,h2) as x -> x - | TacDecomposeAnd c -> TacDecomposeAnd (subst_glob_constr subst c) - | TacDecomposeOr c -> TacDecomposeOr (subst_glob_constr subst c) | TacDecompose (l,c) -> let l = List.map (subst_or_var (subst_ind subst)) l in TacDecompose (l,subst_glob_constr subst c) |