Define many undefined tokens, and other misc fixes.

Progress towards #9411, extracted from #10118, rebased ontop of #10192.

11 files changed, 205 insertions, 215 deletions

diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index 68f6d4008a..e58049b8d0 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -528,7 +528,7 @@ pass additional arguments such as ``using relation``.
 .. tacv:: setoid_reflexivity
           setoid_symmetry {? in @ident}
           setoid_transitivity
-          setoid_rewrite {? @orientation} @term {? at @occs} {? in @ident}
+          setoid_rewrite {? @orientation} @term {? at @occurrences} {? in @ident}
           setoid_replace @term with @term {? using relation @term} {? in @ident} {? by @tactic}
    :name: setoid_reflexivity; setoid_symmetry; setoid_transitivity; setoid_rewrite; setoid_replace
 
@@ -567,13 +567,13 @@ Printing relations and morphisms
 Deprecated syntax and backward incompatibilities
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmd:: Add Setoid @A @Aeq @ST as @ident
+.. cmd:: Add Setoid @qualid__1 @qualid__2 @qualid__3 as @ident
 
    This command for declaring setoids and morphisms is also accepted due
    to backward compatibility reasons.
 
-   Here ``Aeq`` is a congruence relation without parameters, ``A`` is its carrier
-   and ``ST`` is an object of type (``Setoid_Theory A Aeq``) (i.e. a record
+   Here :n:`@qualid__2` is a congruence relation without parameters, :n:`@qualid__1` is its carrier
+   and :n:`@qualid__3` is an object of type (:n:`Setoid_Theory @qualid__1 @qualid__2`) (i.e. a record
    packing together the reflexivity, symmetry and transitivity lemmas).
    Notice that the syntax is not completely backward compatible since the
    identifier was not required.
@@ -708,91 +708,65 @@ Definitions
 The generalized rewriting tactic is based on a set of strategies that can be
 combined to obtain custom rewriting procedures. Its set of strategies is based
 on Elan’s rewriting strategies :cite:`Luttik97specificationof`. Rewriting
-strategies are applied using the tactic ``rewrite_strat s`` where ``s`` is a
+strategies are applied using the tactic :n:`rewrite_strat @strategy` where :token:`strategy` is a
 strategy expression. Strategies are defined inductively as described by the
 following grammar:
 
-.. productionlist:: rewriting
-   s, t, u : `strategy`
-           : `lemma`
-           : `lemma_right_to_left`
-           : `failure`
-           : `identity`
-           : `reflexivity`
-           : `progress`
-           : `failure_catch`
-           : `composition`
-           : `left_biased_choice`
-           : `iteration_one_or_more`
-           : `iteration_zero_or_more`
-           : `one_subterm`
-           : `all_subterms`
-           : `innermost_first`
-           : `outermost_first`
-           : `bottom_up`
-           : `top_down`
-           : `apply_hint`
-           : `any_of_the_terms`
-           : `apply_reduction`
-           : `fold_expression`
-
-.. productionlist:: rewriting
-   strategy : ( `s` )
-   lemma : `c`
-   lemma_right_to_left : <- `c`
-   failure : fail
-   identity : id
-   reflexivity : refl
-   progress : progress `s`
-   failure_catch : try `s`
-   composition : `s` ; `u`
-   left_biased_choice : choice `s` `t`
-   iteration_one_or_more : repeat `s`
-   iteration_zero_or_more : any `s`
-   one_subterm : subterm `s`
-   all_subterms : subterms `s`
-   innermost_first : innermost `s`
-   outermost_first : outermost `s`
-   bottom_up : bottomup `s`
-   top_down : topdown `s`
-   apply_hint : hints `hintdb`
-   any_of_the_terms : terms (`c`)+
-   apply_reduction : eval `redexpr`
-   fold_expression : fold `c`
-
+.. productionlist:: coq
+   strategy : `qualid`                   (lemma, left to right)
+            : <- `qualid`                (lemma, right to left)
+            : fail                    (failure)
+            : id                      (identity)
+            : refl                    (reflexivity)
+            : progress `strategy`        (progress)
+            : try `strategy`             (try catch)
+            : `strategy` ; `strategy`       (composition)
+            : choice `strategy` `strategy`  (left_biased_choice)
+            : repeat `strategy`          (one or more)
+            : any `strategy`             (zero or more)
+            : subterm `strategy`         (one subterm)
+            : subterms `strategy`        (all subterms)
+            : innermost `strategy`       (innermost first)
+            : outermost `strategy`       (outermost first)
+            : bottomup `strategy`        (bottom-up)
+            : topdown `strategy`         (top-down)
+            : hints `ident`              (apply hints from hint database)
+            : terms `term` ... `term`      (any of the terms)
+            : eval `redexpr`             (apply reduction)
+            : fold `term`               (unify)
+            : ( `strategy` )
 
 Actually a few of these are defined in term of the others using a
 primitive fixpoint operator:
 
-.. productionlist:: rewriting
-   try `s` : choice `s` `id`
-   any `s` : fix `u`. try (`s` ; `u`)
-   repeat `s` : `s` ; any `s`
-   bottomup s : fix `bu`. (choice (progress (subterms bu)) s) ; try bu
-   topdown s : fix `td`. (choice s (progress (subterms td))) ; try td
-   innermost s : fix `i`. (choice (subterm i) s)
-   outermost s : fix `o`. (choice s (subterm o))
+- :n:`try @strategy := choice @strategy id`
+- :n:`any @strategy := fix @ident. try (@strategy ; @ident)`
+- :n:`repeat @strategy := @strategy; any @strategy`
+- :n:`bottomup @strategy := fix @ident. (choice (progress (subterms @ident)) @strategy) ; try @ident`
+- :n:`topdown @strategy := fix @ident. (choice @strategy (progress (subterms @ident))) ; try @ident`
+- :n:`innermost @strategy := fix @ident. (choice (subterm @ident) @strategy)`
+- :n:`outermost @strategy := fix @ident. (choice @strategy (subterm @ident))`
 
 The basic control strategy semantics are straightforward: strategies
 are applied to subterms of the term to rewrite, starting from the root
 of the term. The lemma strategies unify the left-hand-side of the
 lemma with the current subterm and on success rewrite it to the right-
 hand-side. Composition can be used to continue rewriting on the
-current subterm. The fail strategy always fails while the identity
+current subterm. The ``fail`` strategy always fails while the identity
 strategy succeeds without making progress. The reflexivity strategy
 succeeds, making progress using a reflexivity proof of rewriting.
-Progress tests progress of the argument strategy and fails if no
+``progress`` tests progress of the argument :token:`strategy` and fails if no
 progress was made, while ``try`` always succeeds, catching failures.
-Choice is left-biased: it will launch the first strategy and fall back
+``choice`` is left-biased: it will launch the first strategy and fall back
 on the second one in case of failure. One can iterate a strategy at
 least 1 time using ``repeat`` and at least 0 times using ``any``.
 
-The ``subterm`` and ``subterms`` strategies apply their argument strategy ``s`` to
+The ``subterm`` and ``subterms`` strategies apply their argument :token:`strategy` to
 respectively one or all subterms of the current term under
 consideration, left-to-right. ``subterm`` stops at the first subterm for
-which ``s`` made progress. The composite strategies ``innermost`` and ``outermost``
+which :token:`strategy` made progress. The composite strategies ``innermost`` and ``outermost``
 perform a single innermost or outermost rewrite using their argument
-strategy. Their counterparts ``bottomup`` and ``topdown`` perform as many
+:token:`strategy`. Their counterparts ``bottomup`` and ``topdown`` perform as many
 rewritings as possible, starting from the bottom or the top of the
 term.
 
@@ -802,15 +776,15 @@ lemmas at the current subterm. The ``terms`` strategy takes the lemma
 names directly as arguments. The ``eval`` strategy expects a reduction
 expression (see :ref:`performingcomputations`) and succeeds
 if it reduces the subterm under consideration. The ``fold`` strategy takes
-a term ``c`` and tries to *unify* it to the current subterm, converting it to ``c``
-on success, it is stronger than the tactic ``fold``.
+a :token:`term` and tries to *unify* it to the current subterm, converting it to :token:`term`
+on success. It is stronger than the tactic ``fold``.
 
 
 Usage
 ~~~~~
 
 
-.. tacn:: rewrite_strat @s {? in @ident }
+.. tacn:: rewrite_strat @strategy {? in @ident }
    :name: rewrite_strat
 
    Rewrite using the strategy s in hypothesis ident or the conclusion.
diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst
index 3b350d5dc0..3f4d5cc784 100644
--- a/doc/sphinx/addendum/ring.rst
+++ b/doc/sphinx/addendum/ring.rst
@@ -310,10 +310,10 @@ The syntax for adding a new ring is
    .. productionlist:: coq
       ring_mod : abstract | decidable `term` | morphism `term`
                : setoid `term` `term`
-               : constants [`ltac`]
-               : preprocess [`ltac`]
-               : postprocess [`ltac`]
-               : power_tac `term` [`ltac`]
+               : constants [ `tactic` ]
+               : preprocess [ `tactic` ]
+               : postprocess [ `tactic` ]
+               : power_tac `term` [ `tactic` ]
                : sign `term`
                : div `term`
 
@@ -341,31 +341,31 @@ The syntax for adding a new ring is
       This modifier needs not be used if the setoid and morphisms have been
       declared.
 
-   constants [ :n:`@ltac` ]
-      specifies a tactic expression :n:`@ltac` that, given a
+   constants [ :n:`@tactic` ]
+      specifies a tactic expression :n:`@tactic` that, given a
       term, returns either an object of the coefficient set that is mapped
       to the expression via the morphism, or returns
       ``InitialRing.NotConstant``. The default behavior is to map only 0 and 1
       to their counterpart in the coefficient set. This is generally not
       desirable for non trivial computational rings.
 
-   preprocess [ :n:`@ltac` ]
-      specifies a tactic :n:`@ltac` that is applied as a
+   preprocess [ :n:`@tactic` ]
+      specifies a tactic :n:`@tactic` that is applied as a
       preliminary step for :tacn:`ring` and :tacn:`ring_simplify`. It can be used to
       transform a goal so that it is better recognized. For instance, ``S n``
       can be changed to ``plus 1 n``.
 
-   postprocess [ :n:`@ltac` ]
-      specifies a tactic :n:`@ltac` that is applied as a final
+   postprocess [ :n:`@tactic` ]
+      specifies a tactic :n:`@tactic` that is applied as a final
       step for :tacn:`ring_simplify`. For instance, it can be used to undo
       modifications of the preprocessor.
 
-   power_tac :n:`@term` [ :n:`@ltac` ]
+   power_tac :n:`@term` [ :n:`@tactic` ]
       allows :tacn:`ring` and :tacn:`ring_simplify` to recognize
       power expressions with a constant positive integer exponent (example:
       :math:`x^2` ). The term :n:`@term` is a proof that a given power function satisfies
       the specification of a power function (term has to be a proof of
-      ``Ring_theory.power_theory``) and :n:`@ltac` specifies a tactic expression
+      ``Ring_theory.power_theory``) and :n:`@tactic` specifies a tactic expression
       that, given a term, “abstracts” it into an object of type |N| whose
       interpretation via ``Cp_phi`` (the evaluation function of power
       coefficient) is the original term, or returns ``InitialRing.NotConstant``
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index 1aa2111816..395b5ce2d3 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -366,24 +366,32 @@ The syntax has been extended to allow users to explicitly bind names
 to universes and explicitly instantiate polymorphic definitions.
 
 .. cmd:: Universe @ident
