diff options
| author | aspiwack | 2011-05-13 17:57:41 +0000 |
|---|---|---|
| committer | aspiwack | 2011-05-13 17:57:41 +0000 |
| commit | edcf0d8b8bff399443ddf4cd436185c33bf59829 (patch) | |
| tree | b95d6dd4ae5ccae0114b2fa27c00bcd89f445f78 /plugins/subtac | |
| 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/subtac')
| -rw-r--r-- | plugins/subtac/g_subtac.ml4 | 2 | ||||
| -rw-r--r-- | plugins/subtac/subtac.ml | 2 | ||||
| -rw-r--r-- | plugins/subtac/subtac_obligations.ml | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4 index c42f13b045..ca1240e5f1 100644 --- a/plugins/subtac/g_subtac.ml4 +++ b/plugins/subtac/g_subtac.ml4 @@ -90,7 +90,7 @@ VERNAC COMMAND EXTEND Subtac let try_catch_exn f e = try f e - with exn -> errorlabstrm "Program" (Cerrors.explain_exn exn) + with exn -> errorlabstrm "Program" (Errors.print exn) let subtac_obligation e = try_catch_exn Subtac_obligations.subtac_obligation e let next_obligation e = try_catch_exn Subtac_obligations.next_obligation e diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml index fbdaa8d3b1..710149ae4f 100644 --- a/plugins/subtac/subtac.ml +++ b/plugins/subtac/subtac.ml @@ -224,5 +224,5 @@ let subtac (loc, command) = Loc.Exc_located (loc, e') as e) -> raise e | e -> - (* msg_warning (str "Uncaught exception: " ++ Cerrors.explain_exn e); *) + (* msg_warning (str "Uncaught exception: " ++ Errors.print e); *) raise e diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml index 76cc7644d6..5c2f24a673 100644 --- a/plugins/subtac/subtac_obligations.ml +++ b/plugins/subtac/subtac_obligations.ml @@ -482,7 +482,7 @@ let rec solve_obligation prg num tac = let obls = Array.copy obls in let _ = obls.(num) <- obl in let res = try update_obls prg obls (pred rem) - with e -> pperror (Cerrors.explain_exn e) + with e -> pperror (Errors.print e) in match res with | Remain n when n > 0 -> |