Separate index for vernacular options.

21 files changed, 102 insertions, 115 deletions

diff --git a/Makefile.doc b/Makefile.doc
index 33dd60dba..1f3509351 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -99,6 +99,8 @@ doc/refman/Reference-Manual.dvi: $(REFMANFILES) doc/refman/Reference-Manual.tex
 	$(SHOWMAKEINDEXERROR) Reference-Manual.ilg;\
 	$(MAKEINDEX) -q Reference-Manual.comidx -o Reference-Manual.comind;\
 	$(SHOWMAKEINDEXERROR) Reference-Manual.ilg;\
+	$(MAKEINDEX) -q Reference-Manual.optidx -o Reference-Manual.optind;\
+	$(SHOWMAKEINDEXERROR) Reference-Manual.ilg;\
 	$(MAKEINDEX) -q Reference-Manual.erridx -o Reference-Manual.errind;\
 	$(SHOWMAKEINDEXERROR) Reference-Manual.ilg;\
 	$(LATEX) -interaction=batchmode Reference-Manual > /dev/null;\
diff --git a/doc/common/styles/html/coqremote/cover.html b/doc/common/styles/html/coqremote/cover.html
index 7b8f82960..db8271709 100644
--- a/doc/common/styles/html/coqremote/cover.html
+++ b/doc/common/styles/html/coqremote/cover.html
@@ -88,6 +88,7 @@
   <ul class="menu">
   <li><a href="general-index.html">General</a></li>
   <li><a href="command-index.html">Commands</a></li>
+  <li><a href="option-index.html">Options</a></li>
   <li><a href="tactic-index.html">Tactics</a></li>
   <li><a href="error-index.html">Errors</a></li>
   </ul>
diff --git a/doc/common/styles/html/coqremote/styles.hva b/doc/common/styles/html/coqremote/styles.hva
index 94fb0d38b..a09dc4f85 100644
--- a/doc/common/styles/html/coqremote/styles.hva
+++ b/doc/common/styles/html/coqremote/styles.hva
@@ -53,6 +53,7 @@
             <ul class="menu">
               <li><a href="general-index.html">General</a></li>
               <li><a href="command-index.html">Commands</a></li>
+              <li><a href="option-index.html">Options</a></li>
               <li><a href="tactic-index.html">Tactics</a></li>
               <li><a href="error-index.html">Errors</a></li>
             </ul>
diff --git a/doc/common/styles/html/simple/cover.html b/doc/common/styles/html/simple/cover.html
index c2ac2c19d..1641a1ed3 100644
--- a/doc/common/styles/html/simple/cover.html
+++ b/doc/common/styles/html/simple/cover.html
@@ -58,6 +58,7 @@
   <li><a href="toc.html">Table of contents</a></li>
   <li><a href="general-index.html">General index</a></li>
   <li><a href="command-index.html">Commands index</a></li>
+  <li><a href="option-index.html">Options index</a></li>
   <li><a href="tactic-index.html">Tactics index</a></li>
   <li><a href="error-index.html">Errors index</a></li>
 </ul>
diff --git a/doc/common/styles/html/simple/styles.hva b/doc/common/styles/html/simple/styles.hva
index 71c4ffedf..20d0d4dd0 100644
--- a/doc/common/styles/html/simple/styles.hva
+++ b/doc/common/styles/html/simple/styles.hva
@@ -32,6 +32,7 @@
   <li><a href="toc.html">Table of contents</a></li>
   <li><a href="general-index.html">General index</a></li>
   <li><a href="command-index.html">Commands index</a></li>
+  <li><a href="option-index.html">Options index</a></li>
   <li><a href="tactic-index.html">Tactics index</a></li>
   <li><a href="error-index.html">Errors index</a></li>
 </ul>
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 35d64053c..96b486cdf 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -414,7 +414,7 @@ based on a variant of eauto. The flags semantics are:
 \end{itemize}
 
 \subsection{\tt Set Refine Instance Mode}
-\comindex{Set Refine Instance Mode}\comindex{Unset Refine Instance Mode}
+\optindex{Refine Instance Mode}
 
 The option {\tt Refine Instance Mode} allows to switch the behavior of instance
 declarations made through the {\tt Instance} command.