+         Polymorphic Universe @ident
 
    In the monorphic case, this command declares a new global universe
    named :g:`ident`, which can be referred to using its qualified name
    as well. Global universe names live in a separate namespace. The
-   command supports the polymorphic flag only in sections, meaning the
+   command supports the ``Polymorphic`` flag only in sections, meaning the
    universe quantification will be discharged on each section definition
    independently. One cannot mix polymorphic and monomorphic
    declarations in the same section.
 
 
-.. cmd:: Constraint @ident @ord @ident
+.. cmd:: Constraint @universe_constraint
+         Polymorphic Constraint @universe_constraint
 
-   This command declares a new constraint between named universes. The
-   order relation :n:`@ord` can be one of :math:`<`, :math:`≤` or :math:`=`. If consistent, the constraint
-   is then enforced in the global environment. Like ``Universe``, it can be
-   used with the ``Polymorphic`` prefix in sections only to declare
-   constraints discharged at section closing time. One cannot declare a
-   global constraint on polymorphic universes.
+   This command declares a new constraint between named universes.
+
+   .. productionlist:: coq
+      universe_constraint : `qualid` < `qualid`
+                          : `qualid` <= `qualid`
+                          : `qualid` = `qualid`
+
+   If consistent, the constraint is then enforced in the global
+   environment. Like :cmd:`Universe`, it can be used with the
+   ``Polymorphic`` prefix in sections only to declare constraints
+   discharged at section closing time. One cannot declare a global
+   constraint on polymorphic universes.
 
    .. exn:: Undeclared universe @ident.
       :undocumented:
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 2b673ff62b..c1af4d067f 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -603,11 +603,16 @@ The following experimental command is available when the ``FunInd`` library has
    The meaning of this declaration is to define a function ident,
    similarly to ``Fixpoint``. Like in ``Fixpoint``, the decreasing argument must
    be given (unless the function is not recursive), but it might not
