Document undocumented flags and options

Also remove a few undocumented settings

8 files changed, 141 insertions, 45 deletions

diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index b7d05fd6ef..8891234330 100644
--- a/doc/sphinx/addendum/extraction.rst
+++ b/doc/sphinx/addendum/extraction.rst
@@ -164,7 +164,7 @@ The type-preserving optimizations are controlled by the following |Coq| options:
 .. cmd:: Extraction Inline {+ @qualid }
 
    In addition to the automatic inline feature, the constants
-   mentionned by this command will always be inlined during extraction.
+   mentioned by this command will always be inlined during extraction.
 
 .. cmd:: Extraction NoInline {+ @qualid }
 
@@ -410,6 +410,52 @@ It is possible to instruct the extraction not to use particular filenames.
 For |OCaml|, a typical use of these commands is
 ``Extraction Blacklist String List``.
 
+Additional settings
+~~~~~~~~~~~~~~~~~~~
+
+.. opt:: Extraction File Comment @string
+   :name: Extraction File Comment
+
+   Provides a comment that is included at the beginning of the output files.
+
+.. opt:: Extraction Flag @num
+   :name: Extraction Flag
+
+   Controls which optimizations are used during extraction, providing a finer-grained
+   control than :flag:`Extraction Optimize`.  The bits of *num* are used as a bit mask.
+   Keeping an option off keeps the extracted ML more similar to the Coq term.
+   Values are:
+
+   +-----+-------+----------------------------------------------------------------+
+   | Bit | Value | Optimization (default is on unless noted otherwise)            |
+   +-----+-------+----------------------------------------------------------------+
+   |   0 |    1  | Remove local dummy variables                                   |
+   +-----+-------+----------------------------------------------------------------+
+   |   1 |    2  | Use special treatment for fixpoints                            |
+   +-----+-------+----------------------------------------------------------------+
+   |   2 |    4  | Simplify case with iota-redux                                  |
+   +-----+-------+----------------------------------------------------------------+
+   |   3 |    8  | Factor case branches as functions                              |
+   +-----+-------+----------------------------------------------------------------+
+   |   4 |   16  | (not available, default false)                                 |
+   +-----+-------+----------------------------------------------------------------+
+   |   5 |   32  | Simplify case as function of one argument                      |
+   +-----+-------+----------------------------------------------------------------+
+   |   6 |   64  | Simplify case by swapping case and lambda                      |
+   +-----+-------+----------------------------------------------------------------+
+   |   7 |  128  | Some case optimization                                         |
+   +-----+-------+----------------------------------------------------------------+
+   |   8 |  256  | Push arguments inside a letin                                  |
+   +-----+-------+----------------------------------------------------------------+
+   |   9 |  512  | Use linear let reduction (default false)                       |
+   +-----+-------+----------------------------------------------------------------+
+   |  10 | 1024  | Use linear beta reduction (default false)                      |
+   +-----+-------+----------------------------------------------------------------+
+
+.. flag:: Extraction TypeExpand
+
+   If set, fully expand Coq types in ML.  **see type_expand in mlutil.ml**
+
 Differences between |Coq| and ML type systems
 ----------------------------------------------
 
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 98dfcb2373..7933cdaee0 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -461,12 +461,12 @@ type, like:
 This is equivalent to ``Hint Transparent, Opaque ident : typeclass_instances``.
 
 
-Options
-~~~~~~~
+Settings
+~~~~~~~~
 
 .. flag:: Typeclasses Dependency Order
 
-   This option (on by default since 8.6) respects the dependency order
+   This flag (on by default since 8.6) respects the dependency order
    between subgoals, meaning that subgoals on which other subgoals depend
    come first, while the non-dependent subgoals were put before
    the dependent ones previously (Coq 8.5 and below). This can result in
@@ -475,7 +475,7 @@ Options
 
 .. flag:: Typeclasses Filtered Unification
 
-   This option, available since Coq 8.6 and off by default, switches the
+   This flag, available since Coq 8.6 and off by default, switches the
    hint application procedure to a filter-then-unify strategy. To apply a
    hint, we first check that the goal *matches* syntactically the
    inferred or specified pattern of the hint, and only then try to
@@ -483,13 +483,13 @@ Options
    improve performance by calling unification less often, matching
    syntactic patterns being very quick. This also provides more control
    on the triggering of instances. For example, forcing a constant to
-   explicitely appear in the pattern will make it never apply on a goal
+   explicitly appear in the pattern will make it never apply on a goal
    where there is a hole in that place.
 
 
 .. flag:: Typeclasses Limit Intros
 