diff --git a/doc/refman/Coercion.tex b/doc/refman/Coercion.tex
index 60b4b2241..e4aa69353 100644
--- a/doc/refman/Coercion.tex
+++ b/doc/refman/Coercion.tex
@@ -305,8 +305,7 @@ Print the list of valid coercion paths from {\class$_1$} to {\class$_2$}.
 \asection{Activating the Printing of Coercions}
 
 \asubsection{\tt Set Printing Coercions.}
-\comindex{Set Printing Coercions}
-\comindex{Unset Printing Coercions}
+\optindex{Printing Coercions}
 
 This command forces all the coercions to be printed.
 Conversely, to skip the printing of coercions, use
@@ -314,8 +313,7 @@ Conversely, to skip the printing of coercions, use
 By default, coercions are not printed.
 
 \asubsection{\tt Set Printing Coercion {\qualid}.}
-\comindex{Set Printing Coercion}
-\comindex{Unset Printing Coercion}
+\optindex{Printing Coercion}
 
 This command forces coercion denoted by {\qualid} to be printed.
 To skip the printing of coercion {\qualid}, use
@@ -378,8 +376,7 @@ imported or not.
 To recover the behavior of the versions of Coq prior to 8.3, use the
 following command:
 
-\comindex{Set Automatic Coercions Import}
-\comindex{Unset Automatic Coercions Import}
+\optindex{Automatic Coercions Import}
 \begin{verbatim}
 Set Automatic Coercions Import.
 \end{verbatim}
diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index e9664f791..187fe5342 100644
--- a/doc/refman/Extraction.tex
+++ b/doc/refman/Extraction.tex
@@ -117,22 +117,20 @@ The type-preserving optimizations are controlled by the following \Coq\ options:
 
 \begin{description}
 
-\item \comindex{Set Extraction Optimize}
+\item \optindex{Extraction Optimize}
 {\tt Set Extraction Optimize.}
 
-\item \comindex{Unset Extraction Optimize}
-{\tt Unset Extraction Optimize.}
+\item {\tt Unset Extraction Optimize.}
 
 Default is Set. This controls all type-preserving optimizations made on
 the ML terms (mostly reduction of dummy beta/iota redexes, but also
 simplifications on Cases, etc). Put this option to Unset if you want a
 ML term as close as possible to the Coq term.
 
-\item \comindex{Set Extraction Conservative Types}
+\item \optindex{Extraction Conservative Types}
 {\tt Set Extraction Conservative Types.}
 
-\item \comindex{Unset Extraction Conservative Types}
-{\tt Unset Extraction Conservative Types.}
+\item {\tt Unset Extraction Conservative Types.}
 
 Default is Unset. This controls the non type-preserving optimizations
 made on ML terms (which try to avoid function abstraction of dummy
@@ -140,11 +138,10 @@ types). Turn this option to Set to make sure that {\tt e:t}
 implies that {\tt e':t'} where {\tt e'} and {\tt t'} are the extracted
 code of {\tt e} and {\tt t} respectively.
 
-\item \comindex{Set Extraction KeepSingleton}
+\item \optindex{Extraction KeepSingleton}
 {\tt Set Extraction KeepSingleton.}
 
