diff options
| author | Pierre-Marie Pédrot | 2018-12-05 17:20:54 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-05 12:09:44 +0100 |
| commit | b1e0fa29b62ee958b31c55ea3c8eea4087e6e2b4 (patch) | |
| tree | c5ef8ee2b21825e782650607628b661df004fad1 | |
| parent | 151ec20b1202df17b75a7c8d3fe9f8ff258a88bd (diff) | |
Documenting the Ltac Backtrace flag.
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 442077616f..830b24159e 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -1154,6 +1154,15 @@ Printing |Ltac| tactics Debugging |Ltac| tactics ------------------------ +Backtraces +~~~~~~~~~~ + +.. flag:: Ltac Backtrace + + Setting this flag displays a backtrace on Ltac failures that can be useful + to find out what went wrong. It is disabled by default for performance + reasons. + Info trace ~~~~~~~~~~ |