diff options
| -rw-r--r-- | stm/stm.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 4a303f036..ed7c234c1 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1577,7 +1577,8 @@ end = struct (* {{{ *) vernac_interp r_for { r_what with verbose = true }; feedback ~state_id:r_for Feedback.Processed with e when Errors.noncritical e -> - let msg = string_of_ppcmds (print e) in + let e = Errors.push e in + let msg = string_of_ppcmds (iprint e) in feedback ~state_id:r_for (Feedback.ErrorMsg (Loc.ghost, msg)) let name_of_task { t_what } = string_of_ppcmds (pr_ast t_what) |