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.

11 files changed, 10 insertions, 12 deletions

diff --git a/CHANGES.md b/CHANGES.md
index 1070e4e433..9d584989aa 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -95,7 +95,7 @@ Tactics
   by posing the specifying equation for `Z.div` and `Z.modulo` before
   replacing them with atoms.
 
-- Ltac backtraces can be turned off using the "Ltac Backtrace" option.
+- Ltac backtraces can be turned on using the "Ltac Backtrace" option.
 
 Vernacular commands
 
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
diff --git a/test-suite/output/Errors.v b/test-suite/output/Errors.v
index edc35f17b4..b52537dec0 100644
--- a/test-suite/output/Errors.v
+++ b/test-suite/output/Errors.v
@@ -1,6 +1,8 @@
 (* coq-prog-args: ("-top" "Errors") *)
 (* Test error messages *)
 
+Set Ltac Backtrace.
+
 (* Test non-regression of bug fixed in r13486 (bad printer for module names) *)
 
 Module Type S.
diff --git a/test-suite/output/FunExt.out b/test-suite/output/FunExt.out
index 8d2a125c1d..2a823396d5 100644
--- a/test-suite/output/FunExt.out
+++ b/test-suite/output/FunExt.out
@@ -1,19 +1,12 @@
 The command has indeed failed with message:
-Ltac call to "extensionality in (var)" failed.
 Tactic failure: Not an extensional equality.
 The command has indeed failed with message:
-Ltac call to "extensionality in (var)" failed.
 Tactic failure: Not an extensional equality.
 The command has indeed failed with message:
-Ltac call to "extensionality in (var)" failed.
 Tactic failure: Not an extensional equality.
 The command has indeed failed with message:
-Ltac call to "extensionality in (var)" failed.
 Tactic failure: Not an extensional equality.
 The command has indeed failed with message:
-Ltac call to "extensionality in (var)" failed.
 Tactic failure: Already an intensional equality.
 The command has indeed failed with message:
-In nested Ltac calls to "extensionality in (var)" and
-"clearbody (ne_var_list)", last call failed.
 Hypothesis e depends on the body of H'
diff --git a/test-suite/output/TypeclassDebug.out b/test-suite/output/TypeclassDebug.out
index 8b38fe0ff4..7ea7a08cb3 100644
--- a/test-suite/output/TypeclassDebug.out
+++ b/test-suite/output/TypeclassDebug.out
@@ -14,5 +14,4 @@ Debug: 1.1-1.1-1.1-1.1-1: looking for foo without backtracking
 Debug: 1.1-1.1-1.1-1.1-1.1: simple apply H on foo, 1 subgoal(s)
 Debug: 1.1-1.1-1.1-1.1-1.1-1 : foo
 The command has indeed failed with message:
-Ltac call to "typeclasses eauto (int_or_var_opt) with (ne_preident_list)" failed.
 Tactic failure: Proof search reached its limit.
diff --git a/test-suite/output/bug5778.v b/test-suite/output/bug5778.v
index 0dcd76aeff..441e87af84 100644
--- a/test-suite/output/bug5778.v
+++ b/test-suite/output/bug5778.v
@@ -1,3 +1,4 @@
+Set Ltac Backtrace.
 Ltac a _ := pose (I : I).
 Ltac b _ := a ().
 Ltac abs _ := abstract b ().
diff --git a/test-suite/output/bug6404.v b/test-suite/output/bug6404.v
index bbe6b1a00f..d9e5e20b66 100644
--- a/test-suite/output/bug6404.v
+++ b/test-suite/output/bug6404.v
@@ -1,3 +1,4 @@
+Set Ltac Backtrace.
 Ltac a _ := pose (I : I).
 Ltac b _ := a ().
 Ltac abs _ := transparent_abstract b ().
diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v
index 40e743c3f0..fcd5dd05f0 100644
--- a/test-suite/output/ltac.v
+++ b/test-suite/output/ltac.v
@@ -1,3 +1,5 @@
+Set Ltac Backtrace.
+
 (* This used to refer to b instead of z sometimes between 8.4 and 8.5beta3 *)
 Goal True.
 Fail let T := constr:((fun a b : nat => a+b) 1 1) in
diff --git a/test-suite/output/ltac_missing_args.v b/test-suite/output/ltac_missing_args.v
index 91331a1de5..e30c97aac6 100644
--- a/test-suite/output/ltac_missing_args.v
+++ b/test-suite/output/ltac_missing_args.v
@@ -1,3 +1,5 @@
+Set Ltac Backtrace.
+
 Ltac foo x := idtac x.
 Ltac bar x := fun y _ => idtac x y.
 Ltac baz := foo.
diff --git a/test-suite/output/ssr_clear.out b/test-suite/output/ssr_clear.out
index 1515954060..1a0f90493e 100644
--- a/test-suite/output/ssr_clear.out
+++ b/test-suite/output/ssr_clear.out
@@ -1,3 +1,2 @@
 The command has indeed failed with message:
-Ltac call to "move (ssrmovearg) (ssrclauses)" failed.
 No assumption is named NO_SUCH_NAME
diff --git a/test-suite/output/ssr_explain_match.out b/test-suite/output/ssr_explain_match.out
index 32cfb354bf..0f68ab0b02 100644
--- a/test-suite/output/ssr_explain_match.out
+++ b/test-suite/output/ssr_explain_match.out
@@ -51,5 +51,4 @@ instance: (addnC y x) matches: (x + y)
 instance: (addnC y x) matches: (x + y)
 END INSTANCES
 The command has indeed failed with message:
-Ltac call to "ssrinstancesoftpat (cpattern)" failed.
 Not supported