diff options
| author | Pierre-Marie Pédrot | 2017-09-09 20:45:48 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-09 20:46:02 +0200 |
| commit | 6bc632021b47103b57abb34836766a57198d9cb4 (patch) | |
| tree | 4ddb0538aae3e61a725726a42efe20b39176c5d7 /src | |
| parent | 91a9313fbe24dfb0c9b7fcaa31e3c11bf055450a (diff) | |
Update backtraces only when the Ltac2 Backtrace flag is set.
Diffstat (limited to 'src')
| -rw-r--r-- | src/tac2core.ml | 6 |
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 -> |