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/invfun.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'plugins/funind/invfun.ml') 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)); -- cgit v1.2.3