From 40c483a95f354e457e10d00951fd6a8eec08176d Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Mon, 5 Nov 2018 13:32:36 -0800
Subject: Document undocumented flags and options Also remove a few
 undocumented settings

---
 doc/sphinx/practical-tools/coq-commands.rst | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'doc/sphinx/practical-tools')

diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index de9e327740..9bc67147f7 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -198,10 +198,10 @@ and ``coqtop``, unless stated otherwise:
 :-type-in-type: Collapse the universe hierarchy of |Coq|.
 
   .. warning:: This makes the logic inconsistent.
-:-mangle-names *ident*: Experimental: Do not depend on this option. Replace
+:-mangle-names *ident*: *Experimental.* Do not depend on this option. Replace
   Coq's auto-generated name scheme with names of the form *ident0*, *ident1*,
-  etc. The command ``Set Mangle Names`` turns the behavior on in a document,
-  and ``Set Mangle Names Prefix "ident"`` changes the used prefix. This feature
+  etc. Within Coq, the flag :flag:`Mangle Names` turns this behavior on,
+  and the :opt:`Mangle Names Prefix` option sets the prefix to use. This feature
   is intended to be used as a linter for developments that want to be robust to
   changes in the auto-generated name scheme. The options are provided to
   facilitate tracking down problems.
-- 
cgit v1.2.3