diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 14 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 37 | ||||
| -rw-r--r-- | plugins/funind/indfun.mli | 4 |
3 files changed, 32 insertions, 23 deletions
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 893baad8c9..93a89330e3 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -198,15 +198,13 @@ let warning_error names e = let (e, _) = Cerrors.process_vernac_interp_error (e, Exninfo.null) in match e with | Building_graph e -> - Feedback.msg_warning - (str "Cannot define graph(s) for " ++ - h 1 (pr_enum Libnames.pr_reference names) ++ - if do_observe () then (spc () ++ Errors.print e) else mt ()) + let names = pr_enum Libnames.pr_reference names in + let error = if do_observe () then (spc () ++ Errors.print e) else mt () in + warn_cannot_define_graph (names,error) | Defining_principle e -> - Feedback.msg_warning - (str "Cannot define principle(s) for "++ - h 1 (pr_enum Libnames.pr_reference names) ++ - if do_observe () then Errors.print e else mt ()) + let names = pr_enum Libnames.pr_reference names in + let error = if do_observe () then Errors.print e else mt () in + warn_cannot_define_principle (names,error) | _ -> raise e diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 1c5eb16218..2ebbb34e4c 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -227,6 +227,11 @@ let prepare_body ((name,_,args,types,_),_) rt = let process_vernac_interp_error e = fst (Cerrors.process_vernac_interp_error (e, Exninfo.null)) +let warn_funind_cannot_build_inversion = + CWarnings.create ~name:"funind-cannot-build-inversion" ~category:"funind" + (fun e' -> strbrk "Cannot build inversion information" ++ + if do_observe () then (fnl() ++ Errors.print e') else mt ()) + let derive_inversion fix_names = try let evd' = Evd.from_env (Global.env ()) in @@ -269,14 +274,20 @@ let derive_inversion fix_names = lind; with e when Errors.noncritical e -> let e' = process_vernac_interp_error e in - Feedback.msg_warning - (str "Cannot build inversion information" ++ - if do_observe () then (fnl() ++ Errors.print e') else mt ()) + warn_funind_cannot_build_inversion e' with e when Errors.noncritical e -> - let e' = process_vernac_interp_error e in - Feedback.msg_warning - (str "Cannot build inversion information (early)" ++ - if do_observe () then (fnl() ++ Errors.print e') else mt ()) + let e' = process_vernac_interp_error e in + warn_funind_cannot_build_inversion e' + +let warn_cannot_define_graph = + CWarnings.create ~name:"funind-cannot-define-graph" ~category:"funind" + (fun (names,error) -> strbrk "Cannot define graph(s) for " ++ + h 1 names ++ error) + +let warn_cannot_define_principle = + CWarnings.create ~name:"funind-cannot-define-principle" ~category:"funind" + (fun (names,error) -> strbrk "Cannot define induction principle(s) for "++ + h 1 names ++ error) let warning_error names e = let e = process_vernac_interp_error e in @@ -294,15 +305,11 @@ let warning_error names e = in match e with | Building_graph e -> - Feedback.msg_warning - (str "Cannot define graph(s) for " ++ - h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++ - e_explain e) + let names = prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names in + warn_cannot_define_graph (names,e_explain e) | Defining_principle e -> - Feedback.msg_warning - (str "Cannot define principle(s) for "++ - h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++ - e_explain e) + let names = prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names in + warn_cannot_define_principle (names,e_explain e) | _ -> raise e let error_error names e = diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index e720691406..1c27bdface 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -1,5 +1,9 @@ open Misctypes +val warn_cannot_define_graph : ?loc:Loc.t -> Pp.std_ppcmds * Pp.std_ppcmds -> unit + +val warn_cannot_define_principle : ?loc:Loc.t -> Pp.std_ppcmds * Pp.std_ppcmds -> unit + val do_generate_principle : bool -> (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> |