diff options
| author | Pierre-Marie Pédrot | 2014-01-30 15:30:01 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-01-30 16:02:33 +0100 |
| commit | 1059ecce2a2662e4d8f335bd4db743df70b100b1 (patch) | |
| tree | 236cad1f42ecaea078f8a0fb17dd17eec81631e0 /toplevel/stm.ml | |
| parent | a5e78ef4a8450991c6f1ee748b720eb0d54d04d2 (diff) | |
Fixing backtrace handling here and there.
Diffstat (limited to 'toplevel/stm.ml')
| -rw-r--r-- | toplevel/stm.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/toplevel/stm.ml b/toplevel/stm.ml index 613ff672bf..ac041a9f78 100644 --- a/toplevel/stm.ml +++ b/toplevel/stm.ml @@ -49,7 +49,9 @@ let vernac_interp ?proof id { verbose; loc; expr } = Aux_file.record_in_aux_set_at loc; prerr_endline ("interpreting " ^ string_of_ppcmds(pr_vernac expr)); try Vernacentries.interp ~verbosely:verbose ?proof (loc, expr) - with e -> raise (Errors.push (Cerrors.process_vernac_interp_error e)) + with e -> + let e = Errors.push e in + raise (Cerrors.process_vernac_interp_error e) end (* Wrapper for Vernac.parse_sentence to set the feedback id *) |