diff options
Diffstat (limited to 'plugins/subtac/g_subtac.ml4')
| -rw-r--r-- | plugins/subtac/g_subtac.ml4 | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4 index 956ccf09..6e7a8d32 100644 --- a/plugins/subtac/g_subtac.ml4 +++ b/plugins/subtac/g_subtac.ml4 @@ -90,7 +90,8 @@ VERNAC COMMAND EXTEND Subtac let try_catch_exn f e = try f e - with exn -> errorlabstrm "Program" (Errors.print exn) + with exn when Errors.noncritical 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 |