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 /proofs/proofview.ml | |
| parent | a5e78ef4a8450991c6f1ee748b720eb0d54d04d2 (diff) | |
Fixing backtrace handling here and there.
Diffstat (limited to 'proofs/proofview.ml')
| -rw-r--r-- | proofs/proofview.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index a0c64d29d0..013b2f2047 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -582,7 +582,9 @@ let tclTIMEOUT n t = end begin function | Proof_errors.Timeout -> Proofview_monad.NonLogical.ret (Util.Inr Timeout) - | Proof_errors.TacticFailure e -> Proofview_monad.NonLogical.ret (Util.Inr e) + | Proof_errors.TacticFailure e as src -> + let e = Backtrace.app_backtrace ~src ~dst:e in + Proofview_monad.NonLogical.ret (Util.Inr e) | e -> Proofview_monad.NonLogical.raise e end end >>= function |