From 08b399f55a8bc01affa54273e6792392ea9eb926 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sun, 29 Dec 2019 13:55:13 -0800
Subject: Remove :flag: that appears in the output

---
 doc/sphinx/language/gallina-specification-language.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 967b0461d0..f82282911f 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -1478,7 +1478,7 @@ Chapter :ref:`Tactics`. The basic assertion command is:
       The name you provided is already defined. You have then to choose
       another name.
 
-   .. exn:: Nested proofs are not allowed unless you turn the :flag:`Nested Proofs Allowed` flag on.
+   .. exn:: Nested proofs are not allowed unless you turn the Nested Proofs Allowed flag on.
 
       You are asserting a new statement while already being in proof editing mode.
       This feature, called nested proofs, is disabled by default.
-- 
cgit v1.2.3