diff options
Diffstat (limited to 'plugins/subtac/subtac.ml')
| -rw-r--r-- | plugins/subtac/subtac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml index fbdaa8d3b..710149ae4 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 |