From ec7dd674ea25dfd36c007bb863fed63ce8d31ff2 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sat, 1 Sep 2018 12:39:09 -0700
Subject: Rewrite "Flags, Options and Tables" section. Mark boolean-valued
 options with :flag: Adjust tactic and command names so parameters aren't
 shown in the index unless they're needed for disambiguation. Remove
 references to synchronous options. Revise doc for tables. Correct indentation
 for text below :flag:

---
 doc/sphinx/addendum/omega.rst | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'doc/sphinx/addendum/omega.rst')

diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst
index f7a431ef29..828505b850 100644
--- a/doc/sphinx/addendum/omega.rst
+++ b/doc/sphinx/addendum/omega.rst
@@ -116,23 +116,23 @@ loaded by
 Options
 -------
 
-.. opt:: Stable Omega
+.. flag:: Stable Omega
 
    .. deprecated:: 8.5
 
    This deprecated option (on by default) is for compatibility with Coq pre 8.5. It
    resets internal name counters to make executions of :tacn:`omega` independent.
 
-.. opt:: Omega UseLocalDefs
+.. flag:: Omega UseLocalDefs
 
    This option (on by default) allows :tacn:`omega` to use the bodies of local
    variables.
 
-.. opt:: Omega System
+.. flag:: Omega System
 
    This option (off by default) activate the printing of debug information
 
-.. opt:: Omega Action
+.. flag:: Omega Action
 
    This option (off by default) activate the printing of debug information
 
-- 
cgit v1.2.3