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.
---
 test-suite/output/TypeclassDebug.out | 1 -
 1 file changed, 1 deletion(-)

(limited to 'test-suite/output/TypeclassDebug.out')

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