-   This option (on by default) controls the ability to apply hints while
+   This flag (on by default) controls the ability to apply hints while
    avoiding (functional) eta-expansions in the generated proof term. It
    does so by allowing hints that conclude in a product to apply to a
    goal with a matching product directly, avoiding an introduction.
@@ -503,16 +503,16 @@ Options
 
 .. flag:: Typeclass Resolution For Conversion
 
-   This option (on by default) controls the use of typeclass resolution
+   This flag (on by default) controls the use of typeclass resolution
    when a unification problem cannot be solved during elaboration/type
-   inference. With this option on, when a unification fails, typeclass
+   inference. With this flag on, when a unification fails, typeclass
    resolution is tried before launching unification once again.
 
 
 .. flag:: Typeclasses Strict Resolution
 
-   Typeclass declarations introduced when this option is set have a
-   stricter resolution behavior (the option is off by default). When
+   Typeclass declarations introduced when this flag is set have a
+   stricter resolution behavior (the flag is off by default). When
    looking for unifications of a goal with an instance of this class, we
    “freeze” all the existentials appearing in the goals, meaning that
    they are considered rigid during unification and cannot be
@@ -528,15 +528,28 @@ Options
 
 .. flag:: Typeclasses Unique Instances
 
-   Typeclass declarations introduced when this option is set have a more
-   efficient resolution behavior (the option is off by default). When a
+   Typeclass declarations introduced when this flag is set have a more
+   efficient resolution behavior (the flag is off by default). When a
    solution to the typeclass goal of this class is found, we never
    backtrack on it, assuming that it is canonical.
 
+.. flag:: Typeclasses Iterative Deepening
+
+   When this flag is set, the proof search strategy is breadth-first search.
+   Otherwise, the search strategy is depth-first search.  The default is off.
+   :cmd:`Typeclasses eauto` is another way to set this flag.
+
+.. opt:: Typeclasses Depth @num
+   :name: Typeclasses Depth
+
+   Sets the maximum proof search depth.  The default is unbounded.
+   :cmd:`Typeclasses eauto` is another way to set this option.
+
 .. flag:: Typeclasses Debug
 
    Controls whether typeclass resolution steps are shown during search.  Setting this flag
-   also sets :opt:`Typeclasses Debug Verbosity` to 1.
+   also sets :opt:`Typeclasses Debug Verbosity` to 1.  :cmd:`Typeclasses eauto`
+   is another way to set this flag.
 
 .. opt:: Typeclasses Debug Verbosity @num
    :name: Typeclasses Debug Verbosity
@@ -547,7 +560,7 @@ Options
 
 .. flag:: Refine Instance Mode
 
-   This option allows to switch the behavior of instance declarations made through
+   This flag allows to switch the behavior of instance declarations made through
    the Instance command.
 
    + When it is on (the default), instances that have unsolved holes in
@@ -560,14 +573,17 @@ Typeclasses eauto `:=`
 ~~~~~~~~~~~~~~~~~~~~~~
 
 .. cmd:: Typeclasses eauto := {? debug} {? {dfs | bfs}} depth
+   :name: Typeclasses eauto
 
    This command allows more global customization of the typeclass
    resolution tactic. The semantics of the options are:
 
    + ``debug`` In debug mode, the trace of successfully applied tactics is
-     printed.
+     printed.  This value also be set with :flag:`Typeclasses Debug`.
 
    + ``dfs, bfs`` This sets the search strategy to depth-first search (the
-     default) or breadth-first search.
+     default) or breadth-first search.  This value can also be set with
+     :flag:`Typeclasses Iterative Deepening`.
 
-   + ``depth`` This sets the depth limit of the search.
+   + ``depth`` This sets the depth limit of the search.  This value can also be set with
+     :opt:`Typeclasses Depth`.
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.
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 0ea8c7be2d..1071682ead 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -1208,7 +1208,7 @@ Interactive debugger
 
 .. flag:: Ltac Debug
 
-   This option governs the step-by-step debugger that comes with the |Ltac| interpreter
+   This option governs the step-by-step debugger that comes with the |Ltac| interpreter.
 
 When the debugger is activated, it stops at every step of the evaluation of
 the current |Ltac| expression and prints information on what it is doing.
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 3ca0ffe678..e3089f0d09 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -157,14 +157,18 @@ compatible with the rest of |Coq|, up to a few discrepancies:
   (see :ref:`pattern_conditional_ssr`).  To use the
   generalized form, turn off the |SSR| Boolean ``if`` notation using the command:
   ``Close Scope boolean_if_scope``.
