diff options
Diffstat (limited to 'proofs/proofview.ml')
| -rw-r--r-- | proofs/proofview.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 055cd14b6..22d908e94 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -723,8 +723,9 @@ module V82 = struct let init = { solution = gls.Evd.sigma ; comb = [gls.Evd.it] } in let (_,final,_) = apply (Goal.V82.env gls.Evd.sigma gls.Evd.it) t init in { Evd.sigma = final.solution ; it = final.comb } - with Proof_errors.TacticFailure e -> - let e = Errors.push e in + with Proof_errors.TacticFailure e as src -> + let src = Errors.push src in + let e = Backtrace.app_backtrace ~src ~dst:e in raise e let put_status b = |