diff options
Diffstat (limited to 'toplevel/obligations.ml')
| -rw-r--r-- | toplevel/obligations.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index d5073802d..aa0685861 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -839,7 +839,8 @@ let rec solve_obligation prg num tac = obls (pred rem) with e when Errors.noncritical e -> - pperror (Errors.print (Cerrors.process_vernac_interp_error e)) + let e = Errors.push e in + pperror (Errors.iprint (Cerrors.process_vernac_interp_error e)) in match res with | Remain n when n > 0 -> @@ -892,7 +893,7 @@ and solve_obligation_by_tac prg obls i tac = true else false with e when Errors.noncritical e -> - let e = Errors.push e in + let (e, _) = Errors.push e in match e with | Refiner.FailError (_, s) -> user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s) |