-\item \comindex{Unset Extraction KeepSingleton}
-{\tt Unset Extraction KeepSingleton.}
+\item {\tt Unset Extraction KeepSingleton.}
 
 Default is Unset. Normally, when the extraction of an inductive type
 produces a singleton type (i.e. a type with only one constructor, and
@@ -153,11 +150,10 @@ removed and this type is seen as an alias to the inner type.
 The typical example is {\tt sig}. This option allows disabling this
 optimization when one wishes to preserve the inductive structure of types.
 
-\item \comindex{Set Extraction AutoInline}
+\item \optindex{Extraction AutoInline}
 {\tt Set Extraction AutoInline.} 
 
-\item \comindex{Unset Extraction AutoInline}
-{\tt Unset Extraction AutoInline.} 
+\item {\tt Unset Extraction AutoInline.} 
 
 Default is Set, so by default, the extraction mechanism is free to
 inline the bodies of some defined constants, according to some heuristics
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index 193c9d16a..e802398b5 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -253,14 +253,14 @@ tactic is replaced by the default one if not specified.
 \item {\tt Preterm [of \ident]}\comindex{Preterm} 
   Shows the term that will be fed to
   the kernel once the obligations are solved. Useful for debugging.
-\item {\tt Set Transparent Obligations}\comindex{Set Transparent Obligations}
+\item {\tt Set Transparent Obligations}\optindex{Transparent Obligations}
   Control whether all obligations should be declared as transparent (the
   default), or if the system should infer which obligations can be declared opaque. 
-\item {\tt Set Hide Obligations}\comindex{Set Hide Obligations}
+\item {\tt Set Hide Obligations}\optindex{Hide Obligations}
   Control whether obligations appearing in the term should be hidden
   as implicit arguments of the special constant
   \texttt{Program.Tactics.obligation}.
-\item {\tt Set Shrink Obligations}\comindex{Set Shrink Obligations}
+\item {\tt Set Shrink Obligations}\optindex{Shrink Obligations}
   Control whether obligations defined by tactics should have their
   context minimized to the set of variables used in the proof of the
   obligation, to avoid unnecessary dependencies.
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 11b4f2614..d1ce3bf41 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -470,9 +470,7 @@ The following commands give some control over the pretty-printing of
 
 \subsubsection{Printing nested patterns
 \label{SetPrintingMatching}
-\comindex{Set Printing Matching}
-\comindex{Unset Printing Matching}
-\comindex{Test Printing Matching}}
+\optindex{Printing Matching}}
 
 The Calculus of Inductive Constructions knows pattern-matching only
 over simple patterns. It is however convenient to re-factorize nested
@@ -498,9 +496,7 @@ This tells if the printing matching mode is on or off. The default is
 on.
 
 \subsubsection{Printing of wildcard pattern
-\comindex{Set Printing Wildcard}
-\comindex{Unset Printing Wildcard}
-\comindex{Test Printing Wildcard}}
+\optindex{Printing Wildcard}}
 
 Some variables in a pattern may not occur in the right-hand side of
 the pattern-matching clause.  There are options to control the
@@ -527,9 +523,7 @@ This tells if the wildcard printing mode is on or off. The default is
 to print wildcard for useless variables.
 
 \subsubsection{Printing of the elimination predicate
-\comindex{Set Printing Synth}
-\comindex{Unset Printing Synth}
-\comindex{Test Printing Synth}}
+\optindex{Printing Synth}}
 
 In most of the cases, the type of the result of a matched term is
 mechanically synthesizable. Especially, if the result type does not
@@ -1451,8 +1445,7 @@ Check (p r1 r2).
 
 \subsection{Mode for automatic declaration of implicit arguments
 \label{Auto-implicit}
-\comindex{Set Implicit Arguments}
-\comindex{Unset Implicit Arguments}}
+\optindex{Implicit Arguments}}
 
 In case one wants to systematically declare implicit the arguments
 detectable as such, one may switch to the automatic declaration of
@@ -1466,8 +1459,7 @@ arguments is governed by options controlling whether strict and
 contextual implicit arguments have to be considered or not.
 
 \subsection{Controlling strict implicit arguments
-\comindex{Set Strict Implicit}
-\comindex{Unset Strict Implicit}
+\optindex{Strict Implicit}
 \label{SetStrictImplicit}}
 
 When the mode for automatic declaration of implicit arguments is on,
@@ -1482,8 +1474,7 @@ Conversely, use the command {\tt Set Strict Implicit} to
 restore the original mode that declares implicit only the strict implicit arguments plus a small subset of the non strict implicit arguments.
 
 In the other way round, to capture exactly the strict implicit arguments and no more than the strict implicit arguments, use the command:
-\comindex{Set Strongly Strict Implicit}
-\comindex{Unset Strongly Strict Implicit}
+\optindex{Strongly Strict Implicit}
 \begin{quote}
 \tt Set Strongly Strict Implicit.
 \end{quote}
@@ -1494,8 +1485,7 @@ let the option ``{\tt Strict Implicit}'' decide what to do.
 declare the strict implicit arguments as implicit.
 
 \subsection{Controlling contextual implicit arguments
-\comindex{Set Contextual Implicit}
-\comindex{Unset Contextual Implicit}
+\optindex{Contextual Implicit}
 \label{SetContextualImplicit}}
 
 By default, {\Coq} does not automatically set implicit the contextual