-+ The following two options can be unset to disable the incompatible
-  rewrite syntax and allow reserved identifiers to appear in scripts.
++ The following flags can be unset to make |SSR| more compatible with
+  parts of Coq:
 
-  .. coqtop:: in
+.. flag:: SsrRewrite
+
+   Controls whether the incompatible rewrite syntax is enabled (the default).
+   Disabling the flag makes the syntax compatible with other parts of Coq.
 
-     Unset SsrRewrite.
-     Unset SsrIdents.
+.. flag:: SsrIdents
 
+   Controls whether reserved identifiers can appear in scripts.  The default
+   is "on".  "off" is compatible with other parts of Coq.
 
 |Gallina| extensions
 --------------------
@@ -3063,6 +3067,17 @@ An :token:`r_item` can be:
         rewrite -[f y x]/(y + _).
 
 
+.. flag:: SsrOldRewriteGoalsOrder
+
+   Controls the order in which generated subgoals (side conditions)
+   are added to the
+   proof context.  "off", the default value, puts subgoals generated
+   by conditional rules first, followed by the main goal.  "on" puts
+   the main goal first.  If your proofs are organized to complete
+   proving the main goal before side conditions, "on" will save you
+   from having to add :tacn:`last first` tactics that would be needed
+   to keep the main goal as the currently focused goal.
+
 Remarks and examples
 ~~~~~~~~~~~~~~~~~~~~
 
@@ -5428,6 +5443,17 @@ right hand side double , view hint declaration see :ref:`declaring_new_hints_ssr
 
 prenex implicits declaration see :ref:`parametric_polymorphism_ssr`
 
+Settings
+~~~~~~~~
+
+.. flag:: Debug Ssreflect
+
+   *Developer only.* Print debug information on reflect.
+
+.. flag:: Debug SsrMatching
+
+   *Developer only.* Print debug information on SSR matching.
+
 .. rubric:: Footnotes
 
 .. [#1] Unfortunately, even after a call to the Set Printing All command,
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 150aadc15a..6b48c3cc14 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -4503,3 +4503,28 @@ user-defined tactics.
   significant changes in your theories to obtain the same result. As a
   drawback of the re-engineering of the code, this tactic has also been
   completely revised to get a very compact and readable version.
+
+Proof maintenance
+-----------------
+
+*Experimental.*  Many tactics, such as :tacn:`intros`, can automatically generate names, such
+as "H0" or "H1" for a new hypothesis introduced from a goal.  Subsequent proof steps
+may explicitly refer to these names.  However, future versions of Coq may not assign
+names exactly the same way, which could cause the proof to fail because the
+new names don't match the explicit references in the proof.
+
+The following "Mangle Names" settings let users find all the
+places where proofs rely on automatically generated names, which can
+then be named explicitly to avoid any incompatibility.  These
+settings cause Coq to generate different names, producing errors for
+references to automatically generated names.
+
+.. flag:: Mangle Names
+
+   When set, generated names use the prefix specified in the following
+   option instead of the default prefix.
+
+.. opt:: Mangle Names Prefix @string
+   :name: Mangle Names Prefix
+
+   Specifies the prefix to use when generating names.
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index c4d8072ba5..cf5eb442be 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2048,13 +2048,4 @@ let () =
       optread  = (fun () -> get_debug () != Tactic_debug.DebugOff);
       optwrite = vernac_debug }
 
-let () =
-  let open Goptions in
-  declare_bool_option
-    { optdepr  = false;
-      optname  = "Ltac debug";
-      optkey   = ["Debug";"Ltac"];
-      optread  = (fun () -> get_debug () != Tactic_debug.DebugOff);
-      optwrite = vernac_debug }
-
 let () = Hook.set Vernacentries.interp_redexp_hook interp_redexp
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 719d552def..fd2a163f80 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -121,15 +121,7 @@ let () =
       optread  = get_typeclasses_debug;
       optwrite = set_typeclasses_debug; }
 
-let () =
-  declare_bool_option
-    { optdepr  = false;
-      optname  = "debug output for typeclasses proof search";
-      optkey   = ["Debug";"Typeclasses"];
-      optread  = get_typeclasses_debug;
-      optwrite = set_typeclasses_debug; }
-
-let () =
+let _ =
   declare_int_option
     { optdepr  = false;
       optname  = "verbosity of debug output for typeclasses proof search";