Moving the decompose tactic out of the AST.

9 files changed, 14 insertions, 28 deletions

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index abb2292cd..261c28d7f 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -144,7 +144,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
-  | TacDecompose of 'ind list * 'trm
 
   (* Automation tactics *)
   | TacTrivial of debug * 'trm list * string list option
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index ae4bf8a12..861ac5dfd 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -629,8 +629,6 @@ GEXTEND Gram
 	  TacAtom (!@loc, TacInductionDestruct(false,false,icl))
       | IDENT "edestruct";  icl = induction_clause_list ->
 	  TacAtom (!@loc, TacInductionDestruct(false,true,icl))
-      | IDENT "decompose"; "["; l = LIST1 smart_global; "]"; c = constr
-        -> TacAtom (!@loc, TacDecompose (l,c))
 
       (* Automation tactic *)
       | d = trivial; lems = auto_using; db = hintbases -> TacAtom (!@loc, TacTrivial (d,lems,db))
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index a3a023ce9..f3bec78e2 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -759,10 +759,6 @@ and pr_atom1 = function
         (str "double induction" ++
          pr_arg pr_quantified_hypothesis h1 ++
 	 pr_arg pr_quantified_hypothesis h2)
-  | TacDecompose (l,c) ->
-      hov 1 (str "decompose" ++ spc () ++
-        hov 0 (str "[" ++ prlist_with_sep spc pr_ind l
-	  ++ str "]" ++ pr_constrarg c))
   (* Automation tactics *)
   | TacTrivial (_,[],Some []) as x -> pr_atom0 x
   | TacTrivial (d,lems,db) ->
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index efe9dde78..ff0d89a5c 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -969,3 +969,17 @@ let guard tst =
 TACTIC EXTEND guard
 | [ "guard" test(tst) ] -> [ guard tst ]
 END
+
+let decompose l c =
+  Proofview.Goal.raw_enter begin fun gl ->
+    let to_ind c =
+      if isInd c then Univ.out_punivs (destInd c)
+      else error "not an inductive type"
+    in
+    let l = List.map to_ind l in
+    Elim.h_decompose l c
+  end
+
+TACTIC EXTEND decompose
+| [ "decompose" "[" ne_constr_list(l) "]" constr(c) ] -> [ decompose l c ]
+END
diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml
index 3d3c97b54..955fd5578 100644
--- a/tactics/taccoerce.ml
+++ b/tactics/taccoerce.ml
@@ -232,11 +232,6 @@ let coerce_to_reference env v =
     end
   | None -> raise (CannotCoerceTo "a reference")
 
-let coerce_to_inductive v =
-  match Value.to_constr v with
-  | Some c when isInd c -> Univ.out_punivs (destInd c)
-  | _ -> raise (CannotCoerceTo "an inductive type")
-
 (* Quantified named or numbered hypothesis or hypothesis in context *)
 (* (as in Inversion) *)
 let coerce_to_quantified_hypothesis v =
diff --git a/tactics/taccoerce.mli b/tactics/taccoerce.mli
index cec25d9bd..c0ede540c 100644
--- a/tactics/taccoerce.mli
+++ b/tactics/taccoerce.mli
@@ -82,8 +82,6 @@ val coerce_to_hyp_list : Environ.env -> Value.t -> Id.t list
 
 val coerce_to_reference : Environ.env -> Value.t -> Globnames.global_reference
 
-val coerce_to_inductive : Value.t -> inductive
-
 val coerce_to_quantified_hypothesis : Value.t -> quantified_hypothesis
 
 val coerce_to_decl_or_quant_hyp : Environ.env -> Value.t -> quantified_hypothesis
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 714df10d1..eac80a63a 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -512,8 +512,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)
-  | TacDecompose (l,c) -> let l = List.map (intern_inductive ist) l in
-      TacDecompose (l,intern_constr ist c)
   (* Context management *)
   | TacClear (b,l) -> TacClear (b,List.map (intern_hyp ist) l)
   | TacClearBody l -> TacClearBody (List.map (intern_hyp ist) l)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 9ff0b4923..8c86db613 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -364,10 +364,6 @@ let interp_reference ist env = function
         VarRef v
       with Not_found -> error_global_not_found_loc loc (qualid_of_ident id)
 
-let interp_inductive ist = function
-  | ArgArg r -> r
-  | ArgVar locid -> interp_ltac_var coerce_to_inductive ist None locid
-
 let try_interp_evaluable env (loc, id) =
   let v = Environ.lookup_named id env in
   match v with
@@ -1924,11 +1920,6 @@ and interp_atomic ist tac : unit Proofview.tactic =
       let h1 = interp_quantified_hypothesis ist h1 in
       let h2 = interp_quantified_hypothesis ist h2 in
       Elim.h_double_induction h1 h2
-  | TacDecompose (l,c) ->
-      (new_interp_constr ist c) begin fun c ->
-        let l = List.map (interp_inductive ist) l in
-        Elim.h_decompose l c
-      end
   (* Context management *)
   | TacClear (b,l) ->
       Proofview.V82.tactic begin fun gl ->
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 33f4f499a..cdea2b47b 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -167,9 +167,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
-  | TacDecompose (l,c) ->
-      let l = List.map (subst_or_var (subst_ind subst)) l in
-      TacDecompose (l,subst_glob_constr subst c)
 
   (* Context management *)
   | TacClear _ as x -> x