diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/extratactics.ml4 | 14 | ||||
| -rw-r--r-- | tactics/taccoerce.ml | 5 | ||||
| -rw-r--r-- | tactics/taccoerce.mli | 2 | ||||
| -rw-r--r-- | tactics/tacintern.ml | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 9 | ||||
| -rw-r--r-- | tactics/tacsubst.ml | 3 |
6 files changed, 14 insertions, 21 deletions
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 |