Update grammar in the Terms section of Gallina chapter

Update doc_grammar tool

The grammar in the doc is generated semi-automatically with doc_grammar:
- the grammar is automatically extracted from the mlg files
- developer-prepared editing scripts *.mlg_edit modify the extracted
  grammar for clarity, simplicity and ordering of productions
- chunks of the resulting grammar are automatically inserted into the
  rsts using instructions embedded in the rsts

Running doc_grammar is currently a manual step.

The grammar updates in the rst files have been manually reviewed.

2 files changed, 6 insertions, 6 deletions

diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index e37f300915..b2b426ada5 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -127,7 +127,7 @@ mode but it can also be used in toplevel definitions as shown below.
                      : gfail [`natural`] [`message_token` ... `message_token`]
                      : fresh [ `component` … `component` ]
                      : context `ident` [`term`]
-                     : eval `redexpr` in `term`
+                     : eval `red_expr` in `term`
                      : type of `term`
                      : constr : `term`
                      : uconstr : `term`
@@ -986,9 +986,9 @@ Computing in a constr
 
 Evaluation of a term can be performed with:
 
-.. tacn:: eval @redexpr in @term
+.. tacn:: eval @red_expr in @term
 
-   where :n:`@redexpr` is a reduction tactic among :tacn:`red`, :tacn:`hnf`,
+   where :n:`@red_expr` is a reduction tactic among :tacn:`red`, :tacn:`hnf`,
    :tacn:`compute`, :tacn:`simpl`, :tacn:`cbv`, :tacn:`lazy`, :tacn:`unfold`,
    :tacn:`fold`, :tacn:`pattern`.
 
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index e87b76b4ab..89b24ea8a3 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -195,7 +195,7 @@ Requests to the environment
       (see Section :ref:`invocation-of-tactics`).
 
 
-.. cmd:: Eval @redexpr in @term
+.. cmd:: Eval @red_expr in @term
 
    This command performs the specified reduction on :n:`@term`, and displays
    the resulting term with its type. The term to be reduced may depend on
@@ -1146,7 +1146,7 @@ described first.
       Print all the currently non-transparent strategies.
 
 
-.. cmd:: Declare Reduction @ident := @redexpr
+.. cmd:: Declare Reduction @ident := @red_expr
 
    This command allows giving a short name to a reduction expression, for
    instance ``lazy beta delta [foo bar]``. This short name can then be used
@@ -1158,7 +1158,7 @@ described first.
    functor applications will be rejected if these declarations are not
    local. The name :n:`@ident` cannot be used directly as an Ltac tactic, but
    nothing prevents the user from also performing a
-   :n:`Ltac @ident := @redexpr`.
+   :n:`Ltac @ident := @red_expr`.
 
    .. seealso:: :ref:`performingcomputations`