From db391451c5f89c034e6fec1b10fec66a25e3d4d4 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Mon, 4 Nov 2019 19:14:07 -0800
Subject: Replace "option" in doc when it refers to a flag

---
 doc/sphinx/practical-tools/coq-commands.rst | 4 ++--
 1 file changed, 2 insertions(+), 2 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 70259ff565..97e7af8cb4 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -36,7 +36,7 @@ toplevel with the command ``Coqloop.loop();;``.
 
 .. flag:: Coqtop Exit On Error
 
-   This option, off by default, causes coqtop to exit with status code
+   This flag, off by default, causes coqtop to exit with status code
    ``1`` if a command produces an error instead of recovering from it.
 
 Batch compilation (coqc)
@@ -219,7 +219,7 @@ and ``coqtop``, unless stated otherwise:
   .. warning:: This makes the logic inconsistent.
 :-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. Within Coq, the flag :flag:`Mangle Names` turns this behavior on,
+  etc. Within Coq, the :flag:`Mangle Names` flag 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
-- 
cgit v1.2.3