diff options
Diffstat (limited to 'plugins/funind/g_indfun.ml4')
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 6dfc23511..c63527dea 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -193,12 +193,12 @@ let warning_error names e = let (e, _) = Cerrors.process_vernac_interp_error (e, Exninfo.null) in match e with | Building_graph e -> - Pp.msg_warning + 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 -> - Pp.msg_warning + 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 ()) |