From 6bc632021b47103b57abb34836766a57198d9cb4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 9 Sep 2017 20:45:48 +0200
Subject: Update backtraces only when the Ltac2 Backtrace flag is set.

---
 src/tac2core.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'src')

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 ->
-- 
cgit v1.2.3