diff options
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 -> |