diff options
Diffstat (limited to 'plugins/funind/invfun.ml')
| -rw-r--r-- | plugins/funind/invfun.ml | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index d979401424..628e582e23 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -19,6 +19,7 @@ open Tactics open Indfun_common open Tacmach open Misctypes +open Termops (* Some pretty printing function for debugging purpose *) @@ -70,8 +71,8 @@ let do_observe_tac s tac g = with reraise -> let reraise = Errors.push reraise in let e = Cerrors.process_vernac_interp_error reraise in - observe (str "observation "++ s++str " raised exception " ++ - Errors.iprint e ++ str " on goal " ++ goal ); + observe (hov 0 (str "observation "++ s++str " raised exception " ++ + Errors.iprint e ++ str " on goal" ++ fnl() ++ goal )); iraise reraise;; @@ -457,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) @@ -698,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 @@ -737,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))))) @@ -920,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 @@ -964,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)); |