@@ -1508,8 +1498,7 @@ Conversely, use command {\tt Unset Contextual Implicit} to
 unset the contextual implicit mode.
 
 \subsection{Controlling reversible-pattern implicit arguments
-\comindex{Set Reversible Pattern Implicit}
-\comindex{Unset Reversible Pattern Implicit}
+\optindex{Reversible Pattern Implicit}
 \label{SetReversiblePatternImplicit}}
 
 By default, {\Coq} does not automatically set implicit the reversible-pattern
@@ -1522,8 +1511,7 @@ Conversely, use command {\tt Unset Reversible Pattern Implicit} to
 unset the reversible-pattern implicit mode.
 
 \subsection{Controlling the insertion of implicit arguments not followed by explicit arguments
-\comindex{Set Maximal Implicit Insertion}
-\comindex{Unset Maximal Implicit Insertion}
+\optindex{Maximal Implicit Insertion}
 \label{SetMaximalImplicitInsertion}}
 
 Implicit arguments can be declared to be automatically inserted when a
@@ -1607,10 +1595,8 @@ if each of them is to be used maximally or not, use the command
 \end{quote}
 
 \subsection{Explicit displaying of implicit arguments for pretty-printing
-\comindex{Set Printing Implicit}
-\comindex{Unset Printing Implicit}
-\comindex{Set Printing Implicit Defensive}
-\comindex{Unset Printing Implicit Defensive}}
+\optindex{Printing Implicit}
+\optindex{Printing Implicit Defensive}}
 
 By default the basic pretty-printing rules hide the inferable implicit
 arguments of an application. To force printing all implicit arguments,
@@ -1653,8 +1639,7 @@ Check Prop = nat.
 \end{coq_example*}
 
 \subsection{Deactivation of implicit arguments for parsing}
-\comindex{Set Parsing Explicit}
-\comindex{Unset Parsing Explicit}
+\optindex{Parsing Explicit}
 
 Use of implicit arguments can be deactivated by issuing the command:
 \begin{quote}
@@ -1874,8 +1859,7 @@ More details and examples, and a description of the commands related
 to coercions are provided in Chapter~\ref{Coercions-full}.
 
 \section[Printing constructions in full]{Printing constructions in full\label{SetPrintingAll}
-\comindex{Set Printing All}
-\comindex{Unset Printing All}}
+\optindex{Printing All}}
 
 Coercions, implicit arguments, the type of pattern-matching, but also
 notations (see Chapter~\ref{Addoc-syntax}) can obfuscate the behavior
@@ -1897,8 +1881,7 @@ printing features, use the command
 \end{quote}
 
 \section[Printing universes]{Printing universes\label{PrintingUniverses}
-\comindex{Set Printing Universes}
-\comindex{Unset Printing Universes}}
+\optindex{Printing Universes}}
 
 The following command:
 \begin{quote}
@@ -1991,8 +1974,7 @@ Unset Printing Existential Instances.
 
 \subsection{Explicit displaying of existential instances for pretty-printing
 \label{SetPrintingExistentialInstances}
-\comindex{Set Printing Existential Instances}
-\comindex{Unset Printing Existential Instances}}
+\optindex{Printing Existential Instances}}
 
 The command:
 \begin{quote}
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 1704b4d60..eea53886b 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -779,8 +779,7 @@ f (3+4).
 \end{coq_example}
 
 \item \index{appcontext@\texttt{appcontext}!in pattern}
-  \comindex{Set Tactic Compat Context}
-  \comindex{Unset Tactic Compat Context}
+  \optindex{Tactic Compat Context}
 For historical reasons, {\tt context} used to consider $n$-ary applications
 such as {\tt (f 1 2)} as a whole, and not as a sequence of unary
 applications {\tt ((f 1) 2)}. Hence {\tt context [f ?x]} would fail
@@ -1094,9 +1093,7 @@ Defined {\ltac} functions can be displayed using the command
 
 \section{Debugging {\ltac} tactics}
 
-\subsection[Info trace]{Info trace\comindex{Info}\comindex{Set Info Level}
-\comindex{Unset Info Level}
-\comindex{Test Info Level}}
+\subsection[Info trace]{Info trace\comindex{Info}\optindex{Info Level}}
 
 It is possible to print the trace of the path eventually taken by an {\ltac} script. That is, the list of executed tactics, discarding all the branches which have failed. To that end the {\tt Info} command can be used with the following syntax.
 
@@ -1142,9 +1139,7 @@ This will automatically print the same trace as {\tt Info \num} at each tactic c
 
 The current value for the {\tt Info Level} option can be checked using the {\tt Test Info Level} command.
 
