From 151ec20b1202df17b75a7c8d3fe9f8ff258a88bd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 5 Dec 2018 16:09:36 +0100
Subject: Unset the Ltac backtrace printing by default.

This is only used for debugging, if a user wants more feedback she can turn
on the option. Conversely, it has a cost for any tactic script, so it is
wiser to disable it by default.
---
 plugins/ltac/tacinterp.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index b55cb08c90..31e6b4c28f 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -117,7 +117,7 @@ let combine_appl appl1 appl2 =
 let of_tacvalue v = in_gen (topwit wit_tacvalue) v
 let to_tacvalue v = out_gen (topwit wit_tacvalue) v
 
-let log_trace = ref true
+let log_trace = ref false
 
 let is_traced () =
   !log_trace || !Flags.profile_ltac
-- 
cgit v1.2.3