-   necessarily be *structurally* decreasing. The point of the {} annotation
+   necessarily be *structurally* decreasing. The point of the :n:`{ @decrease_annot }` annotation
    is to name the decreasing argument *and* to describe which kind of
    decreasing criteria must be used to ensure termination of recursive
    calls.
 
+   .. productionlist::
+      decrease_annot : struct `ident`
+                     : measure `term` `ident`
+                     : wf `term` `ident`
+
 The ``Function`` construction also enjoys the ``with`` extension to define
 mutually recursive definitions. However, this feature does not work
 for non structurally recursive functions.
@@ -616,31 +621,33 @@ See the documentation of functional induction (:tacn:`function induction`)
 and ``Functional Scheme`` (:ref:`functional-scheme`) for how to use
 the induction principle to easily reason about the function.
 
-Remark: To obtain the right principle, it is better to put rigid
-parameters of the function as first arguments. For example it is
-better to define plus like this:
+.. note::
 
-.. coqtop:: reset none
+   To obtain the right principle, it is better to put rigid
+   parameters of the function as first arguments. For example it is
+   better to define plus like this:
 
-   Require Import FunInd.
+   .. coqtop:: reset none
 
-.. coqtop:: all
+      Require Import FunInd.
 
-   Function plus (m n : nat) {struct n} : nat :=
-   match n with
-   | 0 => m
-   | S p => S (plus m p)
-   end.
+   .. coqtop:: all
 
-than like this:
+      Function plus (m n : nat) {struct n} : nat :=
+      match n with
+      | 0 => m
+      | S p => S (plus m p)
+      end.
 
-.. coqtop:: reset all
+   than like this:
 
-   Function plus (n m : nat) {struct n} : nat :=
-   match n with
-   | 0 => m
-   | S p => S (plus p m)
-   end.
+   .. coqtop:: reset all
+
+      Function plus (n m : nat) {struct n} : nat :=
+      match n with
+      | 0 => m
+      | S p => S (plus p m)
+      end.
 
 
 *Limitations*
@@ -710,7 +717,7 @@ used by ``Function``. A more precise description is given below.
    with :cmd:`Fixpoint`. Moreover the following are defined:
 
     + The same objects as above;
-    + The fixpoint equation of :token:`ident`: :n:`@ident_equation`.
+    + The fixpoint equation of :token:`ident`: :token:`ident`\ ``_equation``.
 
 .. cmdv:: Function @ident {* @binder } { measure @term @ident } : @type := @term
           Function @ident {* @binder } { wf @term @ident } : @type := @term
@@ -1909,7 +1916,7 @@ This syntax extension is given in the following grammar:
 Renaming implicit arguments
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmd:: Arguments @qualid {* @name} : @rename
+.. cmd:: Arguments @qualid {* @name} : rename
    :name: Arguments (rename)
 
    This command is used to redefine the names of implicit arguments.
@@ -2296,7 +2303,7 @@ Printing universes
       language, and can be processed by Graphviz tools. The format is
       unspecified if `string` doesn’t end in ``.dot`` or ``.gv``.
 
