diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-09-28 16:33:46 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-10-08 09:51:13 +0200 |
| commit | 0de499ab4702708ddfae162389617869b170c7d7 (patch) | |
| tree | 610ac1decede9759541007f7b778a5d1406cb4af /stm/stm.ml | |
| parent | ce83c2b9fd1685e46049ee7f47c8716dcf66dbd1 (diff) | |
STM: fix backtrace handling
Diffstat (limited to 'stm/stm.ml')
| -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) |