Merge PR #8911: Document undocumented flags and options

3 files changed, 96 insertions, 9 deletions

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..9fbac95f0c 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -157,14 +157,24 @@ 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.
+
+.. flag:: SsrIdents
 
-     Unset SsrRewrite.
-     Unset SsrIdents.
+   Controls whether tactics can refer to |SSR|-generated variables that are
+   in the form _xxx_.  Scripts with explicit references to such variables
+   are fragile; they are prone to failure if the proof is later modified or
+   if the details of variable name generation change in future releases of Coq.
 
+   The default is on, which gives an error message when the user tries to
+   create such identifiers.  Disabling the flag generates a warning instead,
+   increasing compatibility with other parts of Coq.
 
 |Gallina| extensions
 --------------------
@@ -3063,6 +3073,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.  The flag is off by default, which puts subgoals generated
+   by conditional rules first, followed by the main goal.  When it is on,
+   the main goal appears first.  If your proofs are organized to complete
+   proving the main goal before side conditions, turning the flag 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 +5449,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..ad80cb62e1 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -264,6 +264,11 @@ Applying theorems
       This tactic behaves like :tacn:`simple refine` except it performs type checking
       without resolution of typeclasses.
 
+   .. flag:: Debug Unification
+
+      Enables printing traces of unification steps used during
+      elaboration/typechecking and the :tacn:`refine` tactic.
+
 .. tacn:: apply @term
    :name: apply
 
@@ -606,6 +611,10 @@ Applying theorems
       when the instantiation of a variable cannot be found
       (cf. :tacn:`eapply` and :tacn:`apply`).
 
+.. flag:: Debug Tactic Unification
+
+   Enables printing traces of unification steps in tactic unification.
+   Tactic unification is used in tactics such as :tacn:`apply` and :tacn:`rewrite`.
 
 .. _managingthelocalcontext:
 
@@ -2096,9 +2105,9 @@ and an explanation of the underlying technique.
    Part of the behavior of the ``inversion`` tactic is to generate
    equalities between expressions that appeared in the hypothesis that is
    being processed. By default, no equalities are generated if they
-   relate two proofs (i.e. equalities between :n:`@terms` whose type is in sort
-   :g:`Prop`). This behavior can be turned off by using the option
-   :flag`Keep Proof Equalities`.
+   relate two proofs (i.e. equalities between :token:`term`\s whose type is in sort
+   :g:`Prop`). This behavior can be turned off by using the
+   :flag:`Keep Proof Equalities` setting.
 
 .. tacv:: inversion @num
 
@@ -2534,6 +2543,13 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
       unresolved bindings into existential variables, if any, instead of
       failing. It has the same variants as :tacn:`rewrite` has.
 
+   .. flag:: Keyed Unification
+
+      Makes higher-order unification used by :tacn:`rewrite` rely on a set of keys to drive
+      unification.  The subterms, considered as rewriting candidates, must start with
+      the same key as the left- or right-hand side of the lemma given to rewrite, and the arguments
+      are then unified up to full reduction.
+
 .. tacn:: replace @term with @term’
    :name: replace
 
@@ -4503,3 +4519,42 @@ 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.
+
+Delaying solving unification constraints
+----------------------------------------
+
+.. tacn:: solve_constraints
+   :name: solve_constraints
+   :undocumented:
+
+.. flag:: Solve Unification Constraints
+
+   By default, after each tactic application, postponed typechecking unification
+   problems are resolved using heuristics. Unsetting this flag disables this
+   behavior, allowing tactics to leave unification constraints unsolved. Use the
+   :tacn:`solve_constraints` tactic at any point to solve the constraints.
+
+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.