-.. cmdv:: Print Universes Subgraph(@names)
+.. cmdv:: Print Universes Subgraph({+ @qualid })
    :name: Print Universes Subgraph
 
    Prints the graph restricted to the requested names (adjusting
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 0a95a6edd6..c48dd5b99e 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -32,22 +32,25 @@ The syntax of the tactic language is given below. See Chapter
 :ref:`gallinaspecificationlanguage` for a description of the BNF metasyntax used
 in these grammar rules. Various already defined entries will be used in this
 chapter: entries :token:`natural`, :token:`integer`, :token:`ident`,
-:token:`qualid`, :token:`term`, :token:`cpattern` and :token:`atomic_tactic`
+:token:`qualid`, :token:`term`, :token:`cpattern` and :token:`tactic`
 represent respectively the natural and integer numbers, the authorized
 identificators and qualified names, Coq terms and patterns and all the atomic
-tactics described in Chapter :ref:`tactics`. The syntax of :token:`cpattern` is
+tactics described in Chapter :ref:`tactics`.
+
+The syntax of :production:`cpattern` is
 the same as that of terms, but it is extended with pattern matching
 metavariables. In :token:`cpattern`, a pattern matching metavariable is
-represented with the syntax :g:`?id` where :g:`id` is an :token:`ident`. The
+represented with the syntax :n:`?@ident`. The
 notation :g:`_` can also be used to denote metavariable whose instance is
-irrelevant. In the notation :g:`?id`, the identifier allows us to keep
+irrelevant. In the notation :n:`?@ident`, the identifier allows us to keep
 instantiations and to make constraints whereas :g:`_` shows that we are not
 interested in what will be matched. On the right hand side of pattern matching
 clauses, the named metavariables are used without the question mark prefix. There
 is also a special notation for second-order pattern matching problems: in an
-applicative pattern of the form :g:`@?id id1 … idn`, the variable id matches any
-complex expression with (possible) dependencies in the variables :g:`id1 … idn`
-and returns a functional term of the form :g:`fun id1 … idn => term`.
+applicative pattern of the form :n:`%@?@ident @ident__1 … @ident__n`,
+the variable :token:`ident` matches any complex expression with (possible)
+dependencies in the variables :n:`@ident__i` and returns a functional term
+of the form :n:`fun @ident__1 … ident__n => @term`.
 
 The main entry of the grammar is :n:`@expr`. This language is used in proof
 mode but it can also be used in toplevel definitions as shown below.
@@ -133,7 +136,7 @@ mode but it can also be used in toplevel definitions as shown below.
                      : guard `test`
                      : assert_fails `tacexpr3`
                      : assert_succeeds `tacexpr3`
-                     : `atomic_tactic`
+                     : `tactic`
                      : `qualid` `tacarg` ... `tacarg`
                      : `atom`
    atom              : `qualid`
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index aa603fc966..2f9c7c2b89 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -179,7 +179,7 @@ constructions from ML.
                     : let `ltac2_var` := `ltac2_term` in `ltac2_term`
                     : let rec `ltac2_var` := `ltac2_term` in `ltac2_term`
                     : match `ltac2_term` with `ltac2_branch` ... `ltac2_branch` end
-                    : `int`
+                    : `integer`
                     : `string`
                     : `ltac2_term` ; `ltac2_term`
                     : [| `ltac2_term` ; ... ; `ltac2_term` |]
@@ -619,7 +619,7 @@ calls to term matching functions from the `Pattern` module. Internally, it is
 implemented thanks to a specific scope accepting the :n:`@constrmatching` syntax.
 
 Variables from the :n:`@constrpattern` are statically bound in the body of the branch, to
-values of type `constr` for the variables from the :n:`@constr` pattern and to a
+values of type `constr` for the variables from the :n:`@term` pattern and to a
 value of type `Pattern.context` for the variable :n:`@lident`.
 
 Note that unlike Ltac, only lowercase identifiers are valid as Ltac2
@@ -686,20 +686,22 @@ The following scopes are built-in.
 
 - :n:`list0(@ltac2_scope)`:
 
-  + if :n:`@ltac2_scope` parses :production:`entry`, parses :n:`(@entry__0, ..., @entry__n)` and produces
-    :n:`[@entry__0; ...; @entry__n]`.
+  + if :n:`@ltac2_scope` parses :n:`@quotentry`,
+    then it parses :n:`(@quotentry__0, ..., @quotentry__n)` and produces
+    :n:`[@quotentry__0; ...; @quotentry__n]`.
 
 - :n:`list0(@ltac2_scope, sep = @string__sep)`:
 
-  + if :n:`@ltac2_scope` parses :n:`@entry`, parses :n:`(@entry__0 @string__sep ... @string__sep @entry__n)`
-    and produces :n:`[@entry__0; ...; @entry__n]`.
+  + if :n:`@ltac2_scope` parses :n:`@quotentry`,
+    then it parses :n:`(@quotentry__0 @string__sep ... @string__sep @quotentry__n)`
+    and produce :n:`[@quotentry__0; ...; @quotentry__n]`.
 
-- :n:`list1`: same as :n:`list0` (with or without separator) but parses :n:`{+ @entry}` instead
-  of :n:`{* @entry}`.
+- :n:`list1`: same as :n:`list0` (with or without separator) but parses :n:`{+ @quotentry}` instead
+  of :n:`{* @quotentry}`.
 
 - :n:`opt(@ltac2_scope)`
 
-  + if :n:`@ltac2_scope` parses :n:`@entry`, parses :n:`{? @entry}` and produces either :n:`None` or
+  + if :n:`@ltac2_scope` parses :n:`@quotentry`, parses :n:`{? @quotentry}` and produces either :n:`None` or
     :n:`Some x` where :n:`x` is the parsed expression.
 
 - :n:`self`:
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 4a2f9c0db3..3f966755ca 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -175,12 +175,12 @@ list of assertion commands is given in :ref:`Assertions`. The command
 
       Use all section variables except the list of :token:`ident`.
 
-   .. cmdv:: Proof using @collection1 + @collection2
+   .. cmdv:: Proof using @collection__1 + @collection__2
 
       Use section variables from the union of both collections.
       See :ref:`nameaset` to know how to form a named collection.
 
-   .. cmdv:: Proof using @collection1 - @collection2
+   .. cmdv:: Proof using @collection__1 - @collection__2
 
       Use section variables which are in the first collection but not in the
       second one.
@@ -202,10 +202,10 @@ Proof using options
 The following options modify the behavior of ``Proof using``.
 
 
-.. opt:: Default Proof Using "@expression"
+.. opt:: Default Proof Using "@collection"
    :name: Default Proof Using
 
-   Use :n:`@expression` as the default ``Proof using`` value. E.g. ``Set Default
+   Use :n:`@collection` as the default ``Proof using`` value. E.g. ``Set Default
    Proof Using "a b"`` will complete all ``Proof`` commands not followed by a
    ``using`` part with ``using a b``.
 
@@ -220,7 +220,7 @@ The following options modify the behavior of ``Proof using``.
 Name a set of section hypotheses for ``Proof using``
 ````````````````````````````````````````````````````
 
-.. cmd:: Collection @ident := @expression
+.. cmd:: Collection @ident := @collection
 
    This can be used to name a set of section
    hypotheses, with the purpose of making ``Proof using`` annotations more
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 45c40ee787..3149d64d3e 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -3478,7 +3478,7 @@ efficient ones, e.g. for the purpose of a correctness proof.
 Wildcards vs abstractions
 `````````````````````````
 
-The rewrite tactic supports :token:`r_items` containing holes. For example, in
+The rewrite tactic supports :token:`r_item`\s containing holes. For example, in
 the tactic ``rewrite (_ : _ * 0 = 0).``
 the term ``_ * 0 = 0`` is interpreted as ``forall n : nat, n * 0 = 0.``
 Anyway this tactic is *not* equivalent to
@@ -3753,7 +3753,7 @@ involves the following steps:
 
 3. If so :tacn:`under` puts these n goals in head normal form (using
    the defective form of the tactic :tacn:`move`), then executes
-   the corresponding intro pattern :n:`@ipat__i` in each goal.
+   the corresponding intro pattern :n:`@i_pattern__i` in each goal.
 
 4. Then :tacn:`under` checks that the first n subgoals
    are (quantified) equalities or double implications between a
@@ -3802,11 +3802,11 @@ One-liner mode
 
 The Ltac expression:
 
-:n:`under @term => [ @i_item__1 | … | @i_item__n ] do [ @tac__1 | … | @tac__n ].`
+:n:`under @term => [ @i_item__1 | … | @i_item__n ] do [ @tactic__1 | … | @tactic__n ].`
 
 can be seen as a shorter form for the following expression:
 
-:n:`(under @term) => [ @i_item__1 | … | @i_item__n | ]; [ @tac__1; over | … | @tac__n; over | cbv beta iota ].`
+:n:`(under @term) => [ @i_item__1 | … | @i_item__n | ]; [ @tactic__1; over | … | @tactic__n; over | cbv beta iota ].`
 
 Notes:
 
@@ -3819,14 +3819,14 @@ Notes:
   involving the `bigop` theory from the Mathematical Components library.
 
 + If there is only one tactic, the brackets can be omitted, e.g.:
-  :n:`under @term => i do @tac.` and that shorter form should be
+  :n:`under @term => i do @tactic.` and that shorter form should be
   preferred.
 
 + If the ``do`` clause is provided and the intro pattern is omitted,
   then the default :token:`i_item` ``*`` is applied to each branch.
   E.g., the Ltac expression:
-  :n:`under @term do [ @tac__1 | … | @tac__n ]` is equivalent to:
-  :n:`under @term => [ * | … | * ] do [ @tac__1 | … | @tac__n ]`
+  :n:`under @term do [ @tactic__1 | … | @tactic__n ]` is equivalent to:
+  :n:`under @term => [ * | … | * ] do [ @tactic__1 | … | @tactic__n ]`
   (and it can be noted here that the :tacn:`under` tactic performs a
   ``move.`` before processing the intro patterns ``=> [ * | … | * ]``).
 
@@ -4237,7 +4237,7 @@ selecting a specific redex and has been described in the previous
 sections. We have seen so far that the possibility of selecting a
 redex using a term with holes is already a powerful means of redex
 selection. Similarly, any terms provided by the user in the more
-complex forms of :token:`c_patterns`
+complex forms of :token:`c_pattern`\s
 presented in the tables above can contain
 holes.
 
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index cdd23f4d06..0c86e31052 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -462,7 +462,7 @@ Occurrence sets and occurrence clauses
 An occurrence clause is a modifier to some tactics that obeys the
 following syntax:
 
-  .. productionlist:: sentence
+  .. productionlist:: coq
      occurrence_clause : in `goal_occurrences`
      goal_occurrences : [`ident` [`at_occurrences`], ... , `ident` [`at_occurrences`] [|- [* [`at_occurrences`]]]]
                       : * |- [* [`at_occurrences`]]
@@ -2127,7 +2127,7 @@ and an explanation of the underlying technique.
    :name: discriminate
 
    This tactic proves any goal from an assumption stating that two
-   structurally different :n:`@terms` of an inductive set are equal. For
+   structurally different :n:`@term`\s of an inductive set are equal. For
    example, from :g:`(S (S O))=(S O)` we can derive by absurdity any
    proposition.
 
@@ -2294,7 +2294,7 @@ and an explanation of the underlying technique.
 
    .. flag:: Keep Proof Equalities
 
-      By default, :tacn:`injection` only creates new equalities between :n:`@terms`
+      By default, :tacn:`injection` only creates new equalities between :n:`@term`\s
       whose type is in sort :g:`Type` or :g:`Set`, thus implementing a special
       behavior for objects that are proofs of a statement in :g:`Prop`. This option
       controls this behavior.
@@ -2705,8 +2705,8 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
 
    .. tacv:: rewrite @term in @goal_occurrences
 
-      Analogous to :n:`rewrite @term` but rewriting is done following clause
-      (similarly to :ref:`performing computations <performingcomputations>`). For instance:
+      Analogous to :n:`rewrite @term` but rewriting is done following
+      the clause :token:`goal_occurrences`. For instance:
 
       + :n:`rewrite H in H'` will rewrite `H` in the hypothesis
         ``H'`` instead of the current goal.
@@ -2724,7 +2724,7 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
 
    .. tacv:: rewrite @term at @occurrences
 
-      Rewrite only the given occurrences of :token:`term`. Occurrences are
+      Rewrite only the given :token:`occurrences` of :token:`term`. Occurrences are
       specified from left to right as for pattern (:tacn:`pattern`). The rewrite is
       always performed using setoid rewriting, even for Leibniz’s equality, so one
       has to ``Import Setoid`` to use this variant.
@@ -2734,11 +2734,11 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
       Use tactic to completely solve the side-conditions arising from the
       :tacn:`rewrite`.
 
-   .. tacv:: rewrite {+, @term}
+   .. tacv:: rewrite {+, @orientation @term} {? in @ident }
 
       Is equivalent to the `n` successive tactics :n:`{+; rewrite @term}`, each one
-      working on the first subgoal generated by the previous one. Orientation
-      :g:`->` or :g:`<-` can be inserted before each :token:`term` to rewrite.  One
+      working on the first subgoal generated by the previous one. An :production:`orientation`
+      ``->`` or ``<-`` can be inserted before each :token:`term` to rewrite.  One
       unique clause can be added at the end after the keyword in; it will then
       affect all rewrite operations.
 
@@ -3065,7 +3065,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
 .. tacv:: native_compute
    :name: native_compute
 
-   This tactic evaluates the goal by compilation to Objective Caml as described
+   This tactic evaluates the goal by compilation to OCaml as described
    in :cite:`FullReduction`. If Coq is running in native code, it can be
    typically two to five times faster than ``vm_compute``. Note however that the
    compilation cost is higher, so it is worth using only for intensive
@@ -3231,8 +3231,8 @@ the conversion in hypotheses :n:`{+ @ident}`.
 
 .. tacv:: simpl @pattern
 
-   This applies ``simpl`` only to the subterms matching :n:`@pattern` in the
-   current goal.
+   This applies :tacn:`simpl` only to the subterms matching
+   :n:`@pattern` in the current goal.
 
 .. tacv:: simpl @pattern at {+ @num}
 
@@ -3448,9 +3448,9 @@ Automation
       :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` for the list of
       pre-defined databases and the way to create or extend a database.
 
-   .. tacv:: auto using {+ @ident__i} {? with {+ @ident } }
+   .. tacv:: auto using {+ @qualid__i} {? with {+ @ident } }
 
-      Uses lemmas :n:`@ident__i` in addition to hints. If :n:`@ident` is an
+      Uses lemmas :n:`@qualid__i` in addition to hints. If :n:`@qualid` is an
       inductive type, it is the collection of its constructors which are added
       as hints.
 
@@ -3458,8 +3458,8 @@ Automation
 
          The hints passed through the `using` clause are used in the same
          way as if they were passed through a hint database. Consequently,
-         they use a weaker version of :tacn:`apply` and :n:`auto using @ident`
-         may fail where :n:`apply @ident` succeeds.
+         they use a weaker version of :tacn:`apply` and :n:`auto using @qualid`
+         may fail where :n:`apply @qualid` succeeds.
 
          Given that this can be seen as counter-intuitive, it could be useful
          to have an option to use full-blown :tacn:`apply` for lemmas passed
@@ -3477,7 +3477,7 @@ Automation
       Behaves like :tacn:`auto` but shows the tactics it tries to solve the goal,
       including failing paths.
 
-   .. tacv:: {? info_}auto {? @num} {? using {+ @lemma}} {? with {+ @ident}}
+   .. tacv:: {? info_}auto {? @num} {? using {+ @qualid}} {? with {+ @ident}}
 
       This is the most general form, combining the various options.
 
@@ -3490,10 +3490,10 @@ Automation
 
    .. tacv:: trivial with {+ @ident}
              trivial with *
-             trivial using {+ @lemma}
+             trivial using {+ @qualid}
              debug trivial
              info_trivial
-             {? info_}trivial {? using {+ @lemma}} {? with {+ @ident}}
+             {? info_}trivial {? using {+ @qualid}} {? with {+ @ident}}
       :name: _; _; _; debug trivial; info_trivial; _
       :undocumented:
 
@@ -3532,7 +3532,7 @@ Automation
       Note that ``ex_intro`` should be declared as a hint.
 
 
-   .. tacv:: {? info_}eauto {? @num} {? using {+ @lemma}} {? with {+ @ident}}
+   .. tacv:: {? info_}eauto {? @num} {? using {+ @qualid}} {? with {+ @ident}}
 
       The various options for :tacn:`eauto` are the same as for :tacn:`auto`.
 
@@ -3593,10 +3593,9 @@ Automation
   Performs all the rewritings in hypothesis :n:`@qualid` applying :n:`@tactic`
   to the main subgoal after each rewriting step.
 
-.. tacv:: autorewrite with {+ @ident} in @clause
+.. tacv:: autorewrite with {+ @ident} in @goal_occurrences
 
-  Performs all the rewriting in the clause :n:`@clause`. The clause argument
-  must not contain any ``type of`` nor ``value of``.
+  Performs all the rewriting in the clause :n:`@goal_occurrences`.
 
 .. seealso::
 
@@ -3667,10 +3666,11 @@ automatically created.
    from the order in which they were inserted, making this implementation
    observationally different from the legacy one.
 
-The general command to add a hint to some databases :n:`{+ @ident}` is
-
 .. cmd:: Hint @hint_definition : {+ @ident}
 
+   The general command to add a hint to some databases :n:`{+ @ident}`.
+   The various possible :production:`hint_definition`\s are given below.
+
    .. cmdv:: Hint @hint_definition
 
       No database name is given: the hint is registered in the ``core`` database.
@@ -3719,7 +3719,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
       before, the tactic actually used is a restricted version of
       :tacn:`apply`).
 
-   .. cmdv:: Resolve <- @term
+   .. cmdv:: Hint Resolve <- @term
 
       Adds the right-to-left implication of an equivalence  as a hint.
 
@@ -3739,7 +3739,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
    .. exn:: @term cannot be used as a hint
       :undocumented:
 
-   .. cmdv:: Immediate {+ @term} : @ident
+   .. cmdv:: Hint Immediate {+ @term} : @ident
 
       Adds each :n:`Hint Immediate @term`.
 
@@ -4557,14 +4557,14 @@ Automating
    .. _btauto_grammar:
 
    .. productionlist:: sentence
-      t : `x`
-        : true
-        : false
-        : orb `t` `t`
-        : andb `t` `t`
-        : xorb `t` `t`
-        : negb `t`
-        : if `t` then `t` else `t`
+      btauto_term : `ident`
+                  : true
+                  : false
+                  : orb `btauto_term` `btauto_term`
+                  : andb `btauto_term` `btauto_term`
+                  : xorb `btauto_term` `btauto_term`
+                  : negb `btauto_term`
+                  : if `btauto_term` then `btauto_term` else `btauto_term`
 
    Whenever the formula supplied is not a tautology, it also provides a
    counter-example.
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index ffa727ff6c..c9e5247854 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -189,18 +189,13 @@ Requests to the environment
    This command displays the type of :n:`@term`. When called in proof mode, the
    term is checked in the local context of the current subgoal.
 
-
-   .. TODO : selector is not a syntax entry
-
    .. cmdv:: @selector: Check @term
 
       This variant specifies on which subgoal to perform typing
       (see Section :ref:`invocation-of-tactics`).
 
 
-.. TODO : convtactic is not a syntax entry
-
-.. cmd:: Eval @convtactic in @term
+.. cmd:: Eval @redexpr 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
@@ -1167,19 +1162,19 @@ described first.
       Print all the currently non-transparent strategies.
 
 
-.. cmd:: Declare Reduction @ident := @convtactic
+.. cmd:: Declare Reduction @ident := @redexpr
 
    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
+   instance ``lazy beta delta [foo bar]``. This short name can then be used
    in :n:`Eval @ident in` or ``eval`` directives. This command
    accepts the
-   Local modifier, for discarding this reduction name at the end of the
-   file or module. For the moment the name cannot be qualified. In
+   ``Local`` modifier, for discarding this reduction name at the end of the
+   file or module. For the moment, the name is not qualified. In
    particular declaring the same name in several modules or in several
-   functor applications will be refused if these declarations are not
+   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 to also perform a
-   :n:`Ltac @ident := @convtactic`.
+   :n:`Ltac @ident := @redexpr`.
 
    .. seealso:: :ref:`performingcomputations`
 
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 3710c0af9d..ee71368729 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -109,7 +109,7 @@ the associativity of disjunction and conjunction, so let us apply for instance a
 right associativity (which is the choice of Coq).
 
 Precedence levels and associativity rules of notations have to be
-given between parentheses in a list of modifiers that the :cmd:`Notation`
+given between parentheses in a list of :token:`modifiers` that the :cmd:`Notation`
 command understands. Here is how the previous examples refine.
 
 .. coqtop:: in
@@ -249,7 +249,7 @@ bar of the notation.
    Check (sig (fun x : nat => x=x)).
 
 The second, more powerful control on printing is by using the format
-modifier. Here is an example
+:token:`modifier`. Here is an example
 
 .. coqtop:: all
 
@@ -298,8 +298,8 @@ expression is performed at definition time. Type checking is done only
 at the time of use of the notation.
 
 .. note:: Sometimes, a notation is expected only for the parser. To do
-          so, the option ``only parsing`` is allowed in the list of modifiers
-          of :cmd:`Notation`. Conversely, the ``only printing`` modifier can be
+          so, the option ``only parsing`` is allowed in the list of :token:`modifiers`
+          of :cmd:`Notation`. Conversely, the ``only printing`` :token:`modifier` can be
           used to declare that a notation should only be used for printing and
           should not declare a parsing rule. In particular, such notations do
           not modify the parser.
@@ -310,11 +310,11 @@ The Infix command
 The :cmd:`Infix` command is a shortening for declaring notations of infix
 symbols.
 
-.. cmd:: Infix "@symbol" := @term ({+, @modifier}).
+.. cmd:: Infix "@symbol" := @term {? (@modifiers) }.
 
    This command is equivalent to
 
-       :n:`Notation "x @symbol y" := (@term x y) ({+, @modifier}).`
+       :n:`Notation "x @symbol y" := (@term x y) {? (@modifiers) }.`
 
    where ``x`` and ``y`` are fresh names. Here is an example.
 
@@ -437,7 +437,7 @@ application of the notation:
 
    Check sigma z : nat, z = 0.
 
-Notice the modifier ``x ident`` in the declaration of the
+Notice the :token:`modifier` ``x ident`` in the declaration of the
 notation. It tells to parse :g:`x` as a single identifier.
 
 Binders bound in the notation and parsed as patterns
@@ -457,7 +457,7 @@ binder. Here is an example:
 
    Check subset '(x,y), x+y=0.
 
-The modifier ``p pattern`` in the declaration of the notation tells to parse
+The :token:`modifier` ``p pattern`` in the declaration of the notation tells to parse
 :g:`p` as a pattern. Note that a single variable is both an identifier and a
 pattern, so, e.g., the following also works:
 
@@ -467,7 +467,7 @@ pattern, so, e.g., the following also works:
 
 If one wants to prevent such a notation to be used for printing when the
 pattern is reduced to a single identifier, one has to use instead
-the modifier ``p strict pattern``. For parsing, however, a
+the :token:`modifier` ``p strict pattern``. For parsing, however, a
 ``strict pattern`` will continue to include the case of a
 variable. Here is an example showing the difference:
 
@@ -507,7 +507,7 @@ that ``x`` is parsed as a term at level 99 (as done in the notation for
 :g:`sumbool`), but that this term has actually to be an identifier.
 
 The notation :g:`{ x | P }` is already defined in the standard
-library with the ``as ident`` modifier. We cannot redefine it but
+library with the ``as ident`` :token:`modifier`. We cannot redefine it but
 one can define an alternative notation, say :g:`{ p such that P }`,
 using instead ``as pattern``.
 
@@ -527,7 +527,7 @@ is just an identifier, one could have said
 ``p at level 99 as strict pattern``.
 
 Note also that in the absence of a ``as ident``, ``as strict pattern`` or
-``as pattern`` modifiers, the default is to consider sub-expressions occurring
+``as pattern`` :token:`modifier`\s, the default is to consider sub-expressions occurring
 in binding position and parsed as terms to be ``as ident``.
 
 .. _NotationsWithBinders:
@@ -628,7 +628,7 @@ except that in the iterator
 position of the binding variable of a ``fun`` or a ``forall``.
 
 To specify that the part “``x .. y``” of the notation parses a sequence of
-binders, ``x`` and ``y`` must be marked as ``binder`` in the list of modifiers
+binders, ``x`` and ``y`` must be marked as ``binder`` in the list of :token:`modifiers`
 of the notation. The binders of the parsed sequence are used to fill the
 occurrences of the first placeholder of the iterating pattern which is
 repeatedly nested as many times as the number of binders generated. If ever the
@@ -678,7 +678,7 @@ Predefined entries
 ~~~~~~~~~~~~~~~~~~
 
 By default, sub-expressions are parsed as terms and the corresponding
-grammar entry is called :n:`@constr`. However, one may sometimes want
+grammar entry is called ``constr``. However, one may sometimes want
 to restrict the syntax of terms in a notation. For instance, the
 following notation will accept to parse only global reference in
 position of :g:`x`:
@@ -866,16 +866,17 @@ notations are given below. The optional :production:`scope` is described in
 :ref:`Scopes`.
 
 .. productionlist:: coq
-   notation      : [Local] Notation `string` := `term` [`modifiers`] [: `scope`].
-                 : [Local] Infix `string` := `qualid` [`modifiers`] [: `scope`].
-                 : [Local] Reserved Notation `string` [`modifiers`] .
+   notation      : [Local] Notation `string` := `term` [(`modifiers`)] [: `scope`].
+                 : [Local] Infix `string` := `qualid` [(`modifiers`)] [: `scope`].
+                 : [Local] Reserved Notation `string` [(`modifiers`)] .
                  : Inductive `ind_body` [`decl_notation`] with … with `ind_body` [`decl_notation`].
                  : CoInductive `ind_body` [`decl_notation`] with … with `ind_body` [`decl_notation`].
                  : Fixpoint `fix_body` [`decl_notation`] with … with `fix_body` [`decl_notation`].
                  : CoFixpoint `cofix_body` [`decl_notation`] with … with `cofix_body` [`decl_notation`].
                  : [Local] Declare Custom Entry `ident`.
    decl_notation : [where `string` := `term` [: `scope`] and … and `string` := `term` [: `scope`]].
-   modifiers     : at level `num`
+   modifiers     : `modifier`, … , `modifier`
+   modifier      : at level `num`
                  : in custom `ident`
                  : in custom `ident` at level `num`
                  : `ident` , … , `ident` at level `num` [`binderinterp`]
@@ -1657,15 +1658,15 @@ Tactic notations allow to customize the syntax of tactics. They have the followi
    tacn                 : Tactic Notation [`tactic_level`] [`prod_item` … `prod_item`] := `tactic`.
    prod_item            : `string` | `tactic_argument_type`(`ident`)
    tactic_level         : (at level `num`)
-   tactic_argument_type : `ident` | `simple_intropattern` | `reference`
-                        : `hyp` | `hyp_list` | `ne_hyp_list`
-                        : `constr` | `uconstr` | `constr_list` | `ne_constr_list`
-                        : `integer` | `integer_list` | `ne_integer_list`
-                        : `int_or_var` | `int_or_var_list` | `ne_int_or_var_list`
-                        : `tactic` | `tactic0` | `tactic1` | `tactic2` | `tactic3`
-                        : `tactic4` | `tactic5`
-
-.. cmd:: Tactic Notation {? (at level @level)} {+ @prod_item} := @tactic.
+   tactic_argument_type : ident | simple_intropattern | reference
+                        : hyp | hyp_list | ne_hyp_list
+                        : constr | uconstr | constr_list | ne_constr_list
+                        : integer | integer_list | ne_integer_list
+                        : int_or_var | int_or_var_list | ne_int_or_var_list
+                        : tactic | tactic0 | tactic1 | tactic2 | tactic3
+                        : tactic4 | tactic5
+
+.. cmd:: Tactic Notation {? (at level @num)} {+ @prod_item} := @tactic.
 
    A tactic notation extends the parser and pretty-printer of tactics with a new
    rule made of the list of production items. It then evaluates into the