-\subsection[Interactive debugger]{Interactive debugger\comindex{Set Ltac Debug}
-\comindex{Unset Ltac Debug}
-\comindex{Test Ltac Debug}}
+\subsection[Interactive debugger]{Interactive debugger\optindex{Ltac Debug}}
 
 The {\ltac} interpreter comes with a step-by-step debugger. The
 debugger can be activated using the command
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index d1a1359d6..4547c7fd8 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -493,31 +493,28 @@ Locate I.Dont.Exist.
 \subsection{The {\sc Whelp} searching tool
 \label{Whelp}}
 
-{\sc Whelp} is an experimental searching and browsing tool for the
-whole {\Coq} library and the whole set of {\Coq} user contributions.
-{\sc Whelp} requires a browser to work. {\sc Whelp} has been developed
-at the University of Bologna as part of the HELM\footnote{Hypertextual
-Electronic Library of Mathematics} and MoWGLI\footnote{Mathematics on
-the Web, Get it by Logics and Interfaces} projects.  It can be invoked
-directly from the {\Coq} toplevel or from {\CoqIDE}, assuming a
-graphical environment is also running. The browser to use can be
-selected by setting the environment variable {\tt
-COQREMOTEBROWSER}. If not explicitly set, it defaults to
+{\sc Whelp} is an experimental searching and browsing tool for the whole {\Coq}
+library and the whole set of {\Coq} user contributions.  {\sc Whelp} requires a
+browser to work. {\sc Whelp} has been developed at the University of Bologna as
+part of the HELM\footnote{Hypertextual Electronic Library of Mathematics} and
+MoWGLI\footnote{Mathematics on the Web, Get it by Logics and Interfaces}
+projects.  It can be invoked directly from the {\Coq} toplevel or from
+{\CoqIDE}, assuming a graphical environment is also running. The browser to use
+can be selected by setting the environment variable {\tt COQREMOTEBROWSER}. If
+not explicitly set, it defaults to
 \verb!firefox -remote \"OpenURL(%s,new-tab)\" || firefox %s &"!  or
