Add undocumented options from mattam82

5 files changed, 58 insertions, 13 deletions

diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index 8891234330..e93b01f14d 100644
--- a/doc/sphinx/addendum/extraction.rst
+++ b/doc/sphinx/addendum/extraction.rst
@@ -422,7 +422,7 @@ Additional settings
    :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.
+   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:
 
@@ -454,7 +454,7 @@ Additional settings
 
 .. flag:: Extraction TypeExpand
 
-   If set, fully expand Coq types in ML.  **see type_expand in mlutil.ml**
+   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 7933cdaee0..43d302114e 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -556,7 +556,8 @@ Settings
 
    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
 
@@ -579,7 +580,7 @@ Typeclasses eauto `:=`
    resolution tactic. The semantics of the options are:
 
    + ``debug`` In debug mode, the trace of successfully applied tactics is
-     printed.  This value also be set with :flag:`Typeclasses Debug`.
+     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.  This value can also be set with
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index e3089f0d09..9fbac95f0c 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -167,8 +167,14 @@ compatible with the rest of |Coq|, up to a few discrepancies:
 
 .. flag:: SsrIdents
 
-   Controls whether reserved identifiers can appear in scripts.  The default
-   is "on".  "off" is compatible with other parts of Coq.
+   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
 --------------------
@@ -3071,10 +3077,10 @@ An :token:`r_item` can be:
 
    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
+   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.
 
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 6b48c3cc14..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
 
@@ -4504,6 +4520,20 @@ user-defined tactics.
   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
 -----------------