diff options
Diffstat (limited to 'plugins/subtac')
| -rw-r--r-- | plugins/subtac/subtac_obligations.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml index 01bd3d998a..18752c9f9a 100644 --- a/plugins/subtac/subtac_obligations.ml +++ b/plugins/subtac/subtac_obligations.ml @@ -494,7 +494,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 (Errors.print e) + with e -> pperror (Errors.print (Cerrors.process_vernac_interp_error e)) in match res with | Remain n when n > 0 -> |