5 files changed, 48 insertions, 11 deletions
diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst
index 122b0f5dfb..ba0ec28f8b 100644
--- a/doc/sphinx/language/core/inductive.rst
+++ b/doc/sphinx/language/core/inductive.rst
@@ -342,9 +342,9 @@ Recursive functions: fix
 .. insertprodn term_fix fixannot
 
 .. prodn::
-   term_fix ::= let fix @fix_body in @term
-   | fix @fix_body {? {+ with @fix_body } for @ident }
-   fix_body ::= @ident {* @binder } {? @fixannot } {? : @type } := @term
+   term_fix ::= let fix @fix_decl in @term
+   | fix @fix_decl {? {+ with @fix_decl } for @ident }
+   fix_decl ::= @ident {* @binder } {? @fixannot } {? : @type } := @term
    fixannot ::= %{ struct @ident %}
    | %{ wf @one_term @ident %}
    | %{ measure @one_term {? @ident } {? @one_term } %}
diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst
index 561262262b..3c1983ee97 100644
--- a/doc/sphinx/language/extensions/match.rst
+++ b/doc/sphinx/language/extensions/match.rst
@@ -290,6 +290,43 @@ This example emphasizes what the printing settings offer.
 
        Print snd.
 
+Conventions about unused pattern-matching variables
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Pattern-matching variables that are not used on the right-hand side of ``=>`` are
+considered the sign of a potential error. For instance, it could
+result from an undetected mispelled constant constructor. By default,
+a warning is issued in such situations.
+
+.. warn:: Unused variable @ident catches more than one case.
+
+   This indicates that an unused pattern variable :token:`ident`
+   occurs in a pattern-matching clause used to complete at least two
+   cases of the pattern-matching problem.
+
+   The warning can be deactivated by using a variable name starting
+   with ``_`` or by setting ``Set Warnings
+   "-unused-pattern-matching-variable"``.
+
+   Here is an example where the warning is activated.
+
+   .. example::
+
+      .. coqtop:: none
+
+         Set Warnings "-unused-pattern-matching-variable".
+
+      .. coqtop:: all
+
+         Definition is_zero (o : option nat) := match o with
+         | Some 0 => true
+         | x => false
+         end.
+
+      .. coqtop:: none
+
+         Set Warnings "+unused-pattern-matching-variable".
+
 Patterns
 --------
 
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 5c091f04ac..8663ac646b 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -161,7 +161,7 @@ Syntactic values
 Provides a way to use the syntax and semantics of a grammar nonterminal as a
 value in an :token:`ltac_expr`.  The table below describes the most useful of
 these.  You can see the others by running ":cmd:`Print Grammar` `tactic`" and
-examining the part at the end under "Entry tactic:tactic_arg".
+examining the part at the end under "Entry tactic:tactic_value".
 
    :token:`ident`
       name of a grammar nonterminal listed in the table
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 770de9a6c3..cdbae8ade1 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -5724,11 +5724,11 @@ respectively.
 
    local function definition
 
-.. tacv:: pose fix @fix_body
+.. tacv:: pose fix @fix_decl
 
    local fix definition
 
-.. tacv:: pose cofix @fix_body
+.. tacv:: pose cofix @fix_decl
 
    local cofix definition
 
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 0c51361b64..06018304ab 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -444,7 +444,7 @@ Displaying information about notations
 
    This command doesn't display all nonterminals of the grammar.  For example,
    productions shown by `Print Grammar tactic` refer to nonterminals `tactic_then_locality`
-   and `tactic_then_gen` which are not shown and can't be printed.
+   and `for_each_goal` which are not shown and can't be printed.
 
    Most of the grammar in the documentation was updated in 8.12 to make it accurate and
    readable.  This was done using a new developer tool that extracts the grammar from the
@@ -477,16 +477,16 @@ Displaying information about notations
    such as `1+2*3` in the usual way as `1+(2*3)`.  However, most nonterminals have a single level.
 
    For example, this output from `Print Grammar tactic` shows the first 3 levels for
-   `tactic_expr`, designated as "5", "4" and "3".  Level 3 is right-associative,
+   `ltac_expr`, designated as "5", "4" and "3".  Level 3 is right-associative,
    which applies to the productions within it, such as the `try` construct::
 
-     Entry tactic_expr is
+     Entry ltac_expr is
      [ "5" RIGHTA
        [ binder_tactic ]
      | "4" LEFTA
        [ SELF; ";"; binder_tactic
        | SELF; ";"; SELF
-       | SELF; ";"; tactic_then_locality; tactic_then_gen; "]" ]
+       | SELF; ";"; tactic_then_locality; for_each_goal; "]" ]
      | "3" RIGHTA
        [ IDENT "try"; SELF
        :
@@ -510,7 +510,7 @@ Displaying information about notations
 
    The output for `Print Grammar constr` includes :cmd:`Notation` definitions,
    which are dynamically added to the grammar at run time.
-   For example, in the definition for `operconstr`, the production on the second line shown
+   For example, in the definition for `term`, the production on the second line shown
    here is defined by a :cmd:`Reserved Notation` command in `Notations.v`::
 
      | "50" LEFTA