aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/tac2core.ml6
1 files changed, 4 insertions, 2 deletions
diff --git a/src/tac2core.ml b/src/tac2core.ml
index f19f45fa4e..7bd0164b4d 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -107,8 +107,10 @@ let fatal_flag : unit Exninfo.t = Exninfo.make ()
let fatal_info = Exninfo.add Exninfo.null fatal_flag ()
let set_bt info =
- Tac2interp.get_backtrace >>= fun bt ->
- Proofview.tclUNIT (Exninfo.add info Tac2entries.backtrace bt)
+ if !Tac2interp.print_ltac2_backtrace then
+ Tac2interp.get_backtrace >>= fun bt ->
+ Proofview.tclUNIT (Exninfo.add info Tac2entries.backtrace bt)
+ else Proofview.tclUNIT info
let throw ?(info = Exninfo.null) e =
set_bt info >>= fun info ->