From edcf0d8b8bff399443ddf4cd436185c33bf59829 Mon Sep 17 00:00:00 2001 From: aspiwack Date: Fri, 13 May 2011 17:57:41 +0000 Subject: 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 --- plugins/funind/g_indfun.ml4 | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/funind/g_indfun.ml4') 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 -- cgit v1.2.3