From a101fdc131bd5d7a8ed1470cd7fa705ad6979e92 Mon Sep 17 00:00:00 2001
From: Clément Pit-Claudel
Date: Fri, 10 May 2019 09:47:02 -0400
Subject: [refman] Use 'flag' instead of 'opt' for 'Ltac2 Debug'

---
 doc/sphinx/proof-engine/ltac2.rst | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index 6e33862b39..945ffd6307 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -823,9 +823,9 @@ Ltac2 features a toplevel loop that can be used to evaluate expressions.
 Debug
 -----
 
-.. opt:: Ltac2 Backtrace
+.. flag:: Ltac2 Backtrace
 
-   When this option is set, toplevel failures will be printed with a backtrace.
+   When this flag is set, toplevel failures will be printed with a backtrace.
 
 Compatibility layer with Ltac1
 ------------------------------
-- 
cgit v1.2.3