From b1e0fa29b62ee958b31c55ea3c8eea4087e6e2b4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 5 Dec 2018 17:20:54 +0100
Subject: Documenting the Ltac Backtrace flag.

---
 doc/sphinx/proof-engine/ltac.rst | 9 +++++++++
 1 file changed, 9 insertions(+)

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