diff options
| author | Pierre-Marie Pédrot | 2014-04-25 13:59:39 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-04-25 14:00:43 +0200 |
| commit | b35edb34769fecd4dbdf7030222ba3078eab1c93 (patch) | |
| tree | 0efb56c5711b0a2d9ae8eef5b7792b734899f2be /proofs | |
| parent | a5e0b28f9344744edf2209001fe047b1535775f6 (diff) | |
Fixing various backtrace recordings.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/pfedit.ml | 1 | ||||
| -rw-r--r-- | proofs/proofview.ml | 5 |
2 files changed, 4 insertions, 2 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 68c2ed3288..f45eb2a3aa 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -126,6 +126,7 @@ let build_constant_by_tactic id sign ?(goal_kind = Global,Proof Theorem) typ tac delete_current_proof (); const, status with reraise -> + let reraise = Errors.push reraise in delete_current_proof (); raise reraise diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 055cd14b60..22d908e94c 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 = |