From cfd8ec82784a5c893b63f3c82736eb76fe487ad7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 21 May 2014 20:45:10 +0200
Subject: Removing decompose record / sum from the tactic AST.

---
 tactics/extratactics.ml4 | 11 +++++++++++
 tactics/tacintern.ml     |  2 --
 tactics/tacinterp.ml     |  4 ----
 tactics/tacsubst.ml      |  2 --
 4 files changed, 11 insertions(+), 8 deletions(-)

(limited to 'tactics')

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index f6483e2b3d..da1475d7b3 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -178,6 +178,17 @@ TACTIC EXTEND cut_rewrite
     -> [ cutRewriteInHyp b eqn id ]
 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                                                      *)
 
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)
-- 
cgit v1.2.3