diff options
| author | Pierre-Marie Pédrot | 2017-09-09 20:40:11 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-09 20:40:11 +0200 |
| commit | a059c181c3b2d6c1f9c3682c15270c0942430f39 (patch) | |
| tree | ac85208fe717887ab81846390da422c17f923a2a /src | |
| parent | 254785a4a7f8373b5b0c4a289c2184cac3b5c420 (diff) | |
Fix coq/ltac2#18: Terms should show a backtrace when Set Ltac2 Backtrace is set.
Diffstat (limited to 'src')
| -rw-r--r-- | src/tac2core.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/tac2core.ml b/src/tac2core.ml index ab87fa7739..9920b4c805 100644 --- a/src/tac2core.ml +++ b/src/tac2core.ml @@ -799,6 +799,7 @@ let interp_constr flags ist c = Proofview.tclUNIT c with e when catchable_exception e -> let (e, info) = CErrors.push e in + set_bt info >>= fun info -> match Exninfo.get info fatal_flag with | None -> Proofview.tclZERO ~info e | Some () -> throw ~info e |