diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/hiddentac.ml | 8 | ||||
| -rw-r--r-- | tactics/hiddentac.mli | 12 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 30 | ||||
| -rw-r--r-- | tactics/tactics.ml | 17 | ||||
| -rw-r--r-- | tactics/tactics.mli | 4 |
5 files changed, 39 insertions, 32 deletions
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index d5ee78fea..20b70cef4 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -84,12 +84,12 @@ let out_indarg = function | ElimOnAnonHyp n -> ElimOnAnonHyp n let h_induction_destruct isrec ev lcl = - let lcl' = on_fst (List.map (fun (a,b,c) ->(List.map out_indarg a,b,c))) lcl in + let lcl' = on_pi1 (List.map (fun (a,b) ->(out_indarg a,b))) lcl in abstract_tactic (TacInductionDestruct (isrec,ev,lcl')) (induction_destruct isrec ev lcl) -let h_new_induction ev c e idl cl = - h_induction_destruct true ev ([c,e,idl],cl) -let h_new_destruct ev c e idl cl = h_induction_destruct false ev ([c,e,idl],cl) +let h_new_induction ev c idl e cl = + h_induction_destruct true ev ([c,idl],e,cl) +let h_new_destruct ev c idl e cl = h_induction_destruct false ev ([c,idl],e,cl) let h_specialize n d = abstract_tactic (TacSpecialize (n,d)) (specialize n d) let h_lapply c = abstract_tactic (TacLApply c) (cut_and_apply c) diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index cffe84252..3028d3a1e 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -68,19 +68,19 @@ val h_simple_induction : quantified_hypothesis -> tactic val h_simple_destruct : quantified_hypothesis -> tactic val h_simple_induction_destruct : rec_flag -> quantified_hypothesis -> tactic val h_new_induction : evars_flag -> - (evar_map * constr with_bindings) induction_arg list -> - constr with_bindings option -> + (evar_map * constr with_bindings) induction_arg -> intro_pattern_expr located option * intro_pattern_expr located option -> + constr with_bindings option -> Locus.clause option -> tactic val h_new_destruct : evars_flag -> - (evar_map * constr with_bindings) induction_arg list -> - constr with_bindings option -> + (evar_map * constr with_bindings) induction_arg -> intro_pattern_expr located option * intro_pattern_expr located option -> + constr with_bindings option -> Locus.clause option -> tactic val h_induction_destruct : rec_flag -> evars_flag -> - ((evar_map * constr with_bindings) induction_arg list * - constr with_bindings option * + ((evar_map * constr with_bindings) induction_arg * (intro_pattern_expr located option * intro_pattern_expr located option)) list + * constr with_bindings option * Locus.clause option -> tactic val h_specialize : int option -> constr with_bindings -> tactic diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 2beba9888..3eddb1aae 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -732,12 +732,12 @@ let rec intern_atomic lf ist x = (* Derived basic tactics *) | TacSimpleInductionDestruct (isrec,h) -> TacSimpleInductionDestruct (isrec,intern_quantified_hypothesis ist h) - | TacInductionDestruct (ev,isrec,(l,cls)) -> - TacInductionDestruct (ev,isrec,(List.map (fun (lc,cbo,(ipato,ipats)) -> - (List.map (intern_induction_arg ist) lc, - Option.map (intern_constr_with_bindings ist) cbo, + | TacInductionDestruct (ev,isrec,(l,el,cls)) -> + TacInductionDestruct (ev,isrec,(List.map (fun (c,(ipato,ipats)) -> + (intern_induction_arg ist c, (Option.map (intern_intro_pattern lf ist) ipato, Option.map (intern_intro_pattern lf ist) ipats))) l, + Option.map (intern_constr_with_bindings ist) el, Option.map (clause_app (intern_hyp_location ist)) cls)) | TacDoubleInduction (h1,h2) -> let h1 = intern_quantified_hypothesis ist h1 in @@ -2424,17 +2424,17 @@ and interp_atomic ist gl tac = (* Derived basic tactics *) | TacSimpleInductionDestruct (isrec,h) -> h_simple_induction_destruct isrec (interp_quantified_hypothesis ist h) - | TacInductionDestruct (isrec,ev,(l,cls)) -> + | TacInductionDestruct (isrec,ev,(l,el,cls)) -> let sigma, l = - list_fold_map (fun sigma (lc,cbo,(ipato,ipats)) -> - let lc = List.map (interp_induction_arg ist gl) lc in - let sigma,cbo = - Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in - (sigma,(lc,cbo, + list_fold_map (fun sigma (c,(ipato,ipats)) -> + let c = interp_induction_arg ist gl c in + (sigma,(c, (Option.map (interp_intro_pattern ist gl) ipato, Option.map (interp_intro_pattern ist gl) ipats)))) sigma l in + let sigma,el = + Option.fold_map (interp_constr_with_bindings ist env) sigma el in let cls = Option.map (interp_clause ist gl) cls in - tclWITHHOLES ev (h_induction_destruct isrec ev) sigma (l,cls) + tclWITHHOLES ev (h_induction_destruct isrec ev) sigma (l,el,cls) | TacDoubleInduction (h1,h2) -> let h1 = interp_quantified_hypothesis ist h1 in let h2 = interp_quantified_hypothesis ist h2 in @@ -2862,10 +2862,10 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with (* Derived basic tactics *) | TacSimpleInductionDestruct (isrec,h) as x -> x - | TacInductionDestruct (isrec,ev,(l,cls)) -> - TacInductionDestruct (isrec,ev,(List.map (fun (lc,cbo,ids) -> - List.map (subst_induction_arg subst) lc, - Option.map (subst_glob_with_bindings subst) cbo, ids) l, cls)) + | TacInductionDestruct (isrec,ev,(l,el,cls)) -> + let l' = List.map (fun (c,ids) -> subst_induction_arg subst c, ids) l in + 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) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index ad44171da..44bda9aac 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3207,12 +3207,19 @@ let induct_destruct isrec with_evars (lc,elim,names,cls) gl = end let induction_destruct isrec with_evars = function - | [],_ -> tclIDTAC - | [a,b,c],cl -> induct_destruct isrec with_evars (a,b,c,cl) - | (a,b,c)::l,cl -> + | [],_,_ -> tclIDTAC + | [a,b],el,cl -> induct_destruct isrec with_evars ([a],el,b,cl) + | (a,b)::l,None,cl -> tclTHEN - (induct_destruct isrec with_evars (a,b,c,cl)) - (tclMAP (fun (a,b,c) -> induct_destruct false with_evars (a,b,c,cl)) l) + (induct_destruct isrec with_evars ([a],None,b,cl)) + (tclMAP (fun (a,b) -> induct_destruct false with_evars ([a],None,b,cl)) l) + | l,Some el,cl -> + let check_basic_using = function + | a,(None,None) -> a + | _ -> error "Unsupported syntax for \"using\"." + in + let l' = List.map check_basic_using l in + induct_destruct isrec with_evars (l', Some el, (None,None), cl) let new_induct ev lc e idl cls = induct_destruct true ev (lc,e,idl,cls) let new_destruct ev lc e idl cls = induct_destruct false ev (lc,e,idl,cls) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 6cdac9d55..b1abb67a9 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -295,10 +295,10 @@ val new_destruct : evars_flag -> (** {6 Generic case analysis / induction tactics. } *) val induction_destruct : rec_flag -> evars_flag -> - ((evar_map * constr with_bindings) induction_arg list * - constr with_bindings option * + ((evar_map * constr with_bindings) induction_arg * (intro_pattern_expr located option * intro_pattern_expr located option)) list * + constr with_bindings option * clause option -> tactic (** {6 Eliminations giving the type instead of the proof. } *) |