From d6bd80ff477f3416f4ff0ded65aa658999b5ac21 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 24 Nov 2017 22:27:53 +0100
Subject: Document some omega options (missing Omega Oldstyle).

---
 doc/refman/Omega.tex | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)

diff --git a/doc/refman/Omega.tex b/doc/refman/Omega.tex
index 8025fbe29f..82765da6ed 100644
--- a/doc/refman/Omega.tex
+++ b/doc/refman/Omega.tex
@@ -149,6 +149,32 @@ intro; omega.
 
 % Other examples can be found in \verb+$COQLIB/theories/DEMOS/OMEGA+.
 
+\section{Options}
+
+\begin{quote}
+  \optindex{Stable Omega}
+  {\tt Unset Stable Omega}
+\end{quote}
+This deprecated option (on by default) is for compatibility with Coq
+pre 8.5. It resets internal name counters to make executions of
+{\tt omega} independent.
+
+\begin{quote}
+  \optindex{Omega UseLocalDefs}
+  {\tt Unset Omega UseLocalDefs}
+\end{quote}
+This option (on by default) allows {\tt omega} to use the bodies of
+local variables.
+
+\begin{quote}
+  \optindex{Omega System}
+  {\tt Set Omega System}
+  \optindex{Omega Action}
+  {\tt Set Omega Action}
+\end{quote}
+These two options (off by default) activate the printing of debug
+information.
+
 \asection{Technical data}
 \label{technical}
 
-- 
cgit v1.2.3