Removing decompose record / sum from the tactic AST.

7 files changed, 11 insertions, 16 deletions

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 4b78b55fd5..d03279fc3f 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -127,8 +127,6 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
   | TacInductionDestruct of
       rec_flag * evars_flag * ('trm,'nam) induction_clause_list
   | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
-  | TacDecomposeAnd of 'trm
-  | TacDecomposeOr of 'trm
   | TacDecompose of 'ind list * 'trm
   | TacSpecialize of int option * 'trm with_bindings
 
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 5f9f6e472d..2003ec7f94 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -612,8 +612,6 @@ GEXTEND Gram
 	  TacInductionDestruct(false,false,icl)
       | IDENT "edestruct";  icl = induction_clause_list ->
 	  TacInductionDestruct(false,true,icl)
-      | IDENT "decompose"; IDENT "record" ; c = constr -> TacDecomposeAnd c
-      | IDENT "decompose"; IDENT "sum"; c = constr -> TacDecomposeOr c
       | IDENT "decompose"; "["; l = LIST1 smart_global; "]"; c = constr
         -> TacDecompose (l,c)
 
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 587a8db41b..0dabe3a265 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -718,10 +718,6 @@ and pr_atom1 = function
         (str "double induction" ++
          pr_arg pr_quantified_hypothesis h1 ++
 	 pr_arg pr_quantified_hypothesis h2)
-  | TacDecomposeAnd c ->
-      hov 1 (str "decompose record" ++ pr_constrarg c)
-  | TacDecomposeOr c ->
-      hov 1 (str "decompose sum" ++ pr_constrarg c)
   | TacDecompose (l,c) ->
       hov 1 (str "decompose" ++ spc () ++
         hov 0 (str "[" ++ prlist_with_sep spc pr_ind l
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)