diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/elim.ml | 26 | ||||
| -rw-r--r-- | tactics/elim.mli | 2 | ||||
| -rw-r--r-- | tactics/hiddentac.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 21 | ||||
| -rw-r--r-- | tactics/tactics.mli | 32 |
5 files changed, 50 insertions, 33 deletions
diff --git a/tactics/elim.ml b/tactics/elim.ml index ffe2ff0715..81a5cfc54c 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -97,15 +97,16 @@ let head_in gls indl t = in List.mem ity indl with Induc -> false -let inductive_of_ident gls id = - match kind_of_term (pf_global gls id) with +let inductive_of_qualid gls qid = + let c = Declare.construct_qualified_reference (pf_env gls) qid in + match kind_of_term c with | IsMutInd ity -> ity | _ -> errorlabstrm "Decompose" - [< pr_id id; 'sTR " is not an inductive type" >] + [< Nametab.pr_qualid qid; 'sTR " is not an inductive type" >] let decompose_these c l gls = - let indl = List.map (inductive_of_ident gls) l in + let indl = List.map (inductive_of_qualid gls) l in general_decompose (fun (_,t) -> head_in gls indl t) c gls let decompose_nonrec c gls = @@ -123,17 +124,22 @@ let decompose_or c gls = (fun (_,t) -> is_disjunction t) c gls -let dyn_decompose args gl = +let dyn_decompose args gl = + let out_qualid = function + | Qualid qid -> qid + | l -> bad_tactic_args "DecomposeThese" [l] gl in match args with - | [Clause ids; Command c] -> - decompose_these (pf_interp_constr gl c) ids gl - | [Clause ids; Constr c] -> - decompose_these c ids gl + | Command c :: ids -> + decompose_these (pf_interp_constr gl c) (List.map out_qualid ids) gl + | Constr c :: ids -> + decompose_these c (List.map out_qualid ids) gl | l -> bad_tactic_args "DecomposeThese" l gl let h_decompose = let v_decompose = hide_tactic "DecomposeThese" dyn_decompose in - fun ids c -> v_decompose [Clause ids; Constr c] + fun ids c -> + v_decompose + (Constr c :: List.map (fun x -> Qualid (Nametab.qualid_of_sp x)) ids) let vernac_decompose_and = hide_constr_tactic "DecomposeAnd" decompose_and diff --git a/tactics/elim.mli b/tactics/elim.mli index e2b9a75e35..c21d4452b9 100644 --- a/tactics/elim.mli +++ b/tactics/elim.mli @@ -29,7 +29,7 @@ val general_decompose : (clause * constr -> bool) -> constr -> tactic val decompose_nonrec : constr -> tactic val decompose_and : constr -> tactic val decompose_or : constr -> tactic -val h_decompose : identifier list -> constr -> tactic +val h_decompose : section_path list -> constr -> tactic val double_ind : int -> int -> tactic diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index 2c4f80b748..bc07c9a4d6 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -13,7 +13,7 @@ open Proof_type open Tacmach open Tacentries -let h_clear ids = v_clear [(Clause ids)] +let h_clear ids = v_clear [(Clause (List.map (fun x -> InHyp x) ids))] let h_move dep id1 id2 = (if dep then v_move else v_move_dep) [Identifier id1;Identifier id2] let h_contradiction = v_contradiction [] diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2d68a721f0..0e454846a0 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -152,11 +152,20 @@ type 'a tactic_reduction = env -> enamed_declarations -> constr -> constr let reduct_in_concl redfun gl = convert_concl (pf_reduce redfun gl (pf_concl gl)) gl -let reduct_in_hyp redfun id gl = - let ty = pf_get_hyp_typ gl id in +let reduct_in_hyp redfun idref gl = + let inhyp,id = match idref with + | InHyp id -> true, id + | InHypType id -> false, id in + let c, ty = pf_get_hyp gl id in let redfun' = under_casts (pf_reduce redfun gl) in - convert_hyp id (redfun' ty) gl - + match c with + | None -> convert_hyp id (redfun' ty) gl + | Some b -> + if inhyp then (* Default for defs: reduce in body *) + convert_defbody id (redfun' b) gl + else + convert_deftype id (redfun' ty) gl + let reduct_option redfun = function | Some id -> reduct_in_hyp redfun id | None -> reduct_in_concl redfun @@ -783,7 +792,9 @@ let dyn_assumption = function let clear ids gl = thin ids gl let clear_one id gl = clear [id] gl let dyn_clear = function - | [Clause ids] -> clear ids + | [Clause ids] -> + let out = function InHyp id -> id | _ -> assert false in + clear (List.map out ids) | _ -> assert false (* Clears a list of identifiers clauses form the context *) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 07db3b4590..6f315f358b 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -102,39 +102,39 @@ val dyn_exact_check : tactic_arg list -> tactic type 'a tactic_reduction = env -> enamed_declarations -> constr -> constr -val reduct_in_hyp : 'a tactic_reduction -> identifier -> tactic -val reduct_option : 'a tactic_reduction -> identifier option -> tactic +val reduct_in_hyp : 'a tactic_reduction -> hyp_location -> tactic +val reduct_option : 'a tactic_reduction -> hyp_location option -> tactic val reduct_in_concl : 'a tactic_reduction -> tactic val change_in_concl : constr -> tactic -val change_in_hyp : constr -> identifier -> tactic -val change_option : constr -> identifier option -> tactic +val change_in_hyp : constr -> hyp_location -> tactic +val change_option : constr -> hyp_location option -> tactic val red_in_concl : tactic -val red_in_hyp : identifier -> tactic -val red_option : identifier option -> tactic +val red_in_hyp : hyp_location -> tactic +val red_option : hyp_location option -> tactic val hnf_in_concl : tactic -val hnf_in_hyp : identifier -> tactic -val hnf_option : identifier option -> tactic +val hnf_in_hyp : hyp_location -> tactic +val hnf_option : hyp_location option -> tactic val simpl_in_concl : tactic -val simpl_in_hyp : identifier -> tactic -val simpl_option : identifier option -> tactic +val simpl_in_hyp : hyp_location -> tactic +val simpl_option : hyp_location option -> tactic val normalise_in_concl: tactic -val normalise_in_hyp : identifier -> tactic -val normalise_option : identifier option -> tactic +val normalise_in_hyp : hyp_location -> tactic +val normalise_option : hyp_location option -> tactic val unfold_in_concl : (int list * Closure.evaluable_global_reference) list -> tactic val unfold_in_hyp : - (int list * Closure.evaluable_global_reference) list -> identifier -> tactic + (int list * Closure.evaluable_global_reference) list -> hyp_location -> tactic val unfold_option : - (int list * Closure.evaluable_global_reference) list -> identifier option + (int list * Closure.evaluable_global_reference) list -> hyp_location option -> tactic -val reduce : red_expr -> identifier list -> tactic +val reduce : red_expr -> hyp_location list -> tactic val dyn_reduce : tactic_arg list -> tactic val dyn_change : tactic_arg list -> tactic val unfold_constr : global_reference -> tactic val pattern_option : - (int list * constr * constr) list -> identifier option -> tactic + (int list * constr * constr) list -> hyp_location option -> tactic (*s Modification of the local context. *) |