From aa99912e9adc566a179b4972ff85a92b967fb134 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 7 Dec 2014 22:44:43 +0100 Subject: Removing redundant versions of generalize. --- plugins/funind/functional_principles_proofs.ml | 6 +++--- plugins/funind/invfun.ml | 10 +++++----- plugins/funind/recdef.ml | 6 +++--- 3 files changed, 11 insertions(+), 11 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 5b9f82aa5..f57f12f66 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -706,7 +706,7 @@ let build_proof in tclTHENSEQ [ - Simple.generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps)); + generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps)); thin dyn_infos.rec_hyps; pattern_option [Locus.AllOccurrencesBut [1],t] None; (fun g -> observe_tac "toto" ( @@ -933,7 +933,7 @@ let generalize_non_dep hyp g = in (* observe (str "to_revert := " ++ prlist_with_sep spc Ppconstr.pr_id to_revert); *) tclTHEN - ((* observe_tac "h_generalize" *) (Simple.generalize (List.map mkVar to_revert) )) + ((* observe_tac "h_generalize" *) (generalize (List.map mkVar to_revert) )) ((* observe_tac "thin" *) (thin to_revert)) g @@ -1563,7 +1563,7 @@ let prove_principle_for_gen Nameops.out_name (fresh_id (Name (Id.of_string ("Acc_"^(Id.to_string rec_arg_id))))) in let revert l = - tclTHEN (Tactics.Simple.generalize (List.map mkVar l)) (clear l) + tclTHEN (Tactics.generalize (List.map mkVar l)) (clear l) in let fix_id = Nameops.out_name (fresh_id (Name hrec_id)) in let prove_rec_arg_acc g = diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 363dd1b3b..628e582e2 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -458,7 +458,7 @@ let generalize_dependent_of x hyp g = tclMAP (function | (id,None,t) when not (Id.equal id hyp) && - (Termops.occur_var (pf_env g) x t) -> tclTHEN (Tactics.Simple.generalize [mkVar id]) (thin [id]) + (Termops.occur_var (pf_env g) x t) -> tclTHEN (Tactics.generalize [mkVar id]) (thin [id]) | _ -> tclIDTAC ) (pf_hyps g) @@ -699,7 +699,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = }) Locusops.onConcl ; - Simple.generalize (List.map mkVar ids); + generalize (List.map mkVar ids); thin ids ] else @@ -738,7 +738,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = tclTHENSEQ [ tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) (args_names@[res;hres]); observe_tac "h_generalize" - (Simple.generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]); + (generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]); Proofview.V82.of_tactic (Simple.intro graph_principle_id); observe_tac "" (tclTHEN_i (observe_tac "elim" (Proofview.V82.of_tactic (elim false None (mkVar hres,NoBindings) (Some (mkVar graph_principle_id,NoBindings))))) @@ -921,7 +921,7 @@ let revert_graph kn post_tac hid g = let f_args,res = Array.chop (Array.length args - 1) args in tclTHENSEQ [ - Simple.generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])]; + generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])]; thin [hid]; Proofview.V82.of_tactic (Simple.intro hid); post_tac hid @@ -965,7 +965,7 @@ let functional_inversion kn hid fconst f_correct : tactic = in tclTHENSEQ[ pre_tac hid; - Simple.generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]; + generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]; thin [hid]; Proofview.V82.of_tactic (Simple.intro hid); Proofview.V82.of_tactic (Inv.inv FullInversion None (NamedHyp hid)); diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 6867939c2..60ff10922 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -687,7 +687,7 @@ let mkDestructEq : to_revert_constr in pf_typel new_hyps (fun _ -> observe_tclTHENLIST (str "mkDestructEq") - [Simple.generalize new_hyps; + [generalize new_hyps; (fun g2 -> let changefun patvars = { run = fun sigma -> let sigma = Sigma.to_evar_map sigma in @@ -1115,7 +1115,7 @@ let termination_proof_header is_mes input_type ids args_id relation [observe_tac (str "generalize") (onNLastHypsId (nargs+1) (tclMAP (fun id -> - tclTHEN (Tactics.Simple.generalize [mkVar id]) (clear [id])) + tclTHEN (Tactics.generalize [mkVar id]) (clear [id])) )) ; observe_tac (str "fix") (fix (Some hrec) (nargs+1)); @@ -1305,7 +1305,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in observe_tclTHENLIST (str "") [ - Simple.generalize [lemma]; + generalize [lemma]; Proofview.V82.of_tactic (Simple.intro hid); (fun g -> let ids = pf_ids_of_hyps g in -- cgit v1.2.3