Document undocumented flags and options

Also remove a few undocumented settings

3 files changed, 57 insertions, 6 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..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.