diff options
| author | Pierre-Marie Pédrot | 2018-12-05 16:09:36 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-05 12:09:44 +0100 |
| commit | 151ec20b1202df17b75a7c8d3fe9f8ff258a88bd (patch) | |
| tree | 155191f6c749036ad6b1c779e2714cb0fb597802 /test-suite/output/TypeclassDebug.out | |
| parent | 785d2008988d73d2ec1c93940d9c93084d1acbbc (diff) | |
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.
Diffstat (limited to 'test-suite/output/TypeclassDebug.out')
| -rw-r--r-- | test-suite/output/TypeclassDebug.out | 1 |
1 files changed, 0 insertions, 1 deletions
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. |