Merge PR #8911: Document undocumented flags and options

3 files changed, 90 insertions, 19 deletions

diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index b7d05fd6ef..e93b01f14d 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 :token:`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 the Coq source code to learn more.
+
 Differences between |Coq| and ML type systems
 ----------------------------------------------
 
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index 429dcbee69..56f84d0ff0 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -95,6 +95,14 @@ coercions.
    (the option is on by default). Coercion of subset types and pairs is still
    active in this case.
 
+.. flag:: Program Mode
+
+   Enables the program mode, in which 1) typechecking allows subset coercions and
+   2) the elaboration of pattern matching of :cmd:`Program Fixpoint` and
+   :cmd:`Program Definition` act
+   like Program Fixpoint/Definition, generating obligations if there are
+   unresolved holes after typechecking.
+
 .. _syntactic_control:
 
 Syntactic control over equalities
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 98dfcb2373..43d302114e 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,26 +528,40 @@ 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
 
    Determines how much information is shown for typeclass resolution steps during search.
    1 is the default level.  2 shows additional information such as tried tactics and shelving
-   of goals.  Setting this option also sets :flag:`Typeclasses Debug`.
+   of goals.  Setting this option to 1 or 2 turns on :flag:`Typeclasses Debug`; setting this
+   option to 0 turns that option off.
 
 .. 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 +574,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 can 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`.