Add undocumented options from mattam82

2 files changed, 45 insertions, 9 deletions

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
 -----------------