-\verb!C:\\PROGRA~1\\INTERN~1\\IEXPLORE %s!, depending on the
-underlying operating system (in the command, the string \verb!%s!
-serves as metavariable for the url to open).
-The Whelp tool relies on a dedicated Whelp server and on another server
-called Getter that retrieves formal documents. The default Whelp server name
-can be obtained using the command {\tt Test Whelp Server}
-\comindex{Test Whelp Server} and the default Getter can be obtained
-using the command: {\tt Test Whelp Getter} \comindex{Test Whelp
-Getter}. The Whelp server name can be changed using the command:
+\verb!C:\\PROGRA~1\\INTERN~1\\IEXPLORE %s!, depending on the underlying
+operating system (in the command, the string \verb!%s!  serves as metavariable
+for the url to open).  The Whelp tool relies on a dedicated Whelp server and on
+another server called Getter that retrieves formal documents. The default Whelp
+server name can be obtained using the command {\tt Test Whelp Server} and the
+default Getter can be obtained using the command: {\tt Test Whelp Getter}. The
+Whelp server name can be changed using the command:
 
 \smallskip
 \noindent {\tt Set Whelp Server {\str}}.\\
 where {\str} is a URL (e.g. {\tt http://mowgli.cs.unibo.it:58080}).
-\comindex{Set Whelp Server}
+\optindex{Whelp Server}
 \smallskip
 
 \noindent The Getter can be changed using the command:
@@ -525,7 +522,7 @@ where {\str} is a URL (e.g. {\tt http://mowgli.cs.unibo.it:58080}).
 
 \noindent {\tt Set Whelp Getter {\str}}.\\
 where {\str} is a URL (e.g. {\tt http://mowgli.cs.unibo.it:58081}).  
-\comindex{Set Whelp Getter}
+\optindex{Whelp Getter}
 
 \bigskip
 
@@ -960,53 +957,53 @@ the command has not terminated after the time specified by the integer
 is displayed.
 
 \subsection[\tt Set Default Timeout \textrm{\textsl{int}}.]{\tt Set
-  Default Timeout \textrm{\textsl{int}}.\comindex{Set Default Timeout}}
+  Default Timeout \textrm{\textsl{int}}.\optindex{Default Timeout}}
 
 After using this command, all subsequent commands behave as if they
 were passed to a {\tt Timeout} command. Commands already starting by
 a {\tt Timeout} are unaffected.
 
-\subsection[\tt Unset Default Timeout.]{\tt Unset Default Timeout.\comindex{Unset Default Timeout}}
+\subsection[\tt Unset Default Timeout.]{\tt Unset Default Timeout.\optindex{Default Timeout}}
 
 This command turns off the use of a default timeout.
 
-\subsection[\tt Test Default Timeout.]{\tt Test Default Timeout.\comindex{Test Default Timeout}}
+\subsection[\tt Test Default Timeout.]{\tt Test Default Timeout.\optindex{Default Timeout}}
 
 This command displays whether some default timeout has be set or not.
 
 \section{Controlling display}
 
-\subsection[\tt Set Silent.]{\tt Set Silent.\comindex{Set Silent}
+\subsection[\tt Set Silent.]{\tt Set Silent.\optindex{Silent}
 \label{Begin-Silent}
 \index{Silent mode}}
 This command turns off the normal displaying.
 
-\subsection[\tt Unset Silent.]{\tt Unset Silent.\comindex{Unset Silent}}
+\subsection[\tt Unset Silent.]{\tt Unset Silent.\optindex{Silent}}
 This command turns the normal display on.
 
-\subsection[\tt Set Printing Width {\integer}.]{\tt Set Printing Width {\integer}.\comindex{Set Printing Width}}
+\subsection[\tt Set Printing Width {\integer}.]{\tt Set Printing Width {\integer}.\optindex{Printing Width}}
 \label{SetPrintingWidth}
 This command sets which left-aligned part of the width of the screen
 is used for display. 
 
-\subsection[\tt Unset Printing Width.]{\tt Unset Printing Width.\comindex{Unset Printing Width}}
+\subsection[\tt Unset Printing Width.]{\tt Unset Printing Width.\optindex{Printing Width}}
 This command resets the width of the screen used for display to its
 default value (which is 78 at the time of writing this documentation).
 
-\subsection[\tt Test Printing Width.]{\tt Test Printing Width.\comindex{Test Printing Width}}
+\subsection[\tt Test Printing Width.]{\tt Test Printing Width.\optindex{Printing Width}}
 This command displays the current screen width used for display.
 
-\subsection[\tt Set Printing Depth {\integer}.]{\tt Set Printing Depth {\integer}.\comindex{Set Printing Depth}}
+\subsection[\tt Set Printing Depth {\integer}.]{\tt Set Printing Depth {\integer}.\optindex{Printing Depth}}
 This command sets the nesting depth of the formatter used for
 pretty-printing. Beyond this depth, display of subterms is replaced by
 dots. 
 
-\subsection[\tt Unset Printing Depth.]{\tt Unset Printing Depth.\comindex{Unset Printing Depth}}
+\subsection[\tt Unset Printing Depth.]{\tt Unset Printing Depth.\optindex{Printing Depth}}
 This command resets the nesting depth of the formatter used for
 pretty-printing to its default value (at the
 time of writing this documentation, the default value is 50).
 
-\subsection[\tt Test Printing Depth.]{\tt Test Printing Depth.\comindex{Test Printing Depth}}
+\subsection[\tt Test Printing Depth.]{\tt Test Printing Depth.\optindex{Printing Depth}}
 This command displays the current nesting depth used for display.
 
 %\subsection{\tt Abstraction ...}
@@ -1147,17 +1144,17 @@ perform a {\tt Ltac \ident\ := {\rm\sl convtactic}}.
 
 \subsection{\tt Set Virtual Machine
 \label{SetVirtualMachine}
-\comindex{Set Virtual Machine}}
+\optindex{Virtual Machine}}
 
 This activates the bytecode-based conversion algorithm.
 
 \subsection{\tt Unset Virtual Machine
-\comindex{Unset Virtual Machine}}
+\optindex{Virtual Machine}}
 
 This deactivates the bytecode-based conversion algorithm.
 
 \subsection{\tt Test Virtual Machine
-\comindex{Test Virtual Machine}}
+\optindex{Virtual Machine}}
 
 This tells if the bytecode-based conversion algorithm is
 activated. The default behavior is to have the bytecode-based
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 9055254bb..684a4add4 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -476,18 +476,18 @@ of the proof without having to wait the completion of the proof."
 
 \section{Controlling the effect of proof editing commands}
 
-\subsection[\tt Set Hyps Limit {\num}.]{\tt Set Hyps Limit {\num}.\comindex{Set Hyps Limit}}
+\subsection[\tt Set Hyps Limit {\num}.]{\tt Set Hyps Limit {\num}.\optindex{Hyps Limit}}
 This command sets the maximum number of hypotheses displayed in
 goals after the application of a tactic. 
 All the hypotheses remains usable in the proof development.
 
 
-\subsection[\tt Unset Hyps Limit.]{\tt Unset Hyps Limit.\comindex{Unset Hyps Limit}}
+\subsection[\tt Unset Hyps Limit.]{\tt Unset Hyps Limit.\optindex{Hyps Limit}}
 This command goes back to the default mode which is to print all
 available hypotheses.
 
 
-\subsection[\tt Set Automatic Introduction.]{\tt Set Automatic Introduction.\comindex{Set Automatic Introduction}\comindex{Unset Automatic Introduction}\label{Set Automatic Introduction}}
+\subsection[\tt Set Automatic Introduction.]{\tt Set Automatic Introduction.\optindex{Automatic Introduction}\label{Set Automatic Introduction}}
 
 The option {\tt Automatic Introduction} controls the way binders are
 handled in assertion commands such as {\tt Theorem {\ident}
diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex
index 7d00a4005..571e16d57 100644
--- a/doc/refman/RefMan-sch.tex
+++ b/doc/refman/RefMan-sch.tex
@@ -123,12 +123,9 @@ The type of {\tt even\_odd} shares the same premises but the
 conclusion is {\tt (n:nat)(even n)->(Q n)}.
 
 \subsection{Automatic declaration of schemes
-\comindex{Set Boolean Equality Schemes}
-\comindex{Unset Boolean Equality Schemes}
-\comindex{Set Elimination Schemes}
-\comindex{Unset Elimination Schemes}
-\comindex{Set Nonrecursive Elimination Schemes}
-\comindex{Unset Nonrecursive Elimination Schemes}
+\optindex{Boolean Equality Schemes}
+\optindex{Elimination Schemes}
+\optindex{Nonrecursive Elimination Schemes}
 \label{set-nonrecursive-elimination-schemes}
 }
 
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 24417bd03..15ddf6261 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -405,8 +405,7 @@ where "n + m" := (plus n m).
 \end{coq_example*}
 
 \subsection{Displaying informations about notations
-\comindex{Set Printing Notations}
-\comindex{Unset Printing Notations}}
+\optindex{Printing Notations}}
 
 To deactivate the printing of all notations, use the command
 \begin{quote}
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index a5d053a06..c3d8ad531 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -55,7 +55,7 @@ selector (see Section \ref{default-selector}) is used.
 \end{tabular}
 \subsection[\tt Set Default Goal Selector ``\selector''.]
            {\tt Set Default Goal Selector ``\selector''.
-            \comindex{Set Default Goal Selector}
+            \optindex{Default Goal Selector}
             \label{default-selector}}
 After using this command, the default selector -- used when no selector
 is specified when applying a tactic -- is set to the chosen value. The
@@ -66,8 +66,7 @@ simultaneously. Then, to apply a tactic {\tt tac} to the first goal
 only, you can write {\tt 1:tac}.
 
 \subsection[\tt Test Default Goal Selector.]
-           {\tt Test Default Goal Selector.
-            \comindex{Test Default Goal Selector}}
+           {\tt Test Default Goal Selector.}
 This command displays the current default selector.
 
 \subsection{Bindings list
@@ -4143,7 +4142,7 @@ instead may reason about any first-order class inductive definition.
 \end{Variants}
 
 Proof-search is bounded by a depth parameter which can be set by typing the
-{\nobreak \tt Set Firstorder Depth $n$} \comindex{Set Firstorder Depth}
+{\nobreak \tt Set Firstorder Depth $n$} \optindex{Firstorder Depth}
 vernacular command.
 
 
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index 91d30c073..01ad0f70f 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -143,6 +143,9 @@ Options A and B of the licence are {\em not} elected.}
 \printindex[command]
 \cutname{command-index.html}
 
+\printindex[option]
+\cutname{option-index.html}
+
 \printindex[error]
 \cutname{error-index.html}
 
diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index 65218ba0d..341431114 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -106,7 +106,7 @@ in a universe strictly higher than \texttt{Set}.
 \asection{\tt Polymorphic, Monomorphic}
 \comindex{Polymorphic}
 \comindex{Monomorphic}
-\comindex{Set Universe Polymorphism}
+\optindex{Universe Polymorphism}
 
 As shown in the examples, polymorphic definitions and inductives can be
 declared using the \texttt{Polymorphic} prefix. There also exists an
diff --git a/doc/refman/headers.hva b/doc/refman/headers.hva
index f65e1c10c..df4aec272 100644
--- a/doc/refman/headers.hva
+++ b/doc/refman/headers.hva
@@ -15,6 +15,10 @@
 \protect\addcontentsline{toc}{chapter}{Vernacular Commands Index}%
 Vernacular Commands Index}
 
+\newindex{option}{optidx}{optind}{%
+\protect\addcontentsline{toc}{chapter}{Vernacular Options Index}%
+Vernacular Options Index}
+
 \newindex{error}{erridx}{errind}{%
 \protect\addcontentsline{toc}{chapter}{Index of Error Messages}Index of Error Messages}
 
@@ -26,6 +30,8 @@ Global Index}
 \index{#1@\texttt{#1}}\index[tactic]{#1@\texttt{#1}}}
 \newcommand{\comindex}[1]{%
 \index{#1@\texttt{#1}}\index[command]{#1@\texttt{#1}}}
+\newcommand{\optindex}[1]{%
+\index{#1@\texttt{#1}}\index[option]{#1@\texttt{#1}}}
 \newcommand{\errindex}[1]{\texttt{#1}\index[error]{#1}}
 \newcommand{\errindexbis}[2]{\texttt{#1}\index[error]{#2}}
 \newcommand{\ttindex}[1]{\index{#1@\texttt{#1}}}
diff --git a/doc/refman/headers.sty b/doc/refman/headers.sty
index bc5f5c6c3..ef28588e3 100644
--- a/doc/refman/headers.sty
+++ b/doc/refman/headers.sty
@@ -39,6 +39,11 @@
 \protect\addcontentsline{toc}{chapter}{Vernacular Commands Index}%
 Vernacular Commands Index}
 
+\newindex{option}{optidx}{optind}{%
+\protect\setheaders{Vernacular Options Index}%
+\protect\addcontentsline{toc}{chapter}{Vernacular Options Index}%
+Vernacular Options Index}
+
 \newindex{error}{erridx}{errind}{%
 \protect\setheaders{Index of Error Messages}%
 \protect\addcontentsline{toc}{chapter}{Index of Error Messages}Index of Error Messages}
@@ -51,6 +56,8 @@ Vernacular Commands Index}
 \index{#1@\texttt{#1}}\index[tactic]{#1@\texttt{#1}}}
 \newcommand{\comindex}[1]{%
 \index{#1@\texttt{#1}}\index[command]{#1@\texttt{#1}}}
+\newcommand{\optindex}[1]{%
+\index{#1@\texttt{#1}}\index[option]{#1@\texttt{#1}}}
 \newcommand{\errindex}[1]{\texttt{#1}\index[error]{#1}}
 \newcommand{\errindexbis}[2]{\texttt{#1}\index[error]{#2}}
 \newcommand{\ttindex}[1]{\index{#1@\texttt{#1}}}
diff --git a/doc/refman/menu.html b/doc/refman/menu.html
index db19678f3..7312ad344 100644
--- a/doc/refman/menu.html
+++ b/doc/refman/menu.html
@@ -19,6 +19,9 @@ Tactics Index
 <TD><CENTER><A HREF="command-index.html" TARGET="UP"><FONT SIZE=2>
 Vernacular Commands Index
 </FONT></A></CENTER></TD>
+<TD><CENTER><A HREF="option-index.html" TARGET="UP"><FONT SIZE=2>
+Vernacular Options Index
+</FONT></A></CENTER></TD>
 <TD><CENTER><A HREF="error-index.html" TARGET="UP"><FONT SIZE=2>
 Index of Error Messages
 </FONT></A></CENTER></TD>
@@ -26,4 +29,4 @@ Index of Error Messages
 
 </CENTER>
 
-</BODY></HTML>
\ No newline at end of file
+</BODY></HTML>