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, 23 insertions, 32 deletions
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 93a89330e3..893baad8c9 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -198,13 +198,15 @@ let warning_error names e = let (e, _) = Cerrors.process_vernac_interp_error (e, Exninfo.null) in match e with | Building_graph e -> - 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) + 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 ()) | Defining_principle e -> - 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) + 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 ()) | _ -> raise e diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 2ebbb34e4c..1c5eb16218 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -227,11 +227,6 @@ 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 @@ -274,20 +269,14 @@ let derive_inversion fix_names = lind; with e when Errors.noncritical e -> let e' = process_vernac_interp_error e in - warn_funind_cannot_build_inversion e' + Feedback.msg_warning + (str "Cannot build inversion information" ++ + if do_observe () then (fnl() ++ Errors.print e') else mt ()) with e when Errors.noncritical e -> - 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 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 warning_error names e = let e = process_vernac_interp_error e in @@ -305,11 +294,15 @@ let warning_error names e = in match e with | Building_graph e -> - let names = prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names in - warn_cannot_define_graph (names,e_explain 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) | Defining_principle e -> - let names = prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names in - warn_cannot_define_principle (names,e_explain 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) | _ -> raise e let error_error names e = diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index 1c27bdface..e720691406 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -1,9 +1,5 @@ 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 -> |