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 | |
| parent | a5e78ef4a8450991c6f1ee748b720eb0d54d04d2 (diff) | |
Fixing backtrace handling here and there.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/cerrors.ml | 4 | ||||
| -rw-r--r-- | toplevel/stm.ml | 4 |
2 files changed, 6 insertions, 2 deletions
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index afe08053f4..580e37cdc1 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -118,7 +118,9 @@ let rec process_vernac_interp_error exn = match exn with exc let rec strip_wrapping_exceptions = function - | Proof_errors.TacticFailure e -> strip_wrapping_exceptions e + | Proof_errors.TacticFailure e as src -> + let e = Backtrace.app_backtrace ~src ~dst:e in + strip_wrapping_exceptions e | exc -> exc let process_vernac_interp_error exc = 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 *) |