Define many undefined tokens, and other misc fixes.

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

6 files changed, 77 insertions, 77 deletions

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`