diff options
| author | Hugo Herbelin | 2019-02-18 19:02:23 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-02-18 19:02:23 +0100 |
| commit | ee6d8274483711f84277e449494c3a11a64dfea8 (patch) | |
| tree | fad80601c725129060f5da8d88c79c82814dc454 /doc | |
| parent | 1dbb4e77051324e229f7006161746030e5369565 (diff) | |
| parent | b1e0fa29b62ee958b31c55ea3c8eea4087e6e2b4 (diff) | |
Merge PR #9142: Disable Ltac backtraces
Ack-by: Zimmi48
Reviewed-by: jfehrle
Ack-by: ppedrot
Diffstat (limited to 'doc')
| -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 4f486a777d..c134563efe 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -1162,6 +1162,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 ~~~~~~~~~~ |