diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-13 17:57:41 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-13 17:57:41 +0000 |
| commit | edcf0d8b8bff399443ddf4cd436185c33bf59829 (patch) | |
| tree | b95d6dd4ae5ccae0114b2fa27c00bcd89f445f78 /plugins/funind/g_indfun.ml4 | |
| parent | 1b906116b43f5975fef7bb6f4dfb9589cfe3d6ee (diff) | |
A new mechanism to handle errors.
Instead of the monolitic Cerrors, I introduce a lightweight Errors module
whose error message can be expanded by module introducing exceptions.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14119 85f007b7-540e-0410-9357-904b9bb8a0f7
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 39f4cf07f..53ddfb967 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -180,12 +180,12 @@ let warning_error names e = Pp.msg_warning (str "Cannot define graph(s) for " ++ h 1 (prlist_with_sep (fun _ -> str","++spc ()) Libnames.pr_reference names) ++ - if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ()) + if do_observe () then (spc () ++ Errors.print e) else mt ()) | Defining_principle e -> Pp.msg_warning (str "Cannot define principle(s) for "++ h 1 (prlist_with_sep (fun _ -> str","++spc ()) Libnames.pr_reference names) ++ - if do_observe () then Cerrors.explain_exn e else mt ()) + if do_observe () then Errors.print e else mt ()) | _ -> raise e |