Convert Ltac chapter to prodn

21 files changed, 2001 insertions, 1260 deletions

diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index 5d257c7370..dafa510ade 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -44,7 +44,7 @@ Formally, the syntax of classes is defined as:
    .. prodn::
       class ::= Funclass
       | Sortclass
-      | @smart_qualid
+      | @reference
 
 
 
diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst
index f037fed394..479fa674f5 100644
--- a/doc/sphinx/addendum/ring.rst
+++ b/doc/sphinx/addendum/ring.rst
@@ -102,17 +102,17 @@ forget this paragraph and use the tactic according to your intuition.
 Concrete usage in Coq
 --------------------------
 
-.. tacv:: ring
+.. tacn:: ring {? [ {+ @term } ] }
 
-   This tactic solves equations upon polynomial expressions of a ring
+   Solves polynomical equations of a ring
    (or semiring) structure. It proceeds by normalizing both sides
    of the equation (w.r.t. associativity, commutativity and
    distributivity, constant propagation, rewriting of monomials) and
-   comparing syntactically the results.
+   syntactically comparing the results.
 
-.. tacv:: ring_simplify
+.. tacn:: ring_simplify {? [ {+ @term } ] } {+ @term } {? in @ident }
 
-   This tactic applies the normalization procedure described above to
+   Applies the normalization procedure described above to
    the given terms. The tactic then replaces all occurrences of the terms
    given in the conclusion of the goal by their normal forms. If no term
    is given, then the conclusion should be an equation and both
@@ -125,6 +125,10 @@ Concrete usage in Coq
    ``Require Import ZArithRing`` or simply ``Require Import ZArith``; for |N|, do
    ``Require Import NArithRing`` or ``Require Import NArith``.
 
+   All declared field structures can be printed with the :cmd:`Print Rings` command.
+
+   .. cmd:: Print Rings
+      :undocumented:
 
 .. example::
 
@@ -511,7 +515,7 @@ application of the main correctness theorem to well-chosen arguments.
 Dealing with fields
 ------------------------
 
-.. tacv:: field
+.. tacn:: field {? [ {+ @term } ] }
 
    This tactic is an extension of the :tacn:`ring` tactic that deals with rational
    expressions. Given a rational expression :math:`F = 0`. It first reduces the
@@ -568,7 +572,7 @@ Dealing with fields
    Rewriting works with the equality  :g:`m = p` only if :g:`p` is a polynomial since
    rewriting is handled by the underlying ring tactic.
 
-.. tacv:: field_simplify
+.. tacn:: field_simplify {? [ {+ @term } ] } {+ @term } {? in @ident }
  
    performs the simplification in the conclusion of the
    goal, :math:`F_1 = F_2` becomes :math:`N_1 / D_1 = N_2 / D_2`. A normalization step
@@ -602,7 +606,7 @@ Dealing with fields
    assumption :token:`ident` using the
    equalities defined by the :token:`term`\s inside the brackets.
 
-.. tacv:: field_simplify_eq
+.. tacn:: field_simplify_eq {? [ {+ @term } ] } {? in @ident }
 
    performs the simplification in the conclusion of
    the goal removing the denominator. :math:`F_1 = F_2` becomes :math:`N_1 D_2 = N_2 D_1`.
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index b2b68482ef..f9d24fde0e 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -34,7 +34,7 @@ The prelude
 This section lists the basic notions and results which are directly
 available in the standard |Coq| system. Most of these constructions
 are defined in the ``Prelude`` module in directory ``theories/Init``
-at the |Coq| root directory; this includes the modules
+in the |Coq| root directory; this includes the modules
 ``Notations``,
 ``Logic``,
 ``Datatypes``,
diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst
index 8918e87180..d7f7259ab0 100644
--- a/doc/sphinx/language/core/basic.rst
+++ b/doc/sphinx/language/core/basic.rst
@@ -57,7 +57,7 @@ appending the level to the nonterminal name (as in :n:`@term100` or
 
    |Coq| uses an extensible parser.  Plugins and the :ref:`notation
    system <syntax-extensions-and-notation-scopes>` can extend the
-   syntax at run time.  Some notations are defined in the prelude,
+   syntax at run time.  Some notations are defined in the :term:`prelude`,
    which is loaded by default.  The documented grammar doesn't include
    these notations.  Precedence levels not used by the base grammar
    are omitted from the documentation, even though they could still be
@@ -119,21 +119,19 @@ Numerals
   integer.  Underscores embedded in the digits are ignored, for example
   ``1_000_000`` is the same as ``1000000``.
 
-  .. insertprodn numeral digit
+  .. insertprodn numeral hexdigit
 
   .. prodn::
-     digit ::= 0 .. 9
-     digitu ::= {| @digit | _ }
-     hexdigit ::= {| 0 .. 9 | a..f | A..F }
-     hexdigitu ::= {| @hexdigit | _ }
-     decnum ::= @digit {* @digitu }
-     hexnum ::= {| 0x | 0X } @hexdigit {* @hexdigitu }
-     num ::= {| @decnum | @hexnum }
-     sign ::= {| + | - }
+     numeral ::= {? - } @decnum {? . {+ {| @digit | _ } } } {? {| e | E } {? {| + | - } } @decnum }
+     | {? - } @hexnum {? . {+ {| @hexdigit | _ } } } {? {| p | P } {? {| + | - } } @decnum }
      int ::= {? - } @num
-     decimal ::= @decnum {? . {+ @digitu } } {? {| e | E } {? @sign } @decnum }
-     hexadecimal ::= @hexnum {? . {+ @hexdigitu } } {? {| p | P } {? @sign } @decnum }
-     numeral ::= {? - } {| @decimal | @hexadecimal }
+     num ::= {| @decnum | @hexnum }
+     decnum ::= @digit {* {| @digit | _ } }
+     digit ::= 0 .. 9
+     hexnum ::= {| 0x | 0X } @hexdigit {* {| @hexdigit | _ } }
+     hexdigit ::= {| 0 .. 9 | a .. f | A .. F }
+
+  .. todo PR need some code fixes for hex, see PR 11948
 
 Strings
   Strings begin and end with ``"`` (double quote).  Use ``""`` to represent
@@ -294,7 +292,7 @@ rest of the |Coq| manual: :term:`terms <term>` and :term:`types
         document ::= {* @sentence }
         sentence ::= {? @attributes } @command .
         | {? @attributes } {? @num : } @query_command .
-        | {? @attributes } {? @toplevel_selector } @ltac_expr {| . | ... }
+        | {? @attributes } {? @toplevel_selector : } @ltac_expr {| . | ... }
         | @control_command
 
      :n:`@ltac_expr` syntax supports both simple and compound
diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst
index 0e637e5aa3..42203d9d65 100644
--- a/doc/sphinx/language/core/definitions.rst
+++ b/doc/sphinx/language/core/definitions.rst
@@ -34,18 +34,18 @@ Type cast
 .. insertprodn term_cast term_cast
 
 .. prodn::
-   term_cast ::= @term10 <: @term
-   | @term10 <<: @term
-   | @term10 : @term
+   term_cast ::= @term10 <: @type
+   | @term10 <<: @type
+   | @term10 : @type
    | @term10 :>
 
-The expression :n:`@term : @type` is a type cast expression. It enforces
-the type of :n:`@term` to be :n:`@type`.
+The expression :n:`@term10 : @type` is a type cast expression. It enforces
+the type of :n:`@term10` to be :n:`@type`.
 
-:n:`@term <: @type` locally sets up the virtual machine for checking that
-:n:`@term` has type :n:`@type`.
+:n:`@term10 <: @type` locally sets up the virtual machine for checking that
+:n:`@term10` has type :n:`@type`.
 
-:n:`@term <<: @type` uses native compilation for checking that :n:`@term`
+:n:`@term10 <<: @type` uses native compilation for checking that :n:`@term10`
 has type :n:`@type`.
 
 .. _gallina-definitions:
diff --git a/doc/sphinx/language/core/variants.rst b/doc/sphinx/language/core/variants.rst
index 6d4676b3c4..d00a2f4100 100644
--- a/doc/sphinx/language/core/variants.rst
+++ b/doc/sphinx/language/core/variants.rst
@@ -52,7 +52,7 @@ Private (matching) inductive types
 
 .. index:: match ... with ...
 
-.. _match:
+.. _match_term:
 
 Definition by cases: match
 --------------------------
diff --git a/doc/sphinx/language/extensions/arguments-command.rst b/doc/sphinx/language/extensions/arguments-command.rst
index 613669c34b..0ae9fab7ab 100644
--- a/doc/sphinx/language/extensions/arguments-command.rst
+++ b/doc/sphinx/language/extensions/arguments-command.rst
@@ -3,7 +3,7 @@
 Setting properties of a function's arguments
 ++++++++++++++++++++++++++++++++++++++++++++
 
-.. cmd:: Arguments @smart_qualid {* @arg_specs } {* , {* @implicits_alt } } {? : {+, @args_modifier } }
+.. cmd:: Arguments @reference {* @arg_specs } {* , {* @implicits_alt } } {? : {+, @args_modifier } }
    :name: Arguments
 
    .. insertprodn argument_spec args_modifier
@@ -37,7 +37,7 @@ Setting properties of a function's arguments
    extensions into the core language used by the kernel).  The command's effects include:
 
    * Making arguments implicit. Afterward, implicit arguments
-     must be omitted in any expression that applies :token:`smart_qualid`.
+     must be omitted in any expression that applies :token:`reference`.
    * Declaring that some arguments of a given function should
      be interpreted in a given scope.
    * Affecting when the :tacn:`simpl` and :tacn:`cbn` tactics unfold the function.
@@ -82,7 +82,7 @@ Setting properties of a function's arguments
          evaulate to constructors.  See :ref:`Args_effect_on_unfolding`.
 
       :n:`@name {? % @scope }`
-         a *formal parameter* of the function :n:`@smart_qualid` (i.e.
+         a *formal parameter* of the function :n:`@reference` (i.e.
          the parameter name used in the function definition).  Unless `rename` is specified,
          the list of :n:`@name`\s must be a prefix of the formal parameters, including all implicit
          arguments.  `_` can be used to skip over a formal parameter.
@@ -103,15 +103,15 @@ Setting properties of a function's arguments
             :undocumented:
 
       `clear scopes`
-         clears argument scopes of :n:`@smart_qualid`
+         clears argument scopes of :n:`@reference`
       `extra scopes`
          defines extra argument scopes, to be used in case of coercion to ``Funclass``
          (see :ref:`coercions`) or with a computed type.
       `simpl nomatch`
-         prevents performing a simplification step for :n:`@smart_qualid`
+         prevents performing a simplification step for :n:`@reference`
          that would expose a match construct in the head position.  See :ref:`Args_effect_on_unfolding`.
       `simpl never`
-         prevents performing a simplification step for :n:`@smart_qualid`.  See :ref:`Args_effect_on_unfolding`.
+         prevents performing a simplification step for :n:`@reference`.  See :ref:`Args_effect_on_unfolding`.
 
       `clear bidirectionality hint`
          removes the bidirectionality hint, the `&`
@@ -130,7 +130,7 @@ Setting properties of a function's arguments
          .. todo the above feature seems a bit unnatural and doesn't play well with partial
             application.  See https://github.com/coq/coq/pull/11718#discussion_r408841762
 
-   Use :cmd:`About` to view the current implicit arguments setting for a :token:`smart_qualid`.
+   Use :cmd:`About` to view the current implicit arguments setting for a :token:`reference`.
 
    Or use the :cmd:`Print Implicit` command to see the implicit arguments
    of an object (see :ref:`displaying-implicit-args`).
@@ -268,7 +268,7 @@ Binding arguments to a scope
 
          Arguments plus_fct (f1 f2)%F x%R.
 
-   When interpreting a term, if some of the arguments of :token:`smart_qualid` are built
+   When interpreting a term, if some of the arguments of :token:`reference` are built
    from a notation, then this notation is interpreted in the scope stack
    extended by the scope bound (if any) to this argument. The effect of
    the scope is limited to the argument itself. It does not propagate to
diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst
index f55f3c5495..bfda8befff 100644
--- a/doc/sphinx/language/extensions/canonical.rst
+++ b/doc/sphinx/language/extensions/canonical.rst
@@ -27,11 +27,11 @@ applied to an unknown structure instance (an implicit argument) and a
 value. The complete documentation of canonical structures can be found
 in :ref:`canonicalstructures`; here only a simple example is given.
 
-.. cmd:: Canonical {? Structure } @smart_qualid
+.. cmd:: Canonical {? Structure } @reference
          Canonical {? Structure } @ident_decl @def_body
    :name: Canonical Structure; _
 
-   The first form of this command declares an existing :n:`@smart_qualid` as a
+   The first form of this command declares an existing :n:`@reference` as a
    canonical instance of a structure (a record).
 
    The second form defines a new constant as if the :cmd:`Definition` command
@@ -111,7 +111,7 @@ in :ref:`canonicalstructures`; here only a simple example is given.
    It is equivalent to having a :cmd:`Canonical Structure` declaration just
    after the command.
 
-.. cmd:: Print Canonical Projections {* @smart_qualid }
+.. cmd:: Print Canonical Projections {* @reference }
 
    This displays the list of global names that are components of some
    canonical structure. For each of them, the canonical structure of
diff --git a/doc/sphinx/language/extensions/implicit-arguments.rst b/doc/sphinx/language/extensions/implicit-arguments.rst
index b4f7fe0846..bbd486e3ba 100644
--- a/doc/sphinx/language/extensions/implicit-arguments.rst
+++ b/doc/sphinx/language/extensions/implicit-arguments.rst
@@ -373,7 +373,7 @@ the hiding of implicit arguments for a single function application using the
 Displaying implicit arguments
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmd:: Print Implicit @smart_qualid
+.. cmd:: Print Implicit @reference
 
    Displays the implicit arguments associated with an object,
    identifying which arguments are applied maximally or not.
diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst
index 028d0aaf57..b4558ef07f 100644
--- a/doc/sphinx/language/extensions/match.rst
+++ b/doc/sphinx/language/extensions/match.rst
@@ -289,7 +289,7 @@ This example emphasizes what the printing settings offer.
 Patterns
 --------
 
-The full syntax of `match` is presented in :ref:`match`.
+The full syntax of `match` is presented in :ref:`match_term`.
 Identifiers in patterns are either constructor names or variables. Any
 identifier that is not the constructor of an inductive or co-inductive
 type is considered to be a variable. A variable name cannot occur more
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index d4ceffac9f..058b8ccd5c 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -177,8 +177,8 @@ and ``coqtop``, unless stated otherwise:
      the command-line.
 
 :-rfrom *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid`.
-  This is equivalent to running :cmd:`From <From ... Require>`
-  :n:`@dirpath` :cmd:`Require <From ... Require>` :n:`@qualid`.
+  This is equivalent to running :cmd:`From <From … Require>`
+  :n:`@dirpath` :cmd:`Require <From … Require>` :n:`@qualid`.
   See the :ref:`note above <interleave-command-line>` regarding the order
   of command-line options.
 :-ri *qualid*, -require-import *qualid*: Load |Coq| compiled library :n:`@qualid` and import it.
@@ -191,14 +191,14 @@ and ``coqtop``, unless stated otherwise:
   of command-line options.
 :-rifrom *dirpath* *qualid*, -require-import-from *dirpath* *qualid*:
   Load |Coq| compiled library :n:`@qualid` and import it.  This is
-  equivalent to running :cmd:`From <From ... Require>` :n:`@dirpath`
-  :cmd:`Require Import <From ... Require>` :n:`@qualid`.  See the
+  equivalent to running :cmd:`From <From … Require>` :n:`@dirpath`
+  :cmd:`Require Import <From … Require>` :n:`@qualid`.  See the
   :ref:`note above <interleave-command-line>` regarding the order of
   command-line options.
 :-refrom *dirpath* *qualid*, -require-export-from *dirpath* *qualid*:
   Load |Coq| compiled library :n:`@qualid` and transitively import it.
-  This is equivalent to running :cmd:`From <From ... Require>`
-  :n:`@dirpath` :cmd:`Require Export <From ... Require>` :n:`@qualid`.
+  This is equivalent to running :cmd:`From <From … Require>`
+  :n:`@dirpath` :cmd:`Require Export <From … Require>` :n:`@qualid`.
   See the :ref:`note above <interleave-command-line>` regarding the
   order of command-line options.
 :-batch: Exit just after argument parsing. Available for ``coqtop`` only.
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index a21f7e545c..b0b0367d6d 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -5,14 +5,15 @@ Ltac
 
 This chapter documents the tactic language |Ltac|.
 
-We start by giving the syntax, and next, we present the informal
+We start by giving the syntax followed by the informal
 semantics. To learn more about the language and
 especially about its foundations, please refer to :cite:`Del00`.
+(Note the examples in the paper won't work as-is; Coq has evolved
+since the paper was written.)
 
 .. example:: Basic tactic macros
 
-   Here are some examples of simple tactic macros that the
-   language lets you write.
+   Here are some examples of simple tactic macros you can create with |Ltac|:
 
    .. coqdoc::
 
@@ -29,151 +30,208 @@ Syntax
 ------
 
 The syntax of the tactic language is given below.
-Various already defined entries will be used in this
-chapter: entries :token:`num`, :token:`int`, :token:`ident`
-:token:`qualid`, :token:`term`, :token:`cpattern` and :token:`tactic`
-represent respectively natural and integer numbers,
-identifiers, qualified names, Coq terms, patterns and the atomic
-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 :n:`?@ident`. The
-notation :g:`_` can also be used to denote metavariable whose instance is
-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 :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:`@ltac_expr`. This language is used in proof
-mode but it can also be used in toplevel definitions as shown below.
+
+The main entry of the grammar is :n:`@ltac_expr`, which is used in proof mode
+as well as to define new tactics with the :cmd:`Ltac` command.
+
+The grammar uses multiple :n:`ltac_expr*` nonterminals to express how subexpressions
+are grouped when they're not fully parenthesized.  For example, in many programming
+languages, `a*b+c` is interpreted as `(a*b)+c` because `*` has
+higher precedence than `+`.  Usually `a/b/c` is given the :gdef:`left associative`
+interpretation `(a/b)/c` rather than the :gdef:`right associative` interpretation
+`a/(b/c)`.
+
+In Coq, the expression :n:`try repeat @tactic__1 || @tactic__2; @tactic__3; @tactic__4`
+is interpreted as :n:`(try (repeat (@tactic__1 || @tactic__2)); @tactic__3); @tactic__4`
+because `||` is part of :token:`ltac_expr2`, which has higher precedence than
+:tacn:`try` and :tacn:`repeat` (at the level of :token:`ltac_expr3`), which
+in turn have higher precedence than `;`, which is part of :token:`ltac_expr4`.
+(A *lower* number in the nonterminal name means *higher* precedence in this grammar.)
+
+The constructs in :token:`ltac_expr` are :term:`left associative`.
+
+.. insertprodn ltac_expr tactic_atom
+
+.. prodn::
+   ltac_expr ::= {| @ltac_expr4 | @binder_tactic }
+   ltac_expr4 ::= @ltac_expr3 ; {| @ltac_expr3 | @binder_tactic }
+   | @ltac_expr3 ; [ @for_each_goal ]
+   | @ltac_expr3
+   ltac_expr3 ::= @l3_tactic
+   | @ltac_expr2
+   ltac_expr2 ::= @ltac_expr1 + {| @ltac_expr2 | @binder_tactic }
+   | @ltac_expr1 || {| @ltac_expr2 | @binder_tactic }
+   | @l2_tactic
+   | @ltac_expr1
+   ltac_expr1 ::= @tactic_value
+   | @qualid {+ @tactic_arg }
+   | @l1_tactic
+   | @ltac_expr0
+   tactic_value ::= {| @value_tactic | @syn_value }
+   tactic_arg ::= @tactic_value
+   | @term
+   | ()
+   ltac_expr0 ::= ( @ltac_expr )
+   | [> @for_each_goal ]
+   | @tactic_atom
+   tactic_atom ::= @int
+   | @qualid
+   | ()
+
+.. todo For the moment, I've left the language constructs like +, || and ; unchanged in the grammar.
+   Not sure what to do with them.  If we just make these indirections I think the grammar no longer
+   gives you an overall idea of the concrete grammar without following the hyperlinks for many terms--not so easy
+   (e.g. I have a construct and I want to figure out which productions generate it so I can read about them).
+   We should think about eventually having a cheat sheet for the constructs, perhaps as part of the
+   chapter introduction (use case: I know there's a construct but I can't remember its syntax).  They
+   do show up in the index but they're not so easy to find.  I had thought a little about putting
+   an ltac expression cheat sheet at the top of the tactics index.  Unconventional, but people would
+   see it and remember how to find it.
+
+   OTOH, as you rightly note, they are not really tactics.  Looking for better ideas that we are OK with.
+
+.. note::
+
+   Tactics described in other chapters of the documentation are :production:`simple_tactic`\s,
+   which only modify the proof state.  |Ltac| provides additional constructs that can generally
+   be used wherever a :token:`simple_tactic` can appear, even though they don't modify the proof
+   state and that syntactically they're at
+   varying levels in :token:`ltac_expr`.  For simplicity of presentation, the |Ltac| constructs
+   are documented as tactics.  Tactics are grouped as follows:
+
+   - :production:`binder_tactic`\s are: :tacn:`fun` and :tacn:`let`
+   - :production:`l3_tactic`\s include |Ltac| tactics: :tacn:`try`,
+     :tacn:`do`, :tacn:`repeat`, :tacn:`timeout`, :tacn:`time`, :tacn:`progress`, :tacn:`once`,
+     :tacn:`exactly_once`, :tacn:`only` and :tacn:`abstract`
+   - :production:`l2_tactic`\s are: :tacn:`tryif`
+   - :production:`l1_tactic`\s are the :token:`simple_tactic`\s, :tacn:`first`, :tacn:`solve`,
+     :tacn:`idtac`, :tacn:`fail` and
+     :tacn:`gfail` as well as :tacn:`match`, :tacn:`match goal` and their :n:`lazymatch` and
+     :n:`multimatch` variants.
+   - :production:`value_tactic`\s, which return values rather than change the proof state.
+     They are: :tacn:`eval`, :tacn:`context`, :tacn:`numgoals`, :tacn:`fresh`, :tacn:`type of`
+     and :tacn:`type_term`.
+
+   The documentation for these |Ltac| constructs mentions which group they belong to.
+
+   The difference is only relevant in some compound tactics where
+   extra parentheses may be needed.  For example, parenthesees are required in
+   :n:`idtac + (once idtac)` because :tacn:`once` is an :token:`l3_tactic`, which the
+   production :n:`@ltac_expr2 ::= @ltac_expr1 + {| @ltac_expr2 | @binder_tactic }` doesn't
+   accept after the `+`.
 
 .. note::
 
    - The grammar reserves the token ``||``.
 
-   - The infix tacticals  ``… || …`` ,  ``… + …`` , and  ``… ; …``  are associative.
-
-     .. example::
-
-        If you want that :n:`@tactic__2; @tactic__3` be fully run on the first
-        subgoal generated by :n:`@tactic__1`, before running on the other
-        subgoals, then you should not write
-        :n:`@tactic__1; (@tactic__2; @tactic__3)` but rather
-        :n:`@tactic__1; [> @tactic__2; @tactic__3 .. ]`.
-
-   - In :token:`tacarg`, there is an overlap between :token:`qualid` as a
-     direct tactic argument and :token:`qualid` as a particular case of
-     :token:`term`. The resolution is done by first looking for a reference
-     of the tactic language and if it fails, for a reference to a term.
-     To force the resolution as a reference of the tactic language, use the
-     form :n:`ltac:(@qualid)`. To force the resolution as a reference to a
-     term, use the syntax :n:`(@qualid)`.
-
-   - As shown by the figure, tactical  ``… || …``  binds more than the prefix
-     tacticals :tacn:`try`, :tacn:`repeat`, :tacn:`do` and :tacn:`abstract`
-     which themselves bind more than the postfix tactical  ``… ;[ … ]`` 
-     which binds at the same level as  ``… ; …`` .
-
-     .. example::
-
-        :n:`try repeat @tactic__1 || @tactic__2; @tactic__3; [ {+| @tactic } ]; @tactic__4`
-
-        is understood as:
-
-        :n:`((try (repeat (@tactic__1 || @tactic__2)); @tactic__3); [ {+| @tactic } ]); @tactic__4`
-
-.. productionlist::  coq
-   ltac_expr         : `ltac_expr` ; `ltac_expr`
-                     : [> `ltac_expr` | ... | `ltac_expr` ]
-                     : `ltac_expr` ; [ `ltac_expr` | ... | `ltac_expr` ]
-                     : `ltac_expr3`
-   ltac_expr3        : do (`natural` | `ident`) `ltac_expr3`
-                     : progress `ltac_expr3`
-                     : repeat `ltac_expr3`
-                     : try `ltac_expr3`
-                     : once `ltac_expr3`
-                     : exactly_once `ltac_expr3`
-                     : timeout (`natural` | `ident`) `ltac_expr3`
-                     : time [`string`] `ltac_expr3`
-                     : only `selector`: `ltac_expr3`
-                     : `ltac_expr2`
-   ltac_expr2        : `ltac_expr1` || `ltac_expr3`
-                     : `ltac_expr1` + `ltac_expr3`
-                     : tryif `ltac_expr1` then `ltac_expr1` else `ltac_expr1`
-                     : `ltac_expr1`
-   ltac_expr1        : fun `name` ... `name` => `atom`
-                     : let [rec] `let_clause` with ... with `let_clause` in `atom`
-                     : match goal with `context_rule` | ... | `context_rule` end
-                     : match reverse goal with `context_rule` | ... | `context_rule` end
-                     : match `ltac_expr` with `match_rule` | ... | `match_rule` end
-                     : lazymatch goal with `context_rule` | ... | `context_rule` end
-                     : lazymatch reverse goal with `context_rule` | ... | `context_rule` end
-                     : lazymatch `ltac_expr` with `match_rule` | ... | `match_rule` end
-                     : multimatch goal with `context_rule` | ... | `context_rule` end
-                     : multimatch reverse goal with `context_rule` | ... | `context_rule` end
-                     : multimatch `ltac_expr` with `match_rule` | ... | `match_rule` end
-                     : abstract `atom`
-                     : abstract `atom` using `ident`
-                     : first [ `ltac_expr` | ... | `ltac_expr` ]
-                     : solve [ `ltac_expr` | ... | `ltac_expr` ]
-                     : idtac [ `message_token` ... `message_token`]
-                     : fail [`natural`] [`message_token` ... `message_token`]
-                     : gfail [`natural`] [`message_token` ... `message_token`]
-                     : fresh [ `component` … `component` ]
-                     : context `ident` [`term`]
-                     : eval `red_expr` in `term`
-                     : type of `term`
-                     : constr : `term`
-                     : uconstr : `term`
-                     : type_term `term`
-                     : numgoals
-                     : guard `test`
-                     : assert_fails `ltac_expr3`
-                     : assert_succeeds `ltac_expr3`
-                     : `tactic`
-                     : `qualid` `tacarg` ... `tacarg`
-                     : `atom`
-   atom              : `qualid`
-                     : ()
-                     : `int`
-                     : ( `ltac_expr` )
-   component : `string` | `qualid`
-   message_token     : `string` | `ident` | `int`
-   tacarg            : `qualid`
-                     : ()
-                     : ltac : `atom`
-                     : `term`
-   let_clause        : `ident` [`name` ... `name`] := `ltac_expr`
-   context_rule      : `context_hyp`, ..., `context_hyp` |- `cpattern` => `ltac_expr`
-                     : `cpattern` => `ltac_expr`
-                     : |- `cpattern` => `ltac_expr`
-                     : _ => `ltac_expr`
-   context_hyp       : `name` : `cpattern`
-                     : `name` := `cpattern` [: `cpattern`]
-   match_rule        : `cpattern` => `ltac_expr`
-                     : context [`ident`] [ `cpattern` ] => `ltac_expr`
-                     : _ => `ltac_expr`
-   test              : `int` = `int`
-                     : `int` (< | <= | > | >=) `int`
-   selector          : [`ident`]
-                     : `int`
-                     : (`int` | `int` - `int`), ..., (`int` | `int` - `int`)
-   toplevel_selector : `selector`
-                     : all
-                     : par
-                     : !
-
-.. productionlist:: coq
-   top              : [Local] Ltac `ltac_def` with ... with `ltac_def`
-   ltac_def         : `ident` [`ident` ... `ident`] := `ltac_expr`
-                    : `qualid` [`ident` ... `ident`] ::= `ltac_expr`
+.. _ltac-semantics:
+
+Semantics
+---------
+
+.. todo For the compound tactics, review all the descriptions of evaluation vs application,
+   backtracking, etc. to get the language consistent and simple (refactoring so the common
+   elements are described in one place)
+
+Types of values
+~~~~~~~~~~~~~~~
+
+An |Ltac| value can be a tactic, integer, string, unit (written as "`()`" ) or syntactic value.
+Syntactic values correspond to certain nonterminal symbols in the grammar,
+each of which is a distinct type of value.
+Most commonly, the value of an |Ltac| expression is a tactic that can be executed.
+
+While there are a number of constructs that let you combine multiple tactics into
+compound tactics, there are no operations for combining most other types of values.
+For example, there's no function to add two integers.  Syntactic values are entered
+with the :token:`syn_value` construct.  Values of all types can be assigned to toplevel
+symbols with the :cmd:`Ltac` command or to local symbols with the :tacn:`let` tactic.
+|Ltac| :tacn:`functions<fun>` can return values of any type.
+
+.. todo: there are 36 subsections under "Semantics", which seems like far too many
+
+Syntactic values
+~~~~~~~~~~~~~~~~
+
+.. insertprodn syn_value syn_value
+
+.. prodn::
+   syn_value ::= @ident : ( @nonterminal )
+
+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".
+
+   :token:`ident`
+      name of a grammar nonterminal listed in the table
+
+   :production:`nonterminal`
+      represents syntax described by :token:`nonterminal`.
+
+   .. list-table::
+      :header-rows: 1
+
+      * -  Specified :token:`ident`
+        - Parsed as
+        - Interpreted as
+        - as in tactic
+
+      * - ``ident``
+        - :token:`ident`
+        - a user-specified name
+        - :tacn:`intro`
+
+      * - ``string``
+        - :token:`string`
+        - a string
+        -
+
+      * - ``integer``
+        - :token:`int`
+        - an integer
+        -
+
+      * - ``reference``
+        - :token:`qualid`
+        - a qualified identifier
+        -
+
+      * - ``uconstr``
+        - :token:`term`
+        - an untyped term
+        - :tacn:`refine`
+
+      * - ``constr``
+        - :token:`term`
+        - a term
+        - :tacn:`exact`
+
+      * - ``ltac``
+        - :token:`ltac_expr`
+        - a tactic
+        -
+
+:n:`ltac:(@ltac_expr)` can be used to indicate that the parenthesized item
+should be interpreted as a tactic and not as a term.  The constructs can also
+be used to pass parameters to tactics written in OCaml.  (While all
+of the :token:`syn_value`\s can appear at the beginning of an :token:`ltac_expr`,
+the others are not useful because they will not evaluate to tactics.)
+
+:n:`uconstr:(@term)` can be used to build untyped terms.
+Terms built in |Ltac| are well-typed by default.  Building large
+terms in recursive |Ltac| functions may give very slow behavior because
+terms must be fully type checked at each step.  In this case, using
+an untyped term may avoid most of the repetitive type checking for the term,
+improving performance.
+
+.. todo above: maybe elaborate on "well-typed by default"
+   see https://github.com/coq/coq/pull/12103#discussion_r436317558
+
+Untyped terms built using :n:`uconstr:(…)` can be used as arguments to the
+:tacn:`refine` tactic, for example. In that case the untyped term is type
+checked against the conclusion of the goal, and the holes which are not solved
+by the typing procedure are turned into new subgoals.
 
 Tactics in terms
 ~~~~~~~~~~~~~~~~
@@ -183,84 +241,116 @@ Tactics in terms
 .. prodn::
    term_ltac ::= ltac : ( @ltac_expr )
 
-.. _ltac-semantics:
+Allows including an :token:`ltac_expr` within a term.  Semantically,
+it's the same as the :token:`syn_value` for `ltac`, but these are
+distinct in the grammar.
 
-Semantics
----------
+Substitution
+~~~~~~~~~~~~
+
+.. todo next paragraph: we need a better discussion of substitution.
+   Looks like that also applies to binder_tactics in some form.
+   See https://github.com/coq/coq/pull/12103#discussion_r422105218
+
+:token:`name`\s within |Ltac| expressions are used to represent both terms and
+|Ltac| variables.  If the :token:`name` corresponds to
+an |Ltac| variable or tactic name, |Ltac| substitutes the value before applying
+the expression.  Generally it's best to choose distinctive names for |Ltac| variables
+that won't clash with term names.  You can use :n:`ltac:(@name)` or :n:`(@name)`
+to control whether a :token:`name` is interpreted as, respectively, an |Ltac|
+variable or a term.
+
+Note that values from toplevel symbols, unlike locally-defined symbols, are
+substituted only when they appear at the beginning of an :token:`ltac_expr` or
+as a :token:`tactic_arg`.  Local symbols are also substituted into tactics:
 
-Tactic expressions can only be applied in the context of a proof. The
-evaluation yields either a term, an integer or a tactic. Intermediate
-results can be terms or integers but the final result must be a tactic
-which is then applied to the focused goals.
+.. example:: Substitution of global and local symbols
 
-There is a special case for ``match goal`` expressions of which the clauses
-evaluate to tactics. Such expressions can only be used as end result of
-a tactic expression (never as argument of a non-recursive local
-definition or of an application).
+   .. coqtop:: reset none
 
-The rest of this section explains the semantics of every construction of
-|Ltac|.
+      Goal True.
 
-Sequence
-~~~~~~~~
+   .. coqtop:: all
+
+      Ltac n := 1.
+      let n2 := n in idtac n2.
+      Fail idtac n.
+
+Sequence: ;
+~~~~~~~~~~~
 
 A sequence is an expression of the following form:
 
-.. tacn:: @ltac_expr__1 ; @ltac_expr__2
+.. tacn:: @ltac_expr3__1 ; {| @ltac_expr3__2 | @binder_tactic }
    :name: ltac-seq
 
-   The expression :n:`@ltac_expr__1` is evaluated to :n:`v__1`, which must be
-   a tactic value. The tactic :n:`v__1` is applied to the current goal,
-   possibly producing more goals. Then :n:`@ltac_expr__2` is evaluated to
+   The expression :n:`@ltac_expr3__1` is evaluated to :n:`v__1`, which must be
+   a tactic value. The tactic :n:`v__1` is applied to the current goals,
+   possibly producing more goals. Then the right-hand side is evaluated to
    produce :n:`v__2`, which must be a tactic value. The tactic
    :n:`v__2` is applied to all the goals produced by the prior
    application. Sequence is associative.
 
-Local application of tactics
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+   .. todo I don't see the distinction between evaluating an ltac expression
+      and applying it--how are they not the same thing?  If different, the
+      "Semantics" section above should explain it.
+      See https://github.com/coq/coq/pull/12103#discussion_r422210482
 
-Different tactics can be applied to the different goals using the
-following form:
+   .. note::
 
-.. tacn:: [> {*| @ltac_expr }]
-   :name: [> ... | ... | ... ] (dispatch)
+      - If you want :n:`@tactic__2; @tactic__3` to be fully applied to the first
+        subgoal generated by :n:`@tactic__1` before applying it to the other
+        subgoals, then you should write:
 
-   The expressions :n:`@ltac_expr__i` are evaluated to :n:`v__i`, for
-   i = 1, ..., n and all have to be tactics. The :n:`v__i` is applied to the
-   i-th goal, for i = 1, ..., n. It fails if the number of focused goals is not
-   exactly n.
+        - :n:`@tactic__1; [> @tactic__2; @tactic__3 .. ]` rather than
 
-   .. note::
+        - :n:`@tactic__1; (@tactic__2; @tactic__3)`.
 
-      If no tactic is given for the i-th goal, it behaves as if the tactic idtac
-      were given. For instance, ``[> | auto]`` is a shortcut for ``[> idtac | auto
-      ]``.
+Local application of tactics: [> ... ]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-   .. tacv:: [> {*| @ltac_expr__i} | @ltac_expr .. | {*| @ltac_expr__j}]
+.. tacn:: [> @for_each_goal ]
+   :name: [> … | … | … ] (dispatch)
 
-      In this variant, :n:`@ltac_expr` is used for each goal coming after those
-      covered by the list of :n:`@ltac_expr__i` but before those covered by the
-      list of :n:`@ltac_expr__j`.
+   .. insertprodn for_each_goal goal_tactics
 
-   .. tacv:: [> {*| @ltac_expr} | .. | {*| @ltac_expr}]
+   .. prodn::
+      for_each_goal ::= @goal_tactics
+      | {? @goal_tactics %| } {? @ltac_expr } .. {? %| @goal_tactics }
+      goal_tactics ::= {*| {? @ltac_expr } }
 
-      In this variant, idtac is used for the goals not covered by the two lists of
-      :n:`@ltac_expr`.
+   Applies a different :n:`{? @ltac_expr }` to each of the focused goals.  In the first
+   form of :token:`for_each_goal` (without `..`), the construct fails if the number of specified
+   :n:`{? @ltac_expr }` is not the same as the number of focused goals.  Omitting an
+   :n:`@ltac_expr` leaves the corresponding goal unchanged.
 
-   .. tacv:: [> @ltac_expr .. ]
+   In the second form (with :n:`{? @ltac_expr } ..`), the left and right :token:`goal_tactics`
+   are applied respectively to a prefix or suffix of the list of focused goals.
+   The :n:`{? @ltac_expr }` before the `..` is applied to any focused goals in the middle
+   (possibly none) that are not covered by the :token:`goal_tactics`.  The number of
+   :n:`{? @ltac_expr }` in the :token:`goal_tactics` must be no more than the number of
+   focused goals.
 
-      In this variant, the tactic :n:`@ltac_expr` is applied independently to each of
+   In particular:
+
+   :n:`@goal_tactics | .. | @goal_tactics`
+      The goals not covered by the two :token:`goal_tactics` are left unchanged.
+
+   :n:`[> @ltac_expr .. ]`
+      :n:`@ltac_expr` is applied independently to each of
       the goals, rather than globally. In particular, if there are no goals, the
       tactic is not run at all. A tactic which expects multiple goals, such as
-      ``swap``, would act as if a single goal is focused.
+      :tacn:`swap`, would act as if a single goal is focused.
+
+   Note that :n:`@ltac_expr3 ; [ {*| @ltac_expr} ]` is a convenient idiom to
+   process the goals generated by applying :n:`@ltac_expr3`.
 
-   .. tacv:: @ltac_expr__0 ; [{*| @ltac_expr__i}]
+.. tacn:: @ltac_expr3 ; [ @for_each_goal ]
+   :name: [ … | … | … ] (dispatch)
 
-      This variant of local tactic application is paired with a sequence. In this
-      variant, there must be as many :n:`@ltac_expr__i` as goals generated
-      by the application of :n:`@ltac_expr__0` to each of the individual goals
-      independently. All the above variants work in this form too.
-      Formally, :n:`@ltac_expr ; [ ... ]` is equivalent to :n:`[> @ltac_expr ; [> ... ] .. ]`.
+   :n:`@ltac_expr3 ; [ ... ]` is equivalent to :n:`[> @ltac_expr3 ; [> ... ] .. ]`.
+
+.. todo see discussion of [ ... ] in https://github.com/coq/coq/issues/12283
 
 .. _goal-selectors:
 
@@ -269,100 +359,143 @@ Goal selectors
 
 .. todo: mention this applies to Print commands and the Info command
 
-
-We can restrict the application of a tactic to a subset of the currently
-focused goals with:
+By default, tactic expressions are applied only to the first goal.  Goal
+selectors provide a way to apply a tactic expression to another goal or multiple
+goals.  (The :opt:`Default Goal Selector` option can be used to change the default
+behavior.)
 
 .. tacn:: @toplevel_selector : @ltac_expr
-   :name: ... : ... (goal selector)
+   :name: … : … (goal selector)
 
-   We can also use selectors as a tactical, which allows to use them nested
-   in a tactic expression, by using the keyword ``only``:
+   .. insertprodn toplevel_selector toplevel_selector
 
-   .. tacv:: only @selector : @ltac_expr
-      :name: only ... : ...
+   .. prodn::
+      toplevel_selector ::= @selector
+      | all
+      | !
+      | par
 
-      When selecting several goals, the tactic :token:`ltac_expr` is applied globally to all
-      selected goals.
+   Applies :token:`ltac_expr` to the selected goals.  It can only be used at the top
+   level of a tactic expression; it cannot be used within a tactic expression.
 
-   .. tacv:: [@ident] : @ltac_expr
+   .. todo why shouldn't "all" and "!" be accepted anywhere a @selector is accepted?
+      It would be simpler to explain.
 
-      In this variant, :token:`ltac_expr` is applied locally to a goal previously named
+   `all`
+      Selects all focused goals.
+
+   `!`
+      If exactly one goal is in focus, apply :token:`ltac_expr` to it.
+      Otherwise the tactic fails.
+
+   `par`
+      Applies :n:`@ltac_expr` to all focused goals in parallel.
+      The number of workers can be controlled via the command line option
+      :n:`-async-proofs-tac-j @num` to specify the desired number of workers.
+      Limitations: ``par:`` only works on goals that don't contain existential
+      variables.  :n:`@ltac_expr` must either solve the goal completely or do
+      nothing (i.e. it cannot make some progress).
+
+Selectors can also be used nested within a tactic expression with the
+:tacn:`only` tactic:
+
+.. tacn:: only @selector : @ltac_expr3
+
+   .. insertprodn selector range_selector
+
+   .. prodn::
+      selector ::= {+, @range_selector }
+      | [ @ident ]
+      range_selector ::= @num - @num
+      | @num
+
+   Applies :token:`ltac_expr3` to the selected goals.
+
+   :tacn:`only` is an :token:`l3_tactic`.
+
+   :n:`{+, @range_selector }`
+      The selected goals are the union of the specified :token:`range_selector`\s.
+
+   :n:`[ @ident ]`
+      Limits the application of :token:`ltac_expr3` to the goal previously named :token:`ident`
       by the user (see :ref:`existential-variables`).
 
-   .. tacv:: @num : @ltac_expr
+   :n:`@num__1 - @num__2`
+      Selects the goals :n:`@num__1` through :n:`@num__2`, inclusive.
 
-      In this variant, :token:`ltac_expr` is applied locally to the :token:`num`-th goal.
+   :n:`@num`
+      Selects a single goal.
 
-   .. tacv:: {+, @num-@num} : @ltac_expr
+.. exn:: No such goal.
+   :name: No such goal. (Goal selector)
+   :undocumented:
 
-      In this variant, :n:`@ltac_expr` is applied globally to the subset of goals
-      described by the given ranges. You can write a single ``n`` as a shortcut
-      for ``n-n`` when specifying multiple ranges.
+.. TODO change error message index entry
 
-   .. tacv:: all: @ltac_expr
-      :name: all: ...
 
-      In this variant, :token:`ltac_expr` is applied to all focused goals. ``all:`` can only
-      be used at the toplevel of a tactic expression.
+Processing multiple goals
+~~~~~~~~~~~~~~~~~~~~~~~~~
 
-   .. tacv:: !: @ltac_expr
+When presented with multiple focused goals, most |Ltac| constructs process each goal
+separately.  They succeed only if there is a success for each goal.  For example:
 
-      In this variant, if exactly one goal is focused, :token:`ltac_expr` is
-      applied to it. Otherwise the tactic fails. ``!:`` can only be
-      used at the toplevel of a tactic expression.
+.. example:: Multiple focused goals
 
-   .. tacv:: par: @ltac_expr
-      :name: par: ...
+   This tactic fails because there no match for the second goal (`False`).
 
-      In this variant, :n:`@ltac_expr` is applied to all focused goals in parallel.
-      The number of workers can be controlled via the command line option
-      ``-async-proofs-tac-j`` taking as argument the desired number of workers.
-      Limitations: ``par:`` only works on goals containing no existential
-      variables and :n:`@ltac_expr` must either solve the goal completely or do
-      nothing (i.e. it cannot make some progress). ``par:`` can only be used at
-      the toplevel of a tactic expression.
+   .. coqtop:: reset none fail
 
-   .. exn:: No such goal.
-      :name: No such goal. (Goal selector)
-      :undocumented:
+      Goal True /\ False.
 
-   .. TODO change error message index entry
+   .. coqtop:: out
 
-For loop
-~~~~~~~~
+      split.
 
-There is a for loop that repeats a tactic :token:`num` times:
+   .. coqtop:: all
 
-.. tacn:: do @num @ltac_expr
+      Fail all: let n := numgoals in idtac "numgoals =" n;
+      match goal with
+      | |- True => idtac
+      end.
+
+Do loop
+~~~~~~~
+
+.. tacn:: do @int_or_var @ltac_expr3
    :name: do
 
+   The do loop repeats a tactic :token:`int_or_var` times:
+
    :n:`@ltac_expr` is evaluated to ``v`` which must be a tactic value. This tactic
-   value ``v`` is applied :token:`num` times. Supposing :token:`num` > 1, after the
+   value ``v`` is applied :token:`int_or_var` times. Supposing :token:`int_or_var` > 1, after the
    first application of ``v``, ``v`` is applied, at least once, to the generated
-   subgoals and so on. It fails if the application of ``v`` fails before the num
+   subgoals and so on. It fails if the application of ``v`` fails before :token:`int_or_var`
    applications have been completed.
 
+   :tacn:`do` is an :token:`l3_tactic`.
+
 Repeat loop
 ~~~~~~~~~~~
 
-We have a repeat loop with:
-
-.. tacn:: repeat @ltac_expr
+.. tacn:: repeat @ltac_expr3
    :name: repeat
 
+   The repeat loop repeats a tactic until it fails.
+
    :n:`@ltac_expr` is evaluated to ``v``. If ``v`` denotes a tactic, this tactic is
    applied to each focused goal independently. If the application succeeds, the
    tactic is applied recursively to all the generated subgoals until it eventually
    fails. The recursion stops in a subgoal when the tactic has failed *to make
-   progress*. The tactic :n:`repeat @ltac_expr` itself never fails.
+   progress*. The tactic :tacn:`repeat` :n:`@ltac_expr` itself never fails.
 
-Error catching
-~~~~~~~~~~~~~~
+   :tacn:`repeat` is an :token:`l3_tactic`.
+
+Catching errors: try
+~~~~~~~~~~~~~~~~~~~~
 
 We can catch the tactic errors with:
 
-.. tacn:: try @ltac_expr
+.. tacn:: try @ltac_expr3
    :name: try
 
    :n:`@ltac_expr` is evaluated to ``v`` which must be a tactic value. The tactic
@@ -371,71 +504,170 @@ We can catch the tactic errors with:
    level of the exception is positive, then the exception is re-raised with its
    level decremented.
 
+   :tacn:`try` is an :token:`l3_tactic`.
+
 Detecting progress
 ~~~~~~~~~~~~~~~~~~
 
 We can check if a tactic made progress with:
 
-.. tacn:: progress @ltac_expr
+.. tacn:: progress @ltac_expr3
    :name: progress
 
-   :n:`@ltac_expr` is evaluated to v which must be a tactic value. The tactic value ``v``
+   :n:`@ltac_expr` is evaluated to ``v`` which must be a tactic value. The tactic value ``v``
    is applied to each focused subgoal independently. If the application of ``v``
    to one of the focused subgoal produced subgoals equal to the initial
    goals (up to syntactical equality), then an error of level 0 is raised.
 
+   :tacn:`progress` is an :token:`l3_tactic`.
+
    .. exn:: Failed to progress.
       :undocumented:
 
-Backtracking branching
-~~~~~~~~~~~~~~~~~~~~~~
+Branching and backtracking
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+|Ltac| provides several :gdef:`branching` tactics that permit trying multiple alternative tactics
+for a proof step.  For example, :tacn:`first`, which tries several alternatives and selects the first
+that succeeds, or :tacn:`tryif`, which tests whether a given tactic would succeed or fail if it was
+applied and then, depending on the result, applies one of two alternative tactics.  There
+are also looping constructs :tacn:`do` and :tacn:`repeat`.  The order in which the subparts
+of these tactics are evaluated is generally similar to
+structured programming constructs in many languages.
+
+The :tacn:`+<+ (backtracking branching)>`, :tacn:`multimatch` and :tacn:`multimatch goal` tactics
+provide more complex capability.  Rather than applying a single successful
+tactic, these tactics generate a series of successful tactic alternatives that are tried sequentially
+when subsequent tactics outside these constructs fail.  For example:
 
-We can branch with the following structure:
+   .. example:: Backtracking
 
-.. tacn:: @ltac_expr__1 + @ltac_expr__2
+      .. coqtop:: all
+
+         Fail multimatch True with
+         | True => idtac "branch 1"
+         | _ => idtac "branch 2"
+         end ;
+         idtac "branch A"; fail.
+
+These constructs are evaluated using :gdef:`backtracking`.  Each  creates a
+:gdef:`backtracking point`.  When a subsequent tactic fails, evaluation continues from the nearest
+prior backtracking point with the next successful alternative and repeats the tactics after
+the backtracking point.  When a backtracking point has
+no more successful alternatives, evaluation continues from the next prior backtracking point.
+If there are no more prior backtracking points, the overall tactic fails.
+
+Thus, backtracking tactics can have multiple successes.  Non-backtracking constructs that appear
+after a backtracking point are reprocessed after backtracking, as in the example
+above, in which the :tacn:`;<ltac-seq>` construct is reprocessed after backtracking.  When a
+backtracking construct is within
+a non-backtracking construct, the latter uses the :gdef:`first success`.  Backtracking to
+a point within a non-backtracking construct won't change the branch that was selected by the
+non-backtracking construct.
+
+The :tacn:`once` tactic stops further backtracking to backtracking points within that tactic.
+
+Branching with backtracking: +
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+We can branch with backtracking with the following structure:
+
+.. tacn:: @ltac_expr1 + {| @ltac_expr2 | @binder_tactic }
    :name: + (backtracking branching)
 
-   :n:`@ltac_expr__1` and :n:`@ltac_expr__2` are evaluated respectively to :n:`v__1` and
-   :n:`v__2` which must be tactic values. The tactic value :n:`v__1` is applied to
-   each focused goal independently and if it fails or a later tactic fails, then
-   the proof backtracks to the current goal and :n:`v__2` is applied.
+   Evaluates and applies :n:`@ltac_expr1` to each focused goal independently.  If it fails
+   (i.e. there is no initial success), then evaluates and applies the right-hand side.  If the
+   right-hand side fails, the construct fails.
 
-   Tactics can be seen as having several successes. When a tactic fails it
-   asks for more successes of the prior tactics.
-   :n:`@ltac_expr__1 + @ltac_expr__2` has all the successes of :n:`v__1` followed by all the
-   successes of :n:`v__2`. Algebraically,
-   :n:`(@ltac_expr__1 + @ltac_expr__2); @ltac_expr__3 = (@ltac_expr__1; @ltac_expr__3) + (@ltac_expr__2; @ltac_expr__3)`.
+   If :n:`ltac_expr1` has an initial success and a subsequent tactic (outside the `+` construct)
+   fails, |Ltac| backtracks and selects the next success for :n:`ltac_expr1`.  If there are
+   no more successes, then `+` similarly evaluates and applies (and backtracks in) the right-hand side.
+   To prevent evaluation of further alternatives after an initial success for a tactic, use :tacn:`first` instead.
 
-   Branching is left-associative.
+   `+` is left-associative.
 
-First tactic to work
-~~~~~~~~~~~~~~~~~~~~
+   In all cases, :n:`(@ltac_expr__1 + @ltac_expr__2); @ltac_expr__3` is equivalent to
+   :n:`(@ltac_expr__1; @ltac_expr__3) + (@ltac_expr__2; @ltac_expr__3)`.
+
+   Additionally, in most cases, :n:`(@ltac_expr__1 + @ltac_expr__2) + @ltac_expr__3` is
+   equivalent to :n:`@ltac_expr__1 + (@ltac_expr__2 + @ltac_expr__3)`.
+   Here's an example where the behavior differs slightly:
 
-Backtracking branching may be too expensive. In this case we may
-restrict to a local, left biased, branching and consider the first
-tactic to work (i.e. which does not fail) among a panel of tactics:
+      .. coqtop:: reset none
 
-.. tacn:: first [{*| @ltac_expr}]
+         Goal True.
+
+      .. coqtop:: all
+
+        Fail (fail 2 + idtac) + idtac.
+        Fail fail 2 + (idtac + idtac).
+
+   .. example:: Backtracking branching with +
+
+      In the first tactic, `idtac "2"` is not executed.  In the second, the subsequent `fail` causes
+      backtracking and the execution of `idtac "B"`.
+
+      .. coqtop:: reset none
+
+         Goal True.
+
+      .. coqtop:: all
+
+         idtac "1" + idtac "2".
+         assert_fails ((idtac "A" + idtac "B"); fail).
+
+First tactic to succeed
+~~~~~~~~~~~~~~~~~~~~~~~
+
+In some cases backtracking may be too expensive.
+
+.. tacn:: first [ {*| @ltac_expr } ]
    :name: first
 
-   The :n:`@ltac_expr__i` are evaluated to :n:`v__i` and :n:`v__i` must be
-   tactic values for i = 1, ..., n. Supposing n > 1,
-   :n:`first [@ltac_expr__1 | ... | @ltac_expr__n]` applies :n:`v__1` in each
-   focused goal independently and stops if it succeeds; otherwise it
-   tries to apply :n:`v__2` and so on. It fails when there is no
-   applicable tactic. In other words,
-   :n:`first [@ltac_expr__1 | ... | @ltac_expr__n]` behaves, in each goal, as the first
-   :n:`v__i` to have *at least* one success.
+   For each focused goal, independently apply the first :token:`ltac_expr` that succeeds.
+   The :n:`@ltac_expr`\s must evaluate to tactic values.
+   Failures in tactics after the :tacn:`first` won't cause backtracking.
+   (To allow backtracking, use the :tacn:`+<+ (backtracking branching)>`
+   construct above instead.)
+
+   If the :tacn:`first` contains a tactic that can backtrack, "success" means
+   the first success of that tactic.  Consider the following:
+
+   .. example:: Backtracking inside a non-backtracking construct
+
+      .. coqtop:: reset none
+
+         Goal True.
+
+      The :tacn:`fail` doesn't trigger the second :tacn:`idtac`:
+
+      .. coqtop:: all
+
+         assert_fails (first [ idtac "1" | idtac "2" ]; fail).
+
+      This backtracks within `(idtac "1A" + idtac "1B" + fail)` but
+      :tacn:`first` won't consider the `idtac "2"` alternative:
+
+      .. coqtop:: all
+
+       assert_fails (first [ (idtac "1A" + idtac "1B" + fail) | idtac "2" ]; fail).
+
+   :tacn:`first` is an :token:`l1_tactic`.
 
    .. exn:: No applicable tactic.
       :undocumented:
 
+   .. todo the following is not accepted as a regular tactic but it does seem to do something
+      see https://github.com/coq/coq/pull/12103#discussion_r422249862.
+      Probably the same thing as for the :tacv:`solve` below.
+      The code is in Coretactics.initial_tacticals
+
    .. tacv:: first @ltac_expr
 
       This is an |Ltac| alias that gives a primitive access to the first
       tactical as an |Ltac| definition without going through a parsing rule. It
-      expects to be given a list of tactics through a ``Tactic Notation``,
-      allowing to write notations of the following form:
+      expects to be given a list of tactics through a :cmd:`Tactic Notation` command,
+      permitting notations with the following form to be written:
 
       .. example::
 
@@ -443,188 +675,239 @@ tactic to work (i.e. which does not fail) among a panel of tactics:
 
             Tactic Notation "foo" tactic_list(tacs) := first tacs.
 
-Left-biased branching
-~~~~~~~~~~~~~~~~~~~~~
+Solving
+~~~~~~~
+
+Selects and applies the first tactic that solves each goal (i.e. leaves no subgoal)
+in a series of alternative tactics:
+
+.. tacn:: solve [ {*| @ltac_expr__i } ]
+   :name: solve
+
+   For each current subgoal: evaluates and applies each :n:`@ltac_expr` in order
+   until one is found that solves the subgoal.
+
+   If any of the subgoals are not solved, then the overall :tacn:`solve` fails.
+
+   .. note:: In :tacn:`solve` and :tacn:`first`, :n:`@ltac_expr`\s that don't
+      evaluate to tactic values are ignored.  So :tacn:`solve` `[ () | 1 |` :tacn:`constructor` `]`
+      is equivalent to :tacn:`solve` `[` :tacn:`constructor` `]`.
+      This may make it harder to debug scripts that inadvertently include non-tactic values.
+
+   .. todo check the behavior of other constructs
+      see https://github.com/coq/coq/pull/12103#discussion_r436320430
+
+   :tacn:`solve` is an :token:`l1_tactic`.
+
+   .. tacv:: solve @ltac_expr
+
+      This is an |Ltac| alias that gives a primitive access to the :tacn:`solve`
+      tactic. See the :tacn:`first` tactic for more information.
+
+First tactic to make progress: ||
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 Yet another way of branching without backtracking is the following
 structure:
 
-.. tacn:: @ltac_expr__1 || @ltac_expr__2
-   :name: || (left-biased branching)
+.. tacn:: @ltac_expr1 || {| @ltac_expr2 | @binder_tactic }
+   :name: || (first tactic making progress)
 
-   :n:`@ltac_expr__1` and :n:`@ltac_expr__2` are evaluated respectively to :n:`v__1` and
-   :n:`v__2` which must be tactic values. The tactic value :n:`v__1` is
-   applied in each subgoal independently and if it fails *to progress* then
-   :n:`v__2` is applied. :n:`@ltac_expr__1 || @ltac_expr__2` is
-   equivalent to :n:`first [ progress @ltac_expr__1 | @ltac_expr__2 ]` (except that
-   if it fails, it fails like :n:`v__2`). Branching is left-associative.
+   :n:`@ltac_expr1 || @ltac_expr2` is
+   equivalent to :n:`first [ progress @ltac_expr1 | @ltac_expr2 ]`, except that
+   if it fails, it fails like :n:`@ltac_expr2. `||` is left-associative.
 
-Generalized biased branching
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+   :n:`@ltac_expr`\s that don't evaluate to tactic values are ignored.  See the
+   note at :tacn:`solve`.
 
-The tactic
+Conditional branching: tryif
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. tacn:: tryif @ltac_expr__1 then @ltac_expr__2 else @ltac_expr__3
+.. tacn:: tryif @ltac_expr__test then @ltac_expr__then else @ltac_expr2__else
    :name: tryif
 
-   is a generalization of the biased-branching tactics above. The
-   expression :n:`@ltac_expr__1` is evaluated to :n:`v__1`, which is then
-   applied to each subgoal independently. For each goal where :n:`v__1`
-   succeeds at least once, :n:`@ltac_expr__2` is evaluated to :n:`v__2` which
-   is then applied collectively to the generated subgoals. The :n:`v__2`
-   tactic can trigger backtracking points in :n:`v__1`: where :n:`v__1`
-   succeeds at least once,
-   :n:`tryif @ltac_expr__1 then @ltac_expr__2 else @ltac_expr__3` is equivalent to
-   :n:`v__1; v__2`. In each of the goals where :n:`v__1` does not succeed at least
-   once, :n:`@ltac_expr__3` is evaluated in :n:`v__3` which is is then applied to the
-   goal.
-
-Soft cut
-~~~~~~~~
+   For each focused goal, independently: Evaluate and apply :n:`@ltac_expr__test`.
+   If :n:`@ltac_expr__test` succeeds at least once, evaluate and apply :n:`@ltac_expr__then`
+   to all the subgoals generated by :n:`@ltac_expr__test`.  Otherwise, evaluate and apply
+   :n:`@ltac_expr2__else` to all the subgoals generated by :n:`@ltac_expr__test`.
+
+   :tacn:`tryif` is an :token:`l2_tactic`.
+
+   .. multigoal example - not sure it adds much
+      Goal True /\ False.
+      split; tryif
+        match goal with
+        | |- True => idtac "True"
+        | |- False => idtac "False" end
+      then idtac "then" else idtac "else".
+
+Soft cut: once
+~~~~~~~~~~~~~~
+
+.. todo Would like a different subsection title above.
+   I have trouble distinguishing once and exactly_once.
+   We need to explain backtracking somewhere.
+   See https://github.com/coq/coq/pull/12103#discussion_r422360181
 
 Another way of restricting backtracking is to restrict a tactic to a
 single success:
 
-.. tacn:: once @ltac_expr
+.. tacn:: once @ltac_expr3
    :name: once
 
-   :n:`@ltac_expr` is evaluated to ``v`` which must be a tactic value. The tactic value
+   :n:`@ltac_expr3` is evaluated to ``v`` which must be a tactic value. The tactic value
    ``v`` is applied but only its first success is used. If ``v`` fails,
-   :n:`once @ltac_expr` fails like ``v``. If ``v`` has at least one success,
-   :n:`once @ltac_expr` succeeds once, but cannot produce more successes.
+   :tacn:`once` :n:`@ltac_expr3` fails like ``v``. If ``v`` has at least one success,
+   :tacn:`once` :n:`@ltac_expr3` succeeds once, but cannot produce more successes.
 
-Checking the successes
-~~~~~~~~~~~~~~~~~~~~~~
+   :tacn:`once` is an :token:`l3_tactic`.
+
+Checking for a single success: exactly_once
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 Coq provides an experimental way to check that a tactic has *exactly
 one* success:
 
-.. tacn:: exactly_once @ltac_expr
+.. tacn:: exactly_once @ltac_expr3
    :name: exactly_once
 
-   :n:`@ltac_expr` is evaluated to ``v`` which must be a tactic value. The tactic value
+   :n:`@ltac_expr3` is evaluated to ``v`` which must be a tactic value. The tactic value
    ``v`` is applied if it has at most one success. If ``v`` fails,
-   :n:`exactly_once @ltac_expr` fails like ``v``. If ``v`` has a exactly one success,
-   :n:`exactly_once @ltac_expr` succeeds like ``v``. If ``v`` has two or more
-   successes, :n:`exactly_once @ltac_expr` fails.
+   :tacn:`exactly_once` :n:`@ltac_expr3` fails like ``v``. If ``v`` has a exactly one success,
+   :tacn:`exactly_once` :n:`@ltac_expr3` succeeds like ``v``. If ``v`` has two or more
+   successes, :tacn:`exactly_once` :n:`@ltac_expr3` fails.
+
+   :tacn:`exactly_once` is an :token:`l3_tactic`.
 
    .. warning::
 
       The experimental status of this tactic pertains to the fact if ``v``
-      performs side effects, they may occur in an unpredictable way. Indeed,
+      has side effects, they may occur in an unpredictable way. Indeed,
       normally ``v`` would only be executed up to the first success until
-      backtracking is needed, however exactly_once needs to look ahead to see
+      backtracking is needed, however :tacn:`exactly_once` needs to look ahead to see
       whether a second success exists, and may run further effects
       immediately.
 
    .. exn:: This tactic has more than one success.
       :undocumented:
 
-Checking the failure
-~~~~~~~~~~~~~~~~~~~~
+Checking for failure: assert_fails
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-Coq provides a derived tactic to check that a tactic *fails*:
+Coq defines an |Ltac| tactic in `Init.Tactics` to check that a tactic *fails*:
 
-.. tacn:: assert_fails @ltac_expr
+.. tacn:: assert_fails @ltac_expr3
    :name: assert_fails
 
-   This behaves like :tacn:`idtac` if :n:`@ltac_expr` fails, and
-   behaves like :n:`fail 0 @ltac_expr "succeeds"` if :n:`@ltac_expr`
-   has at least one success.
+   If :n:`@ltac_expr3` fails, the proof state is unchanged and no message is printed.
+   If :n:`@ltac_expr3` unexpectedly has at least one success, the tactic performs
+   a :tacn:`gfail` :n:`0`, printing the following message:
 
-Checking the success
-~~~~~~~~~~~~~~~~~~~~
+   .. exn:: Tactic failure: <tactic closure> succeeds.
+      :undocumented:
 
-Coq provides a derived tactic to check that a tactic has *at least one*
-success:
+   .. note:: :tacn:`assert_fails` and :tacn:`assert_succeeds` work as described when
+      :token:`ltac_expr3` is a :token:`simple_tactic`.  In some more complex expressions,
+      they may report an error from within :token:`ltac_expr3` when they shouldn't.
+      This is due to the order in which parts of the :token:`ltac_expr3`
+      are evaluated and executed.  For example:
 
-.. tacn:: assert_succeeds @ltac_expr
-   :name: assert_succeeds
+      .. coqtop:: reset none
 
-   This behaves like
-   :n:`tryif (assert_fails @ltac_expr) then fail 0 @ltac_expr "fails" else idtac`.
+         Goal True.
 
-Solving
-~~~~~~~
+      .. coqtop:: all fail
 
-We may consider the first to solve (i.e. which generates no subgoal)
-among a panel of tactics:
+         assert_fails match True with _ => fail end.
 
-.. tacn:: solve [{*| @ltac_expr}]
-   :name: solve
+      should not show any message.  The issue is that :tacn:`assert_fails` is an |Ltac|-defined
+      tactic.  That makes it a function that's processed in the evaluation phase, causing
+      the :tacn:`match` to find its first success earlier.  One workaround
+      is to prefix :token:`ltac_expr3` with "`idtac;`".
 
-   The :n:`@ltac_expr__i` are evaluated to :n:`v__i` and :n:`v__i` must be
-   tactic values, for i = 1, ..., n. Supposing n > 1,
-   :n:`solve [@ltac_expr__1 | ... | @ltac_expr__n]` applies :n:`v__1` to
-   each goal independently and stops if it succeeds; otherwise it tries to
-   apply :n:`v__2` and so on. It fails if there is no solving tactic.
+      .. coqtop:: all
 
-   .. exn:: Cannot solve the goal.
-      :undocumented:
+         assert_fails (idtac; match True with _ => fail end).
 
-   .. tacv:: solve @ltac_expr
+      Alternatively, substituting the :tacn:`match` into the definition of :tacn:`assert_fails` works
+      as expected:
+
+      .. coqtop:: all
 
-      This is an |Ltac| alias that gives a primitive access to the :n:`solve:`
-      tactical. See the :n:`first` tactical for more information.
+         tryif (once match True with _ => fail end) then gfail 0 (* tac *) "succeeds" else idtac.
 
-Identity
-~~~~~~~~
 
-The constant :n:`idtac` is the identity tactic: it leaves any goal unchanged but
-it appears in the proof script.
+Checking for success: assert_succeeds
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Coq defines an |Ltac| tactic in `Init.Tactics` to check that a tactic has *at least one*
+success:
+
+.. tacn:: assert_succeeds @ltac_expr3
+   :name: assert_succeeds
 
-.. tacn:: idtac {* @message_token}
+   If :n:`@ltac_expr3` has at least one success, the proof state is unchanged and
+   no message is printed.  If :n:`@ltac_expr3` fails, the tactic performs
+   a :tacn:`gfail` :n:`0`, printing the following message:
+
+   .. exn:: Tactic failure: <tactic closure> fails.
+      :undocumented:
+
+Print/identity tactic: idtac
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+
+.. tacn:: idtac {* {| @ident | @string | @int } }
    :name: idtac
 
-   This prints the given tokens. Strings and integers are printed
-   literally. If a (term) variable is given, its contents are printed.
+   Leaves the proof unchanged and prints the given tokens. Strings and integers are printed
+   literally. If :token:`ident` is an |Ltac| variable, its contents are printed; if not, it
+   is an error.
+
+   :tacn:`idtac` is an :token:`l1_tactic`.
 
 Failing
 ~~~~~~~
 
-.. tacn:: fail
-   :name: fail
+.. tacn:: {| fail | gfail } {? @int_or_var } {* {| @ident | @string | @int } }
+   :name: fail; gfail
 
-   This is the always-failing tactic: it does not solve any
-   goal. It is useful for defining other tacticals since it can be caught by
+   :tacn:`fail` is the always-failing tactic: it does not solve any
+   goal. It is useful for defining other tactics since it can be caught by
    :tacn:`try`, :tacn:`repeat`, :tacn:`match goal`, or the branching tacticals.
 
-   .. tacv:: fail @num
+   :tacn:`gfail` fails even when used after :n:`;` and there are no goals left.
+   Similarly, :tacn:`gfail` fails even when used after ``all:`` and there are no
+   goals left.
+
+   :tacn:`fail` and :tacn:`gfail` are :token:`l1_tactic`\s.
+
+
+   See the example for a comparison of the two constructs.
 
-      The number is the failure level. If no level is specified, it defaults to 0.
+   Note that if Coq terms have to be
+   printed as part of the failure, term construction always forces the
+   tactic into the goals, meaning that if there are no goals when it is
+   evaluated, a tactic call like :tacn:`let` :n:`x := H in` :tacn:`fail` `0 x` will succeed.
+
+   :n:`@int_or_var`
+      The failure level. If no level is specified, it defaults to 0.
       The level is used by :tacn:`try`, :tacn:`repeat`, :tacn:`match goal` and the branching
       tacticals. If 0, it makes :tacn:`match goal` consider the next clause
       (backtracking). If nonzero, the current :tacn:`match goal` block, :tacn:`try`,
       :tacn:`repeat`, or branching command is aborted and the level is decremented. In
       the case of :n:`+`, a nonzero level skips the first backtrack point, even if
-      the call to :n:`fail @num` is not enclosed in a :n:`+` command,
+      the call to :tacn:`fail` :n:`@num` is not enclosed in a :n:`+` construct,
       respecting the algebraic identity.
 
-   .. tacv:: fail {* @message_token}
-
-      The given tokens are used for printing the failure message.
-
-   .. tacv:: fail @num {* @message_token}
-
-      This is a combination of the previous variants.
-
-   .. tacv:: gfail
-      :name: gfail
-
-      This variant fails even when used after :n:`;` and there are no goals left.
-      Similarly, ``gfail`` fails even when used after ``all:`` and there are no
-      goals left. See the example for clarification.
+   :n:`{* {| @ident | @string | @int } }`
+      The given tokens are used for printing the failure message.  If :token:`ident`
+      is an |Ltac| variable, its contents are printed; if not, it is an error.
 
-   .. tacv:: gfail {* @message_token}
-             gfail @num {* @message_token}
-
-      These variants fail with an error message or an error level even if
-      there are no goals left. Be careful however if Coq terms have to be
-      printed as part of the failure: term construction always forces the
-      tactic into the goals, meaning that if there are no goals when it is
-      evaluated, a tactic call like :n:`let x := H in fail 0 x` will succeed.
+   .. exn:: Tactic failure.
+      :undocumented:
 
-   .. exn:: Tactic Failure message (level @num).
+   .. exn:: Tactic failure (level @num).
       :undocumented:
 
    .. exn:: No such goal.
@@ -633,7 +916,12 @@ Failing
 
    .. example::
 
-      .. coqtop:: all fail
+      .. todo the example is too long; could show the Goal True. Proof. once and hide the Aborts
+         to shorten it.  And add a line of text before each subexample.  Perhaps add some very short
+         explanations/generalizations (eg gfail always fails; "tac; fail" succeeds but "fail." alone
+         fails.
+
+      .. coqtop:: reset all fail
 
          Goal True.
          Proof. fail. Abort.
@@ -665,13 +953,15 @@ Timeout
 We can force a tactic to stop if it has not finished after a certain
 amount of time:
 
-.. tacn:: timeout @num @ltac_expr
+.. tacn:: timeout @int_or_var @ltac_expr3
    :name: timeout
 
-   :n:`@ltac_expr` is evaluated to ``v`` which must be a tactic value. The tactic value
+   :n:`@ltac_expr3` is evaluated to ``v`` which must be a tactic value. The tactic value
    ``v`` is applied normally, except that it is interrupted after :n:`@num` seconds
    if it is still running. In this case the outcome is a failure.
 
+   :tacn:`timeout` is an :token:`l3_tactic`.
+
    .. warning::
 
       For the moment, timeout is based on elapsed time in seconds,
@@ -687,17 +977,19 @@ Timing a tactic
 
 A tactic execution can be timed:
 
-.. tacn:: time @string @ltac_expr
+.. tacn:: time {? @string } @ltac_expr3
    :name: time
 
-   evaluates :n:`@ltac_expr` and displays the running time of the tactic expression, whether it
+   evaluates :n:`@ltac_expr3` and displays the running time of the tactic expression, whether it
    fails or succeeds. In case of several successes, the time for each successive
    run is displayed. Time is in seconds and is machine-dependent. The :n:`@string`
    argument is optional. When provided, it is used to identify this particular
-   occurrence of time.
+   occurrence of :tacn:`time`.
 
-Timing a tactic that evaluates to a term
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+   :tacn:`time` is an :token:`l3_tactic`.
+
+Timing a tactic that evaluates to a term: time_constr
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 Tactic expressions that produce terms can be timed with the experimental
 tactic
@@ -713,248 +1005,463 @@ tactic
    based on the innermost execution. This is due to the fact that it is
    implemented using the following internal tactics:
 
-   .. tacn:: restart_timer @string
-      :name: restart_timer
+.. tacn:: restart_timer {? @string }
+   :name: restart_timer
 
-      Reset a timer
+   Reset a timer
 
-   .. tacn:: finish_timing {? (@string)} @string
-      :name: finish_timing
+.. tacn:: finish_timing {? ( @string ) } {? @string }
+   :name: finish_timing
 
-      Display an optionally named timer. The parenthesized string argument
-      is also optional, and determines the label associated with the timer
-      for printing.
+   Display an optionally named timer. The parenthesized string argument
+   is also optional, and determines the label associated with the timer
+   for printing.
 
-   By copying the definition of :tacn:`time_constr` from the standard library,
-   users can achieve support for a fixed pattern of nesting by passing
-   different :token:`string` parameters to :tacn:`restart_timer` and
-   :tacn:`finish_timing` at each level of nesting.
+By copying the definition of :tacn:`time_constr` from the standard library,
+users can achieve support for a fixed pattern of nesting by passing
+different :token:`string` parameters to :tacn:`restart_timer` and
+:tacn:`finish_timing` at each level of nesting.
 
-   .. example::
+.. example::
 
-      .. coqtop:: all abort
+   .. coqtop:: all abort
 
-         Ltac time_constr1 tac :=
-           let eval_early := match goal with _ => restart_timer "(depth 1)" end in
-           let ret := tac () in
-           let eval_early := match goal with _ => finish_timing ( "Tactic evaluation" ) "(depth 1)" end in
-           ret.
+      Ltac time_constr1 tac :=
+        let eval_early := match goal with _ => restart_timer "(depth 1)" end in
+        let ret := tac () in
+        let eval_early := match goal with _ => finish_timing ( "Tactic evaluation" ) "(depth 1)" end in
+        ret.
+
+      Goal True.
+        let v := time_constr
+             ltac:(fun _ =>
+                     let x := time_constr1 ltac:(fun _ => constr:(10 * 10)) in
+                     let y := time_constr1 ltac:(fun _ => eval compute in x) in
+                     y) in
+        pose v.
+
+Local definitions: let
+~~~~~~~~~~~~~~~~~~~~~~
 
-         Goal True.
-           let v := time_constr
-                ltac:(fun _ =>
-                        let x := time_constr1 ltac:(fun _ => constr:(10 * 10)) in
-                        let y := time_constr1 ltac:(fun _ => eval compute in x) in
-                        y) in
-           pose v.
-
-Local definitions
-~~~~~~~~~~~~~~~~~
+.. tacn:: let {? rec } @let_clause {* with @let_clause } in @ltac_expr
 
-Local definitions can be done as follows:
+   .. insertprodn let_clause let_clause
 
-.. tacn:: let @ident__1 := @ltac_expr__1 {* with @ident__i := @ltac_expr__i} in @ltac_expr
-   :name: let ... := ...
+   .. prodn::
+      let_clause ::= @name := @ltac_expr
+      | @ident {+ @name } := @ltac_expr
 
-   each :n:`@ltac_expr__i` is evaluated to :n:`v__i`, then, :n:`@ltac_expr` is evaluated
-   by substituting :n:`v__i` to each occurrence of :n:`@ident__i`, for
-   i = 1, ..., n. There are no dependencies between the :n:`@ltac_expr__i` and the
-   :n:`@ident__i`.
+   Binds symbols within :token:`ltac_expr`.  :tacn:`let` evaluates each :n:`@let_clause`, substitutes
+   the bound variables into :n:`@ltac_expr` and then evaluates :n:`@ltac_expr`.  There are
+   no dependencies between the :n:`@let_clause`\s.
 
-   Local definitions can be made recursive by using :n:`let rec` instead of :n:`let`.
-   In this latter case, the definitions are evaluated lazily so that the rec
-   keyword can be used also in non-recursive cases so as to avoid the eager
-   evaluation of local definitions.
+   Use :tacn:`let` `rec` to create recursive or mutually recursive bindings, which
+   causes the definitions to be evaluated lazily.
 
-   .. but rec changes the binding!!
+   :tacn:`let` is a :token:`binder_tactic`.
 
-Application
-~~~~~~~~~~~
+Function construction and application
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+A parameterized tactic can be built anonymously (without resorting to
+local definitions) with:
 
-An application is an expression of the following form:
+.. tacn:: fun {+ @name } => @ltac_expr
 
-.. tacn:: @qualid {+ @tacarg}
+   Indeed, local definitions of functions are syntactic sugar for binding
+   a :n:`fun` tactic to an identifier.
 
-   The reference :n:`@qualid` must be bound to some defined tactic definition
-   expecting at least as many arguments as the provided :n:`tacarg`. The
-   expressions :n:`@ltac_expr__i` are evaluated to :n:`v__i`, for i = 1, ..., n.
+   :tacn:`fun` is a :token:`binder_tactic`.
 
-   .. what expressions ??
+Functions can return values of any type.
 
-Function construction
-~~~~~~~~~~~~~~~~~~~~~
+A function application is an expression of the form:
 
-A parameterized tactic can be built anonymously (without resorting to
-local definitions) with:
+.. tacn:: @qualid {+ @tactic_arg }
 
-.. tacn:: fun {+ @ident} => @ltac_expr
+   :n:`@qualid` must be bound to a |Ltac| function
+   with at least as many arguments as the provided :n:`@tactic_arg`\s.
+   The :n:`@tactic_arg`\s are evaluated before the function is applied
+   or partially applied.
 
-   Indeed, local definitions of functions are a syntactic sugar for binding
-   a :n:`fun` tactic to an identifier.
+   Functions may be defined with the :tacn:`fun` and :tacn:`let` tactics
+   and with the :cmd:`Ltac` command.
 
-Pattern matching on terms
-~~~~~~~~~~~~~~~~~~~~~~~~~
+   .. todo above: note "gobble" corner case
+      https://github.com/coq/coq/pull/12103#discussion_r436414417
+
+Pattern matching on terms: match
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+.. tacn:: @match_key @ltac_expr__term with {? %| } {+| @match_pattern => @ltac_expr } end
+   :name: lazymatch; match; multimatch
+
+   .. insertprodn match_key cpattern
+
+   .. prodn::
+      match_key ::= lazymatch
+      | match
+      | multimatch
+      match_pattern ::= @cpattern
+      | context {? @ident } [ @cpattern ]
+      cpattern ::= @term
 
-We can carry out pattern matching on terms with:
+   :tacn:`lazymatch`, :tacn:`match` and :tacn:`multimatch` are :token:`ltac_expr1`\s.
 
-.. tacn:: match @ltac_expr with {+| @cpattern__i => @ltac_expr__i} end
+   Evaluates :n:`@ltac_expr__term`, which must yield a term, and matches it
+   sequentially with the :token:`match_pattern`\s, which may have
+   metavariables.  When a match is found, metavariable values are substituted
+   into :n:`@ltac_expr`, which is then applied.
 
-   The expression :n:`@ltac_expr` is evaluated and should yield a term which is
-   matched against :n:`cpattern__1`. The matching is non-linear: if a
-   metavariable occurs more than once, it should match the same expression
-   every time. It is first-order except on the variables of the form :n:`@?id`
-   that occur in head position of an application. For these variables, the
+   Matching may continue depending on whether  `lazymatch`, `match` or `multimatch`
+   is specified.
+
+   In the :token:`match_pattern`\s, metavariables have the form :n:`?@ident`, whereas
+   in the :n:`@ltac_expr`\s, the question mark is omitted.  Choose your metavariable
+   names with care to avoid name conflicts.  For example, if you use the metavariable `S`,
+   then the :token:`ltac_expr` can't use `S` to refer to the constructor of `nat`
+   without qualifying the constructor as `Datatypes.S`.
+
+   .. todo below: is matching non-linear unification?  is it the same or different
+      from unification elsewhere in Coq?
+
+   Matching is non-linear: if a
+   metavariable occurs more than once, each occurrence must match the same
+   expression.  Matching is first-order except on variables of the form :n:`@?@ident`
+   that occur in the head position of an application. For these variables,
    matching is second-order and returns a functional term.
 
-   Alternatively, when a metavariable of the form :n:`?id` occurs under binders,
-   say :n:`x__1, …, x__n` and the expression matches, the
-   metavariable is instantiated by a term which can then be used in any
-   context which also binds the variables :n:`x__1, …, x__n` with
-   same types. This provides with a primitive form of matching under
-   context which does not require manipulating a functional term.
-
-   If the matching with :n:`@cpattern__1` succeeds, then :n:`@ltac_expr__1` is
-   evaluated into some value by substituting the pattern matching
-   instantiations to the metavariables. If :n:`@ltac_expr__1` evaluates to a
-   tactic and the match expression is in position to be applied to a goal
-   (e.g. it is not bound to a variable by a :n:`let in`), then this tactic is
-   applied. If the tactic succeeds, the list of resulting subgoals is the
-   result of the match expression. If :n:`@ltac_expr__1` does not evaluate to a
-   tactic or if the match expression is not in position to be applied to a
-   goal, then the result of the evaluation of :n:`@ltac_expr__1` is the result
-   of the match expression.
-
-   If the matching with :n:`@cpattern__1` fails, or if it succeeds but the
-   evaluation of :n:`@ltac_expr__1` fails, or if the evaluation of
-   :n:`@ltac_expr__1` succeeds but returns a tactic in execution position whose
-   execution fails, then :n:`cpattern__2` is used and so on. The pattern
-   :n:`_` matches any term and shadows all remaining patterns if any. If all
-   clauses fail (in particular, there is no pattern :n:`_`) then a
-   no-matching-clause error is raised.
-
-   Failures in subsequent tactics do not cause backtracking to select new
-   branches or inside the right-hand side of the selected branch even if it
-   has backtracking points.
+   .. todo 30 May 20: the `@?ident` form is in dangling_pattern_extension_rule, not included in the doc yet
+      maybe belongs with "Applications"
+
+   `lazymatch`
+      Causes the match to commit to the first matching branch
+      rather than trying a new match if :n:`@ltac_expr` fails.
+      :ref:`Example<match_vs_lazymatch_ex>`.
+
+   `match`
+      If :n:`@ltac_expr` fails, continue matching with the next branch.
+      Failures in subsequent tactics (after the `match`) will not cause selection
+      of a new branch.  Examples :ref:`here<match_vs_lazymatch_ex>` and
+      :ref:`here<match_vs_multimatch_ex>`.
+
+   `multimatch`
+      If :n:`@ltac_expr` fails, continue matching with the next branch.
+      When an :n:`@ltac_expr` succeeds for a branch, subsequent failures
+      (after the `multimatch`) causing consumption of all the successes
+      of :n:`@ltac_expr` trigger selection of a new matching branch.
+      :ref:`Example<match_vs_multimatch_ex>`.
+
+      :tacn:`match` :n:`…` is, in fact, shorthand for :tacn:`once` :tacn:`multimatch` `…`.
+
+   :n:`@cpattern`
+      The syntax of :token:`cpattern` is
+      the same as that of :token:`term`\s, but it can contain pattern matching
+      metavariables in the form :n:`?@ident`.  :g:`_` can be used to match
+      irrelevant terms.  :ref:`Example<match_with_holes_ex>`.
+
+      .. todo Didn't understand the following 2 paragraphs well enough to revise
+         see https://github.com/coq/coq/pull/12103#discussion_r436297754 for a
+         possible example
+
+      When a metavariable in the form :n:`?id` occurs under binders,
+      say :n:`x__1, …, x__n` and the expression matches, the
+      metavariable is instantiated by a term which can then be used in any
+      context which also binds the variables :n:`x__1, …, x__n` with
+      same types. This provides with a primitive form of matching under
+      context which does not require manipulating a functional term.
+
+      There is also a special notation for second-order pattern matching: in an
+      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`.
+
+   .. _match_term_context:
+
+   :n:`context {? @ident } [ @cpattern ]`
+      Matches any term with a subterm matching :token:`cpattern`. If there is a match
+      and :n:`@ident` is present, it is assigned the "matched
+      context", i.e. the initial term where the matched subterm is replaced by a
+      hole.  Note that `context`
+      (with very similar syntax) appearing after the `=>` is the :tacn:`context` tactic.
+
+      For :tacn:`match` and :tacn:`multimatch`, if the evaluation of the :token:`ltac_expr`
+      fails, the next matching subterm is tried. If no further subterm matches, the next branch
+      is tried.  Matching subterms are considered from top to bottom and from left to
+      right (with respect to the raw printing obtained by setting the
+      :flag:`Printing All` flag).  :ref:`Example<match_term_context_ex>`.
+
+   .. todo There's a more realistic example from @JasonGross here:
+      https://github.com/coq/coq/pull/12103#discussion_r432996954
+
+   :n:`@ltac_expr`
+      The tactic to apply if the construct matches.  Metavariable values from the pattern
+      match are substituted
+      into :n:`@ltac_expr` before it's applied.  Note that metavariables are not
+      prefixed with the question mark as they are in :token:`cpattern`.
+
+      If :token:`ltac_expr` evaluates to a tactic, then it is
+      applied. If the tactic succeeds, the result of the match expression is
+      :tacn:`idtac`.  If :token:`ltac_expr` does not evaluate
+      to a tactic, that value is the result of the match expression.
+
+      If :n:`@ltac_expr` is a tactic with backtracking points, then subsequent
+      failures after a :tacn:`lazymatch` or :tacn:`multimatch` (but not :tacn:`match`) can cause
+      backtracking into :n:`@ltac_expr` to select its next success.
+      (:tacn:`match` :n:`…` is equivalent to :tacn:`once` :tacn:`multimatch` `…`.
+      The :tacn:`once` prevents backtracking into the :tacn:`match` after it has succeeded.)
+
+   .. note::
+      Each |Ltac| construct is processed in two phases: an evaluation phase and an execution phase.
+      In most cases, tactics that may change the proof state are applied in the second phase.
+      (Tactics that generate integer, string or syntactic values, such as :tacn:`fresh`,
+      are processed during the evaluation phase.)
+
+      Unlike other tactics, `*match*` tactics get their first success (applying tactics to do
+      so) as part of the evaluation phase.  Among other things, this can affect how early
+      failures are processed in :tacn:`assert_fails`.  Please see the note in :tacn:`assert_fails`.
+
+   .. exn:: Expression does not evaluate to a tactic.
+
+      :n:`@ltac_expr` must evaluate to a tactic.
 
    .. exn:: No matching clauses for match.
 
-      No pattern can be used and, in particular, there is no :n:`_` pattern.
+      For at least one of the focused goals, there is no branch that matches
+      its pattern *and* gets at least one success for :n:`@ltac_expr`.
 
    .. exn:: Argument of match does not evaluate to a term.
 
-      This happens when :n:`@ltac_expr` does not denote a term.
+      This happens when :n:`@ltac_expr__term` does not denote a term.
 
-   .. tacv:: multimatch @ltac_expr with {+| @cpattern__i => @ltac_expr__i} end
+.. _match_vs_lazymatch_ex:
 
-      Using multimatch instead of match will allow subsequent tactics to
-      backtrack into a right-hand side tactic which has backtracking points
-      left and trigger the selection of a new matching branch when all the
-      backtracking points of the right-hand side have been consumed.
+   .. example:: Comparison of lazymatch and match
 
-      The syntax :n:`match …` is, in fact, a shorthand for :n:`once multimatch …`.
+      In :tacn:`lazymatch`, if :token:`ltac_expr` fails, the :tacn:`lazymatch` fails;
+      it doesn't look for further matches.  In :tacn:`match`, if :token:`ltac_expr` fails
+      in a matching branch, it will try to match on subsequent branches.
 
-   .. tacv:: lazymatch @ltac_expr with {+| @cpattern__i => @ltac_expr__i} end
+      .. coqtop:: reset none
 
-      Using lazymatch instead of match will perform the same pattern
-      matching procedure but will commit to the first matching branch
-      rather than trying a new matching if the right-hand side fails. If
-      the right-hand side of the selected branch is a tactic with
-      backtracking points, then subsequent failures cause this tactic to
-      backtrack.
+         Goal True.
 
-   .. tacv:: context @ident [@cpattern]
+      .. coqtop:: all
 
-      This special form of patterns matches any term with a subterm matching
-      cpattern. If there is a match, the optional :n:`@ident` is assigned the "matched
-      context", i.e. the initial term where the matched subterm is replaced by a
-      hole. The example below will show how to use such term contexts.
+         Fail lazymatch True with
+         | True => idtac "branch 1"; fail
+         | _ => idtac "branch 2"
+         end.
 
-      If the evaluation of the right-hand-side of a valid match fails, the next
-      matching subterm is tried. If no further subterm matches, the next clause
-      is tried. Matching subterms are considered top-bottom and from left to
-      right (with respect to the raw printing obtained by setting the
-      :flag:`Printing All` flag).
+      .. coqtop:: all
 
-   .. example::
+         match True with
+         | True => idtac "branch 1"; fail
+         | _ => idtac "branch 2"
+         end.
 
-      .. coqtop:: all abort
+.. _match_vs_multimatch_ex:
+
+   .. example:: Comparison of match and multimatch
+
+      :tacn:`match` tactics are only evaluated once, whereas :tacn:`multimatch`
+      tactics may be evaluated more than once if the following constructs trigger backtracking:
+
+      .. coqtop:: all
+
+         Fail match True with
+         | True => idtac "branch 1"
+         | _ => idtac "branch 2"
+         end ;
+         idtac "branch A"; fail.
+
+      .. coqtop:: all
+
+         Fail multimatch True with
+         | True => idtac "branch 1"
+         | _ => idtac "branch 2"
+         end ;
+         idtac "branch A"; fail.
+
+.. _match_with_holes_ex:
+
+   .. example:: Matching a pattern with holes
+
+      Notice the :tacn:`idtac` prints ``(z + 1)`` while the :tacn:`pose` substitutes
+      ``(x + 1)``.
 
-         Ltac f x :=
-           match x with
-             context f [S ?X] =>
-             idtac X;                    (* To display the evaluation order *)
-             assert (p := eq_refl 1 : X=1);    (* To filter the case X=1 *)
-             let x:= context f[O] in assert (x=O) (* To observe the context *)
+      .. coqtop:: in reset
+
+         Goal True.
+
+      .. coqtop:: all
+
+           match constr:(fun x => (x + 1) * 3) with
+           | fun z => ?y * 3 => idtac "y =" y; pose (fun z: nat => y * 5)
            end.
+
+.. _match_term_context_ex:
+
+   .. example:: Multiple matches for a "context" pattern.
+
+      Internally "x <> y" is represented as "(not x y)", which produces the
+      first match.
+
+      .. coqtop:: in reset
+
+         Ltac f t := match t with
+                    | context [ (not ?t) ] => idtac "?t = " t; fail
+                    | _ => idtac
+                    end.
          Goal True.
-         f (3+4).
+
+      .. coqtop:: all
+
+         f ((not True) <> (not False)).
 
 .. _ltac-match-goal:
 
-Pattern matching on goals
-~~~~~~~~~~~~~~~~~~~~~~~~~
+Pattern matching on goals and hypotheses: match goal
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+.. tacn:: @match_key {? reverse } goal with {? %| } {+| @goal_pattern => @ltac_expr } end
+   :name: lazymatch goal; match goal; multimatch goal
+
+   .. insertprodn goal_pattern match_hyp
+
+   .. prodn::
+      goal_pattern ::= {*, @match_hyp } |- @match_pattern
+      | [ {*, @match_hyp } |- @match_pattern ]
+      | _
+      match_hyp ::= @name : @match_pattern
+      | @name := @match_pattern
+      | @name := [ @match_pattern ] : @match_pattern
+
+   :tacn:`lazymatch goal`, :tacn:`match goal` and :tacn:`multimatch goal` are :token:`l1_tactic`\s.
+
+   Use this form to match hypotheses and/or goals in the proof context.  These patterns have zero or
+   more subpatterns to match hypotheses followed by a subpattern to match the conclusion.  Except for the
+   differences noted below, this works the same as the corresponding :n:`@match_key @ltac_expr` construct
+   (see :tacn:`match`).  Each current goal is processed independently.
 
-We can perform pattern matching on goals using the following expression:
-
-.. we should provide the full grammar here
-
-.. tacn:: match goal with {+| {+, @context_hyp} |- @cpattern => @ltac_expr } | _ => @ltac_expr end
-   :name: match goal
-
-   If each hypothesis pattern :n:`hyp`\ :sub:`1,i`, with i = 1, ..., m\ :sub:`1` is
-   matched (non-linear first-order unification) by a hypothesis of the
-   goal and if :n:`cpattern_1` is matched by the conclusion of the goal,
-   then :n:`@ltac_expr__1` is evaluated to :n:`v__1` by substituting the
-   pattern matching to the metavariables and the real hypothesis names
-   bound to the possible hypothesis names occurring in the hypothesis
-   patterns. If :n:`v__1` is a tactic value, then it is applied to the
-   goal. If this application fails, then another combination of hypotheses
-   is tried with the same proof context pattern. If there is no other
-   combination of hypotheses then the second proof context pattern is tried
-   and so on. If the next to last proof context pattern fails then
-   the last :n:`@ltac_expr` is evaluated to :n:`v` and :n:`v` is
-   applied. Note also that matching against subterms (using the :n:`context
-   @ident [ @cpattern ]`) is available and is also subject to yielding several
-   matchings.
-
-   Failures in subsequent tactics do not cause backtracking to select new
-   branches or combinations of hypotheses, or inside the right-hand side of
-   the selected branch even if it has backtracking points.
+   :n:`{*, @match_hyp }`
+      Patterns to match with hypotheses.  Each pattern must match a distinct hypothesis in order
+      for the branch to match.
+
+      Hypotheses have the form :n:`@name {? := @term__binder } : @type`.  Patterns bind each of
+      these nonterminals separately:
+
+      .. list-table::
+         :widths: 2 1
+         :header-rows: 1
+
+         * - Pattern syntax
+           - Example pattern
+
+         * - :n:`@name : @match_pattern__type`
+           - `n : ?t`
+
+         * - :n:`@name := @match_pattern__binder`
+           - `n := ?b`
+
+         * - :n:`@name := @term__binder : @type`
+           - `n := ?b : ?t`
+
+         * - :n:`@name := [ @match_pattern__binder ] : @match_pattern__type`
+           - `n := [ ?b ] : ?t`
+
+      ..
+
+         :token:`name` can't have a `?`.  Note that the last two forms are equivalent except that:
+
+         - if the `:` in the third form has been bound to something else in a notation, you must use the fourth form.
+           Note that cmd:`Require Import` `ssreflect` loads a notation that does this.
+         - a :n:`@term__binder` such as `[ ?l ]` (e.g., denoting a singleton list after
+           :cmd:`Import` `ListNotations`) must be parenthesized or, for the fourth form,
+           use double brackets: `[ [ ?l ] ]`.
+
+         :n:`@term__binder`\s in the form `[?x ; ?y]` for a list is not parsed correctly.  The workaround is
+         to add parentheses or to use the underlying term instead of the notation, i.e. `(cons ?x ?y)`.
+
+      If there are multiple :token:`match_hyp`\s in a branch, there may be multiple ways to match them to hypotheses.
+      For :tacn:`match goal` and :tacn:`multimatch goal`, if the evaluation of the :token:`ltac_expr` fails,
+      matching will continue with the next hypothesis combination.  When those are exhausted,
+      the next alternative from any `context` constructs in the :token:`match_pattern`\s is tried and then,
+      when the context alternatives are exhausted, the next branch is tried.
+      :ref:`Example<match_goal_multiple_hyps_ex>`.
+
+   `reverse`
+      Hypothesis matching for :token:`match_hyp`\s normally begins by matching them from left to right,
+      to hypotheses, last to first.  Specifying `reverse` begins matching in the reverse order, from
+      first to last.  :ref:`Normal<match_goal_hyps_ex>` and :ref:`reverse<match_goal_hyps_rev_ex>` examples.
+
+   :n:`|- @match_pattern`
+      A pattern to match with the current goal
+
+   :n:`@goal_pattern with [ ... ]`
+      The square brackets don't affect the semantics.  They are permitted for aesthetics.
 
    .. exn:: No matching clauses for match goal.
 
       No clause succeeds, i.e. all matching patterns, if any, fail at the
-      application of the right-hand-side.
+      application of the :token:`ltac_expr`.
 
-   .. note::
+Examples:
+
+.. _match_goal_hyps_ex:
+
+   .. example:: Matching hypotheses
+
+      Hypotheses are matched from the last hypothesis (which is by default the newest
+      hypothesis) to the first until the :tacn:`apply` succeeds.
+
+      .. coqtop:: reset all
+
+         Goal forall A B : Prop, A -> B -> (A->B).
+         intros.
+         match goal with
+         | H : _ |- _ => idtac "apply " H; apply H
+         end.
+
+.. _match_goal_hyps_rev_ex:
 
-      It is important to know that each hypothesis of the goal can be matched
-      by at most one hypothesis pattern. The order of matching is the
-      following: hypothesis patterns are examined from right to left
-      (i.e. hyp\ :sub:`i,m`\ :sub:`i`` before hyp\ :sub:`i,1`). For each
-      hypothesis pattern, the goal hypotheses are matched in order (newest
-      first), but it possible to reverse this order (oldest first)
-      with the :n:`match reverse goal with` variant.
+   .. example:: Matching hypotheses with reverse
 
-   .. tacv:: multimatch goal with {+| {+, @context_hyp} |- @cpattern => @ltac_expr } | _ => @ltac_expr end
+      Hypotheses are matched from the first hypothesis to the last until the :tacn:`apply` succeeds.
 
-      Using :n:`multimatch` instead of :n:`match` will allow subsequent tactics
-      to backtrack into a right-hand side tactic which has backtracking points
-      left and trigger the selection of a new matching branch or combination of
-      hypotheses when all the backtracking points of the right-hand side have
-      been consumed.
+      .. coqtop:: reset all
 
-      The syntax :n:`match [reverse] goal …` is, in fact, a shorthand for
-      :n:`once multimatch [reverse] goal …`.
+         Goal forall A B : Prop, A -> B -> (A->B).
+         intros.
+         match reverse goal with
+         | H : _ |- _ => idtac "apply " H; apply H
+         end.
 
-   .. tacv:: lazymatch goal with {+| {+, @context_hyp} |- @cpattern => @ltac_expr } | _ => @ltac_expr end
+.. _match_goal_multiple_hyps_ex:
 
-      Using lazymatch instead of match will perform the same pattern matching
-      procedure but will commit to the first matching branch with the first
-      matching combination of hypotheses rather than trying a new matching if
-      the right-hand side fails. If the right-hand side of the selected branch
-      is a tactic with backtracking points, then subsequent failures cause
-      this tactic to backtrack.
+   .. example:: Multiple ways to match hypotheses
+
+      Every possible match for the hypotheses is evaluated until the right-hand
+      side succeeds.  Note that `H1` and `H2` are never matched to the same hypothesis.
+      Observe that the number of permutations can grow as the factorial
+      of the number of hypotheses and hypothesis patterns.
+
+      .. coqtop:: reset all
+
+         Goal forall A B : Prop, A -> B -> (A->B).
+         intros A B H.
+         match goal with
+         | H1 : _, H2 : _ |- _ => idtac "match " H1 H2; fail
+         | _ => idtac
+         end.
+
+   .. todo need examples for:
+      match_context_rule ::= [ {*, @match_hyp } |- @match_pattern ] => @ltac_expr
+      match_hyp ::= | @name := {? [ @match_pattern ] : } @match_pattern
+
+.. todo PR The following items (up to numgoals) are part of "value_tactic".  I'd like to make
+   this a subsection and explain that they all return values.  How do I get a 5th-level section title?
 
 Filling a term context
 ~~~~~~~~~~~~~~~~~~~~~~
@@ -962,11 +1469,12 @@ Filling a term context
 The following expression is not a tactic in the sense that it does not
 produce subgoals but generates a term to be used in tactic expressions:
 
-.. tacn:: context @ident [@ltac_expr]
+.. tacn:: context @ident [ @term ]
+
+   Returns the term matched with the `context` pattern (described :ref:`here<match_term_context>`)
+   substituting :token:`term` for the hole created by the pattern.
 
-   :n:`@ident` must denote a context variable bound by a context pattern of a
-   match expression. This expression evaluates replaces the hole of the
-   value of :n:`@ident` by the value of :n:`@ltac_expr`.
+   :tacn:`context` is a :token:`value_tactic`.
 
    .. exn:: Not a context variable.
       :undocumented:
@@ -974,78 +1482,116 @@ produce subgoals but generates a term to be used in tactic expressions:
    .. exn:: Unbound context identifier @ident.
       :undocumented:
 
+   .. example:: Substituting a matched context
+
+      .. coqtop:: reset all
+
+         Goal True /\ True.
+         match goal with
+         | |- context G [True] => let x := context G [False] in idtac x
+         end.
+
 Generating fresh hypothesis names
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-Tactics sometimes have to generate new names for hypothesis. Letting the
-system decide a name with the intro tactic is not so good since it is
-very awkward to retrieve the name the system gave. The following
+Tactics sometimes need to generate new names for hypothesis.  Letting |Coq|
+choose a name with the intro tactic is not so good since it is
+very awkward to retrieve that name. The following
 expression returns an identifier:
 
-.. tacn:: fresh {* @component}
+.. tacn:: fresh {* {| @string | @qualid } }
+
+   .. todo you can't have a :tacn: with the same name as a :gdef: for now,
+      eg `fresh` can't be both
+
+   Returns a fresh identifier name (i.e. one that is not already used in the context
+   and not previously returned by :tacn:`fresh` in the current :token:`ltac_expr`).
+   The fresh identifier is formed by concatenating the final :token:`ident` of each :token:`qualid`
+   (dropping any qualified components) and each specified :token:`string`.
+   If the resulting name is already used, a number is appended to make it fresh.
+   If no arguments are given, the name is a fresh derivative of the name ``H``.
+
+   .. note:: We recommend generating the fresh identifier immediately before
+      adding it in the proof context.  Using :tacn:`fresh` in a local function
+      may not work as you expect:
+
+      Successive :tacn:`fresh`\es give distinct names even if the names haven't
+      yet been added to the proof context:
+
+      .. coqtop:: reset none
+
+         Goal True -> True.
+
+      .. coqtop:: out
+
+         intro x.
+
+      .. coqtop:: all
+
+         let a := fresh "x" in
+         let b := fresh "x" in
+         idtac a b.
+
+      When applying :tacn:`fresh` in a function, the name is chosen based on the
+      tactic context at the point where the function was defined:
 
-   It evaluates to an identifier unbound in the goal. This fresh identifier
-   is obtained by concatenating the value of the :n:`@component`\ s (each of them
-   is, either a :n:`@qualid` which has to refer to a (unqualified) name, or
-   directly a name denoted by a :n:`@string`).
+      .. coqtop:: all
+
+         let a := fresh "x" in
+         let f := fun _ => fresh "x" in
+         let c := f () in
+         let d := f () in
+         idtac a c d.
 
-   If the resulting name is already used, it is padded with a number so that it
-   becomes fresh. If no component is given, the name is a fresh derivative of
-   the name ``H``.
+   :tacn:`fresh` is a :token:`value_tactic`.
 
-Computing in a constr
-~~~~~~~~~~~~~~~~~~~~~
+Computing in a term: eval
+~~~~~~~~~~~~~~~~~~~~~~~~~
 
 Evaluation of a term can be performed with:
 
 .. tacn:: eval @red_expr in @term
 
-   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`.
+   :tacn:`eval` is a :token:`value_tactic`.
 
-Recovering the type of a term
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Getting the type of a term
+~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 .. tacn:: type of @term
 
    This tactic returns the type of :token:`term`.
 
-Manipulating untyped terms
-~~~~~~~~~~~~~~~~~~~~~~~~~~
+   :tacn:`type of` is a :token:`value_tactic`.
 
-.. tacn:: uconstr : @term
+Manipulating untyped terms: type_term
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-   The terms built in |Ltac| are well-typed by default. It may not be
-   appropriate for building large terms using a recursive |Ltac| function: the
-   term has to be entirely type checked at each step, resulting in potentially
-   very slow behavior. It is possible to build untyped terms using |Ltac| with
-   the :n:`uconstr : @term` syntax.
+The :n:`uconstr : ( @term )` construct can be used to build an untyped term.
+See :token:`syn_value`.
 
-.. tacn:: type_term @term
+.. tacn:: type_term @one_term
 
-   An untyped term, in |Ltac|, can contain references to hypotheses or to
+   In |Ltac|, an untyped term can contain references to hypotheses or to
    |Ltac| variables containing typed or untyped terms. An untyped term can be
-   type checked using the function type_term whose argument is parsed as an
+   type checked with :tacn:`type_term` whose argument is parsed as an
    untyped term and returns a well-typed term which can be used in tactics.
 
-Untyped terms built using :n:`uconstr :` can also be used as arguments to the
-:tacn:`refine` tactic. In that case the untyped term is type
-checked against the conclusion of the goal, and the holes which are not solved
-by the typing procedure are turned into new subgoals.
+   :tacn:`type_term` is a :token:`value_tactic`.
 
-Counting the goals
-~~~~~~~~~~~~~~~~~~
+Counting goals: numgoals
+~~~~~~~~~~~~~~~~~~~~~~~~
 
 .. tacn:: numgoals
 
    The number of goals under focus can be recovered using the :n:`numgoals`
-   function. Combined with the guard command below, it can be used to
+   function. Combined with the :tacn:`guard` tactic below, it can be used to
    branch over the number of goals produced by previous tactics.
 
+   :tacn:`numgoals` is a :token:`value_tactic`.
+
    .. example::
 
-      .. coqtop:: in
+      .. coqtop:: reset in
 
          Ltac pr_numgoals := let n := numgoals in idtac "There are" n "goals".
 
@@ -1056,18 +1602,29 @@ Counting the goals
 
          all:pr_numgoals.
 
-Testing boolean expressions
-~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Testing boolean expressions: guard
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. tacn:: guard @test
+.. tacn:: guard @int_or_var @comparison @int_or_var
    :name: guard
 
-   The :tacn:`guard` tactic tests a boolean expression, and fails if the expression
-   evaluates to false. If the expression evaluates to true, it succeeds
-   without affecting the proof.
+   .. insertprodn comparison comparison
+
+   .. prodn::
+      comparison ::= =
+      | <
+      | <=
+      | >
+      | >=
+
+   Tests a boolean expression.  If the expression evaluates to true,
+   it succeeds without affecting the proof.  The tactic fails if the
+   expression is false.
 
    The accepted tests are simple integer comparisons.
 
+   .. todo why doesn't it support = and <> as well?
+
    .. example::
 
       .. coqtop:: in
@@ -1083,63 +1640,54 @@ Testing boolean expressions
    .. exn:: Condition not satisfied.
       :undocumented:
 
-Proving a subgoal as a separate lemma
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Proving a subgoal as a separate lemma: abstract
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. tacn:: abstract @ltac_expr
-   :name: abstract
+.. tacn:: abstract @ltac_expr2 {? using @ident__name }
 
-   From the outside, :n:`abstract @ltac_expr` is the same as :n:`solve @ltac_expr`.
-   Internally it saves an auxiliary lemma called ``ident_subproofn`` where
-   ``ident`` is the name of the current goal and ``n`` is chosen so that this is
-   a fresh name. Such an auxiliary lemma is inlined in the final proof term.
+   Does a :tacn:`solve` :n:`[ @ltac_expr2 ]` and saves the subproof as an auxiliary lemma.
+   if :n:`@ident__name` is specified, the lemma is saved with that name; otherwise
+   the lemma is saved with the name :n:`@ident`\ `_subproof`\ :n:`{? @num }` where
+   :token:`ident` is the name of the current goal (e.g. the theorem name) and :token:`num`
+   is chosen to get a fresh name.  If the proof is closed with :cmd:`Qed`, the auxiliary lemma
+   is inlined in the final proof term.
 
-   This tactical is useful with tactics such as :tacn:`omega` or
-   :tacn:`discriminate` that generate huge proof terms. With that tool the user
-   can avoid the explosion at time of the Save command without having to cut
-   manually the proof in smaller lemmas.
+   This is useful with tactics such as :tacn:`omega` or
+   :tacn:`discriminate` that generate huge proof terms with many intermediate
+   goals.  It can significantly reduce peak memory use.  In most cases it doesn't
+   have a significant impact on run time.  One case in which it can reduce run time
+   is when a tactic `foo` is known to always pass type checking when it
+   succeeds, such as in reflective proofs.  In this case, the idiom
+   ":tacn:`abstract` :tacn:`exact_no_check` `foo`" will save half the type
+   checking type time compared to ":tacn:`exact` `foo`".
 
-   It may be useful to generate lemmas minimal w.r.t. the assumptions they
-   depend on. This can be obtained thanks to the option below.
+   :tacn:`abstract` is an :token:`l3_tactic`.
 
    .. warning::
 
       The abstract tactic, while very useful, still has some known
-      limitations, see https://github.com/coq/coq/issues/9146 for more
-      details. Thus we recommend using it caution in some
-      "non-standard" contexts. In particular, ``abstract`` won't
-      properly work when used inside quotations ``ltac:(...)``, or
-      if used as part of typeclass resolution, it may produce wrong
-      terms when in universe polymorphic mode.
-
-   .. tacv:: abstract @ltac_expr using @ident
-
-      Give explicitly the name of the auxiliary lemma.
-
-      .. warning::
-
-         Use this feature at your own risk; explicitly named and reused subterms
-         don’t play well with asynchronous proofs.
-
-   .. tacv:: transparent_abstract @ltac_expr
-      :name: transparent_abstract
-
-      Save the subproof in a transparent lemma rather than an opaque one.
+      limitations.  See `#9146 <https://github.com/coq/coq/issues/9146>`_ for more
+      details. We recommend caution when using it in some
+      "non-standard" contexts. In particular, ``abstract`` doesn't
+      work properly when used inside quotations ``ltac:(...)``.
+      If used as part of typeclass resolution, it may produce incorrect
+      terms when in polymorphic universe mode.
 
-      .. warning::
+   .. warning::
 
-         Use this feature at your own risk; building computationally relevant
-         terms with tactics is fragile.
+      Provide :n:`@ident__name` at your own risk; explicitly named and reused subterms
+      don’t play well with asynchronous proofs.
 
-   .. tacv:: transparent_abstract @ltac_expr using @ident
+.. tacn:: transparent_abstract @ltac_expr3 {? using @ident }
 
-      Give explicitly the name of the auxiliary transparent lemma.
+   Like :tacn:`abstract`, but save the subproof in a transparent lemma with a name in
+   the form :n:`@ident`\ :n:`_subterm`\ :n:`{? @num }`.
 
-      .. warning::
+   .. warning::
 
-         Use this feature at your own risk; building computationally relevant terms
-         with tactics is fragile, and explicitly named and reused subterms
-         don’t play well with asynchronous proofs.
+      Use this feature at your own risk; building computationally relevant terms
+      with tactics is fragile, and explicitly named and reused subterms
+      don’t play well with asynchronous proofs.
 
    .. exn:: Proof is not complete.
       :name: Proof is not complete. (abstract)
@@ -1148,37 +1696,59 @@ Proving a subgoal as a separate lemma
 Tactic toplevel definitions
 ---------------------------
 
-Defining |Ltac| functions
-~~~~~~~~~~~~~~~~~~~~~~~~~
+Defining |Ltac| symbols
+~~~~~~~~~~~~~~~~~~~~~~~
 
-Basically, |Ltac| toplevel definitions are made as follows:
+|Ltac| toplevel definitions are made as follows:
 
-.. cmd:: {? Local} Ltac @ident {* @ident} := @ltac_expr
+.. cmd:: Ltac @tacdef_body {* with @tacdef_body }
    :name: Ltac
 
-   This defines a new |Ltac| function that can be used in any tactic
-   script or new |Ltac| toplevel definition.
+   .. insertprodn tacdef_body tacdef_body
+
+   .. prodn::
+      tacdef_body ::= @qualid {* @name } {| := | ::= } @ltac_expr
+
+   Defines or redefines an |Ltac| symbol.
 
-   If preceded by the keyword ``Local``, the tactic definition will not be
+   If the :attr:`local` attribute is specified, the definition will not be
    exported outside the current module.
 
-   .. note::
+   :token:`qualid`
+      Name of the symbol being defined or redefined
+
+   :n:`{* @name }`
+      If specified, the symbol defines a function with the given parameter names.
+      If no names are specified, :token:`qualid` is assigned the value of :token:`ltac_expr`.
 
-      The preceding definition can equivalently be written:
+   `:=`
+      Defines a user-defined symbol, but gives an error if the symbol has already
+      been defined.
 
-      :n:`Ltac @ident := fun {+ @ident} => @ltac_expr`
+.. todo apparent inconsistency: "Ltac intros := idtac" seems like it redefines/hides an existing tactic,
+      but in fact it creates a tactic which can only be called by it's qualified name.  This is true in general
+      of tactic notations.  The only way to overwrite most primitive tactics, and any user-defined tactic
+      notation, is with another tactic notation.
+      .. exn:: There is already an Ltac named @qualid
+         :undocumented:
 
-   .. cmdv:: Ltac @ident {* @ident} {* with @ident {* @ident}} := @ltac_expr
+   `::=`
+      Redefines an existing user-defined symbol, but gives an error if the
+      symbol doesn't exist.  Note that :cmd:`Tactic Notation`\s
+      do not count as user-defined tactics for `::=`.  If :attr:`local` is not
+      specified, the redefinition applies across module boundaries.
 
-      This syntax allows recursive and mutual recursive function definitions.
+      .. exn: There is no Ltac named @qualid
 
-   .. cmdv:: Ltac @qualid {* @ident} ::= @ltac_expr
+   :n:`{* with @tacdef_body }`
+      Permits definition of mutually recursive tactics.
 
-      This syntax *redefines* an existing user-defined tactic.
+   .. note::
 
-      A previous definition of qualid must exist in the environment. The new
-      definition will always be used instead of the old one and it goes across
-      module boundaries.
+      The following definitions are equivalent:
+
+      - :n:`Ltac @qualid {+ @name } := @ltac_expr`
+      - :n:`Ltac @qualid := fun {+ @name } => @ltac_expr`
 
 Printing |Ltac| tactics
 ~~~~~~~~~~~~~~~~~~~~~~~
@@ -1596,17 +2166,16 @@ Backtraces
    to find out what went wrong. It is disabled by default for performance
    reasons.
 
-Info trace
-~~~~~~~~~~
+Tracing execution
+~~~~~~~~~~~~~~~~~
 
 .. cmd:: Info @num @ltac_expr
-   :name: Info
 
-   This command can be used to print the trace of the path eventually taken by an
-   |Ltac| script. That is, the list of executed tactics, discarding
-   all the branches which have failed. To that end the :cmd:`Info` command can be
-   used with the following syntax.
+   Applies :token:`ltac_expr` and prints a trace of the tactics that were successfully
+   applied, discarding branches that failed.
+   :tacn:`idtac` tactics appear in the trace as comments containing the output.
 
+   This command is valid only in proof mode.  It accepts :ref:`goal-selectors`.
 
    The number :n:`@num` is the unfolding level of tactics in the trace. At level
    0, the trace contains a sequence of tactics in the actual script, at level 1,
@@ -1705,13 +2274,17 @@ performance issue.
 
    This flag enables and disables the profiler.
 
-.. cmd:: Show Ltac Profile
+.. cmd:: Show Ltac Profile {? {| CutOff @int | @string } }
+
+   Prints the profile.
 
-   Prints the profile
+   :n:`CutOff @int`
+      By default, tactics that account for less than 2% of the total time are not displayed.
+      `CutOff` lets you specify a different percentage.
 
-   .. cmdv:: Show Ltac Profile @string
+   :n:`@string`
 
-      Prints a profile for all tactics that start with :n:`@string`. Append a period
+      Limits the profile to all tactics that start with :n:`@string`. Append a period
       (.) to the string if you only want exactly that name.
 
 .. cmd:: Reset Ltac Profile
@@ -1769,22 +2342,14 @@ performance issue.
 .. tacn:: reset ltac profile
    :name: reset ltac profile
 
-   This tactic behaves like the corresponding vernacular command
-   and allow displaying and resetting the profile from tactic scripts for
-   benchmarking purposes.
-
-.. tacn:: show ltac profile
-   :name: show ltac profile
-
-   This tactic behaves like the corresponding vernacular command
-   and allow displaying and resetting the profile from tactic scripts for
-   benchmarking purposes.
+   Equivalent to the :cmd:`Reset Ltac Profile` command, which allows
+   resetting the profile from tactic scripts for benchmarking purposes.
 
-.. tacn:: show ltac profile @string
+.. tacn:: show ltac profile {? {| cutoff @int | @string } }
    :name: show ltac profile
 
-   This tactic behaves like the corresponding vernacular command
-   and allow displaying and resetting the profile from tactic scripts for
+   Equivalent to the :cmd:`Show Ltac Profile` command,
+   which allows displaying the profile from tactic scripts for
    benchmarking purposes.
 
 .. warn:: Ltac Profiler encountered an invalid stack (no \
@@ -1809,6 +2374,13 @@ Run-time optimization tactic
 .. tacn:: optimize_heap
    :name: optimize_heap
 
-   This tactic behaves like :n:`idtac`, except that running it compacts the
+   This tactic behaves like :tacn:`idtac`, except that running it compacts the
    heap in the OCaml run-time system. It is analogous to the Vernacular
    command :cmd:`Optimize Heap`.
+
+.. tacn:: infoH @ltac_expr3
+
+   Used internally by Proof General.  See `#12423 <https://github.com/coq/coq/issues/12423>`_ for
+   some background.
+
+   :tacn:`infoH` is an :token:`l3_tactic`.
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index df5e4737b9..00aafe1266 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -90,7 +90,7 @@ list of assertion commands is given in :ref:`Assertions`. The command
 .. cmd:: Save @ident
    :name: Save
 
-   Forces the name of the original goal to be :token:`ident`.
+   Saves a completed proof with the name :token:`ident`.
 
 .. cmd:: Admitted
 
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 9ee61a801a..7b3670164b 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -1336,7 +1336,7 @@ Discharge
 The general syntax of the discharging tactical ``:`` is:
 
 .. tacn:: @tactic {? @ident } : {+ @d_item } {? @clear_switch }
-   :name: ... : ... (ssreflect)
+   :name: … : … (ssreflect)
    :undocumented:
 
 .. prodn::
@@ -5658,7 +5658,7 @@ respectively.
 
    application (see :ref:`the_defective_tactics_ssr`)
 
-.. tacv:: abstract
+.. tacv:: abstract: {+ @d_item}
 
    see :ref:`abstract_ssr` and :ref:`generating_let_ssr`
 
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 3fec940fad..6290620ee1 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -83,7 +83,7 @@ specified, the default selector is used.
    single focused goal or with a local selector (’’strict focusing
    mode’’).
 
-   Although more selectors are available, only ``all``, ``!`` or a
+   Although other selectors are available, only ``all``, ``!`` or a
    single natural number are valid default goal selectors.
 
 .. _bindingslist:
@@ -268,7 +268,7 @@ These patterns can be used when the hypothesis is an equality:
   :ref:`Example <intropattern_2stars_ex>`
 
 * :n:`@simple_intropattern_closed {* % @term}` — first applies each of the terms
-  with the :tacn:`apply ... in` tactic on the hypothesis to be introduced, then it uses
+  with the :tacn:`apply … in` tactic on the hypothesis to be introduced, then it uses
   :n:`@simple_intropattern_closed`.
   :ref:`Example <intropattern_injection_ex>`
 
@@ -851,10 +851,10 @@ Applying theorems
 .. flag:: Universal Lemma Under Conjunction
 
    This flag, which preserves compatibility with versions of Coq prior to
-   8.4 is also available for :n:`apply @term in @ident` (see :tacn:`apply ... in`).
+   8.4 is also available for :n:`apply @term in @ident` (see :tacn:`apply … in`).
 
 .. tacn:: apply @term in @ident
-   :name: apply ... in
+   :name: apply … in
 
    This tactic applies to any goal. The argument :token:`term` is a term
    well-formed in the local context and the argument :token:`ident` is an
@@ -897,18 +897,18 @@ Applying theorems
 
    .. tacv:: eapply {+, @term {? with @bindings_list } } in @ident
 
-      This works as :tacn:`apply ... in` but turns unresolved bindings into
+      This works as :tacn:`apply … in` but turns unresolved bindings into
       existential variables, if any, instead of failing.
 
    .. tacv:: apply {+, @term {? with @bindings_list } } in @ident as @simple_intropattern
-      :name: apply ... in ... as
+      :name: apply … in … as
 
-      This works as :tacn:`apply ... in` then applies the :token:`simple_intropattern`
+      This works as :tacn:`apply … in` then applies the :token:`simple_intropattern`
       to the hypothesis :token:`ident`.
 
    .. tacv:: simple apply @term in @ident
 
-      This behaves like :tacn:`apply ... in` but it reasons modulo conversion
+      This behaves like :tacn:`apply … in` but it reasons modulo conversion
       only on subterms that contain no variables to instantiate. For instance,
       if :g:`id := fun x:nat => x` and :g:`H: forall y, id y = y -> True` and
       :g:`H0 : O = O` then :g:`simple apply H in H0` does not succeed because it
@@ -1107,9 +1107,9 @@ Managing the local context
       or at the bottom of the local context. All hypotheses on which the new
       hypothesis depends are moved too so as to respect the order of
       dependencies between hypotheses. It is equivalent to :n:`intro {? @ident__1 }`
-      followed by the appropriate call to :tacn:`move ... after ...`,
-      :tacn:`move ... before ...`, :tacn:`move ... at top`,
-      or :tacn:`move ... at bottom`.
+      followed by the appropriate call to :tacn:`move … after …`,
+      :tacn:`move … before …`, :tacn:`move … at top`,
+      or :tacn:`move … at bottom`.
 
       .. note::
 
@@ -1119,7 +1119,7 @@ Managing the local context
          :undocumented:
 
 .. tacn:: intros @intropattern_list
-   :name: intros ...
+   :name: intros …
 
    Introduces one or more variables or hypotheses from the goal by matching the
    intro patterns.  See the description in :ref:`intropatterns`.
@@ -1127,7 +1127,7 @@ Managing the local context
 .. tacn:: eintros @intropattern_list
    :name: eintros
 
-   Works just like :tacn:`intros ...` except that it creates existential variables
+   Works just like :tacn:`intros …` except that it creates existential variables
    for any unresolved variables rather than failing.
 
 .. tacn:: clear @ident
@@ -1194,7 +1194,7 @@ Managing the local context
       hypotheses that depend on it.
 
 .. tacn:: move @ident__1 after @ident__2
-   :name: move ... after ...
+   :name: move … after …
 
    This moves the hypothesis named :n:`@ident__1` in the local context after
    the hypothesis named :n:`@ident__2`, where “after” is in reference to the
@@ -1212,23 +1212,23 @@ Managing the local context
    dependencies.
 
    .. tacv:: move @ident__1 before @ident__2
-      :name: move ... before ...
+      :name: move … before …
 
       This moves :n:`@ident__1` towards and just before the hypothesis
-      named :n:`@ident__2`.  As for :tacn:`move ... after ...`, dependencies
+      named :n:`@ident__2`.  As for :tacn:`move … after …`, dependencies
       over :n:`@ident__1` (when :n:`@ident__1` comes before :n:`@ident__2` in
       the order of dependencies) or in the type of :n:`@ident__1`
       (when :n:`@ident__1` comes after :n:`@ident__2` in the order of
       dependencies) are moved too.
 
    .. tacv:: move @ident at top
-      :name: move ... at top
+      :name: move … at top
 
       This moves :token:`ident` at the top of the local context (at the beginning
       of the context).
 
    .. tacv:: move @ident at bottom
-      :name: move ... at bottom
+      :name: move … at bottom
 
       This moves :token:`ident` at the bottom of the local context (at the end of
       the context).
@@ -1765,7 +1765,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
       chaining destruction of a hypothesis.
 
    .. tacv:: destruct @term eqn:@naming_intropattern
-      :name: destruct ... eqn:
+      :name: destruct … eqn:
 
       This behaves as :n:`destruct @term` but adds an equation
       between :token:`term` and the value that it takes in each of the
@@ -1894,7 +1894,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
 
 .. exn:: Unable to find an instance for the variables @ident ... @ident.
 
-   Use in this case the variant :tacn:`elim ... with` below.
+   Use in this case the variant :tacn:`elim … with` below.
 
 .. tacv:: induction @term as @or_and_intropattern_loc
 
@@ -1907,7 +1907,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
    name from the list :n:`p`:sub:`i1` :n:`... p`:sub:`in` in order. If there are
    not enough names, induction invents names for the remaining variables to
    introduce. More generally, the :n:`p`:sub:`ij` can be any
-   disjunctive/conjunctive introduction pattern (see :tacn:`intros ...`). For
+   disjunctive/conjunctive introduction pattern (see :tacn:`intros …`). For
    instance, for an inductive type with  one constructor, the pattern notation
    :n:`(p`:sub:`1` :n:`, ... , p`:sub:`n` :n:`)` can be used instead of
    :n:`[ p`:sub:`1` :n:`... p`:sub:`n` :n:`]`.
@@ -1926,7 +1926,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
    later, in the same way as :tacn:`eapply` does.
 
 .. tacv:: induction @term using @term
-   :name: induction ... using ...
+   :name: induction … using …
 
    This behaves as :tacn:`induction`  but using :n:`@term` as induction scheme.
    It does not expect the conclusion of the type of the first :n:`@term` to be
@@ -1934,7 +1934,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
 
 .. tacv:: induction @term using @term with @bindings_list
 
-   This behaves as :tacn:`induction ... using ...` but also providing instances
+   This behaves as :tacn:`induction … using …` but also providing instances
    for the premises of the type of the second :n:`@term`.
 
 .. tacv:: induction {+, @term} using @qualid
@@ -1985,7 +1985,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
    lemma applies and fails otherwise.
 
 .. tacv:: elim @term with @bindings_list
-   :name: elim ... with
+   :name: elim … with
 
    Allows to give explicit instances to the premises of the type of :n:`@term`
    (see :ref:`bindings list <bindingslist>`).
@@ -2434,7 +2434,7 @@ and an explanation of the underlying technique.
    :n:`dependent inversion_clear @ident`.
 
 .. tacv:: dependent inversion @ident with @term
-   :name: dependent inversion ... with ...
+   :name: dependent inversion … with …
 
    This variant allows you to specify the generalization of the goal. It is
    useful when the system fails to generalize the goal automatically. If
@@ -2449,7 +2449,7 @@ and an explanation of the underlying technique.
 
 .. tacv:: dependent inversion_clear @ident with @term
 
-   Like :tacn:`dependent inversion ... with ...` with but clears :n:`@ident` from the
+   Like :tacn:`dependent inversion … with …` with but clears :n:`@ident` from the
    local context.
 
 .. tacv:: dependent inversion_clear @ident as @or_and_intropattern_loc with @term
@@ -2468,9 +2468,12 @@ and an explanation of the underlying technique.
    This allows naming the hypotheses introduced in the context by
    ``simple inversion``.
 
-.. tacv:: inversion @ident using @ident
+.. tacn:: inversion @ident using @ident
    :name: inversion ... using ...
 
+   .. todo using … instead of ... in the name above gives a Sphinx error, even though
+      this works just find for :tacn:`move … after …`
+
    Let :n:`@ident` have type :g:`(I t)` (:g:`I` an inductive predicate) in the
    local context, and :n:`@ident` be a (dependent) inversion lemma. Then, this
    tactic refines the current goal with the specified lemma.
@@ -2993,7 +2996,7 @@ Performing computations
    | fold {+ @one_term }
    | pattern {+, @pattern_occ }
    | @ident
-   delta_flag ::= {? - } [ {+ @smart_qualid } ]
+   delta_flag ::= {? - } [ {+ @reference } ]
    strategy_flag ::= {+ @red_flags }
    | @delta_flag
    red_flags ::= beta
@@ -3003,13 +3006,13 @@ Performing computations
    | cofix
    | zeta
    | delta {? @delta_flag }
-   ref_or_pattern_occ ::= @smart_qualid {? at @occs_nums }
+   ref_or_pattern_occ ::= @reference {? at @occs_nums }
    | @one_term {? at @occs_nums }
    occs_nums ::= {+ {| @num | @ident } }
    | - {| @num | @ident } {* @int_or_var }
    int_or_var ::= @int
    | @ident
-   unfold_occ ::= @smart_qualid {? at @occs_nums }
+   unfold_occ ::= @reference {? at @occs_nums }
    pattern_occ ::= @one_term {? at @occs_nums }
 
 This set of tactics implements different specialized usages of the
@@ -3418,7 +3421,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
 
    This is the most general syntax that combines the different variants.
 
-.. tacn:: with_strategy @strategy_level_or_var [ {+ @smart_qualid } ] @ltac_expr3
+.. tacn:: with_strategy @strategy_level_or_var [ {+ @reference } ] @ltac_expr3
    :name: with_strategy
 
    Executes :token:`ltac_expr3`, applying the alternate unfolding
@@ -4710,32 +4713,9 @@ Automating
       The goal is not of the form :g:`t = u`. Especially note that :tacn:`btauto`
       doesn't introduce variables into the context on its own.
 
-.. tacn:: ring
-   :name: ring
-
-   This tactic solves equations upon polynomial expressions of a ring
-   (or semiring) structure. It proceeds by normalizing both hand sides
-   of the equation (w.r.t. associativity, commutativity and
-   distributivity, constant propagation) and comparing syntactically the
-   results.
-
-.. tacn:: ring_simplify {* @term}
-   :name: ring_simplify
-
-   This tactic applies the normalization procedure described above to
-   the given terms. The tactic then replaces all occurrences of the terms
-   given in the conclusion of the goal by their normal forms. If no term
-   is given, then the conclusion should be an equation and both hand
-   sides are normalized.
-
-See :ref:`Theringandfieldtacticfamilies` for more information on
-the tactic and how to declare new ring structures. All declared field structures
-can be printed with the ``Print Rings`` command.
-
-.. tacn:: field
+.. tacv:: field
           field_simplify {* @term}
           field_simplify_eq
-   :name: field; field_simplify; field_simplify_eq
 
    The field tactic is built on the same ideas as ring: this is a
    reflexive tactic that solves or simplifies equations in a field
@@ -4801,8 +4781,8 @@ Non-logical tactics
    :name: swap
 
    This tactic switches the position of the goals of indices :n:`@num` and
-   :n:`@num`. If either :n:`@num` or :n:`@num` is negative then goals are
-   counted from the end of the focused goal list. Goals are indexed from 1,
+   :n:`@num`.  Negative values for:n:`@num` indicate counting goals
+   backward from the end of the focused goal list. Goals are indexed from 1,
    there is no goal with position 0.
 
 .. example::
@@ -4917,7 +4897,7 @@ Performance-oriented tactic variants
 .. tacn:: change_no_check @term
    :name: change_no_check
 
-   For advanced usage. Similar to :n:`change @term`, but as an optimization,
+   For advanced usage. Similar to :tacn:`change` :n:`@term`, but as an optimization,
    it skips checking that :n:`@term` is convertible to the goal.
 
    Recall that the Coq kernel typechecks proofs again when they are concluded to
@@ -4929,7 +4909,7 @@ Performance-oriented tactic variants
    indeed convertible to the goal.
 
    In the following example, :tacn:`change_no_check` replaces :g:`False` by
-   :g:`True`, but :g:`Qed` then rejects the proof, ensuring consistency.
+   :g:`True`, but :cmd:`Qed` then rejects the proof, ensuring consistency.
 
    .. example::
 
@@ -4940,7 +4920,7 @@ Performance-oriented tactic variants
            exact I.
          Fail Qed.
 
-   :tacn:`change_no_check` supports all of `change`'s variants.
+   :tacn:`change_no_check` supports all of :tacn:`change`'s variants.
 
    .. tacv:: change_no_check @term with @term’
       :undocumented:
@@ -4971,9 +4951,9 @@ Performance-oriented tactic variants
 .. tacn:: exact_no_check @term
    :name: exact_no_check
 
-   For advanced usage. Similar to :n:`exact @term`, but as an optimization,
+   For advanced usage. Similar to :tacn:`exact` :n:`@term`, but as an optimization,
    it skips checking that :n:`@term` has the goal's type, relying on the kernel
-   check instead. See :tacn:`change_no_check` for more explanations.
+   check instead. See :tacn:`change_no_check` for more explanation.
 
    .. example::
 
@@ -4986,7 +4966,7 @@ Performance-oriented tactic variants
    .. tacv:: vm_cast_no_check @term
       :name: vm_cast_no_check
 
-      For advanced usage. Similar to :n:`exact_no_check @term`, but additionally
+      For advanced usage. Similar to :tacn:`exact_no_check` :n:`@term`, but additionally
       instructs the kernel to use :tacn:`vm_compute` to compare the
       goal's type with the :n:`@term`'s type.
 
@@ -5001,7 +4981,7 @@ Performance-oriented tactic variants
    .. tacv:: native_cast_no_check @term
       :name: native_cast_no_check
 
-      for advanced usage. similar to :n:`exact_no_check @term`, but additionally
+      for advanced usage. similar to :tacn:`exact_no_check` :n:`@term`, but additionally
       instructs the kernel to use :tacn:`native_compute` to compare the goal's
       type with the :n:`@term`'s type.
 
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 3db9d2e80c..ad0aab19b5 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -11,14 +11,14 @@ Displaying
 
 .. _Print:
 
-.. cmd:: Print {? Term } @smart_qualid {? @univ_name_list }
+.. cmd:: Print {? Term } @reference {? @univ_name_list }
 
    .. insertprodn univ_name_list univ_name_list
 
    .. prodn::
       univ_name_list ::= @%{ {* @name } %}
 
-   Displays definitions of terms, including opaque terms, for the object :n:`@smart_qualid`.
+   Displays definitions of terms, including opaque terms, for the object :n:`@reference`.
 
    * :n:`Term` - a syntactic marker to allow printing a term
      that is the same as one of the various :n:`Print` commands.  For example,
@@ -26,7 +26,7 @@ Displaying
      information on the object whose name is ":n:`All`".
 
    * :n:`@univ_name_list` - locally renames the
-     polymorphic universes of :n:`@smart_qualid`.
+     polymorphic universes of :n:`@reference`.
      The name `_` means the usual name is printed.
 
    .. exn:: @qualid not a defined object.
@@ -65,14 +65,14 @@ If no selector is provided,
 the command applies to the current goal.  If no proof is open, then the command only applies
 to accessible objects.  (see Section :ref:`invocation-of-tactics`).
 
-.. cmd:: About @smart_qualid {? @univ_name_list }
+.. cmd:: About @reference {? @univ_name_list }
 
-   Displays information about the :n:`@smart_qualid` object, which,
+   Displays information about the :n:`@reference` object, which,
    if a proof is open,  may be a hypothesis of the selected goal,
    or an accessible theorem, axiom, etc.:
    its kind (module, constant, assumption, inductive,
    constructor, abbreviation, …), long name, type, implicit arguments and
-   argument scopes (as set in the definition of :token:`smart_qualid` or
+   argument scopes (as set in the definition of :token:`reference` or
    subsequently with the :cmd:`Arguments` command). It does not print the body of definitions or proofs.
 
 .. cmd:: Check @term
@@ -120,10 +120,10 @@ to accessible objects.  (see Section :ref:`invocation-of-tactics`).
 
    :n:`- @search_query`
       Excludes the objects that would be filtered by
-      :n:`@search_query`.  Cf. :ref:`this example
+      :n:`@search_query`.  See :ref:`this example
       <search-disambiguate-notation>`.
 
-   :n:`[ @search_query ... @search_query | ... | @search_query ... @search_query ]`
+   :n:`[ {+ @search_query } | ... | {+ @search_query } ]`
       This is a disjunction of conjunctions of queries.  A simple
       conjunction can be expressed by having a single disjunctive
       branch.  For a conjunction at top-level, the surrounding
@@ -146,48 +146,45 @@ to accessible objects.  (see Section :ref:`invocation-of-tactics`).
       pattern :n:`@one_term`.  Holes of the pattern are indicated by
       `_` or :n:`?@ident`.  If the same :n:`?@ident` occurs more than
       once in the pattern, all occurrences in the subterm must be
-      identical.  Cf. :ref:`this example <search-pattern>`.
+      identical.  See :ref:`this example <search-pattern>`.
 
    :n:`@string {? % @scope_key }`
       - If :n:`@string` is a substring of a valid identifier and no
         :n:`% @scope_key` is provided, search for objects whose name
-        contains :n:`@string`.  Cf. :ref:`this example
+        contains :n:`@string`.  See :ref:`this example
         <search-part-ident>`.
 
-      - If :n:`@string` is not a substring of a valid identifier or if
-        the optional :n:`% @scope_key` is provided, search for objects
+      - Otherwise, search for objects
         whose type contains the reference that this string,
-        interpreted as a notation, is attached to (as in
-        :n:`@smart_qualid`).  Cf. :ref:`this example
-        <search-by-notation>`.
+        interpreted as a notation, is attached to (as described in
+        :n:`@reference`).  See :ref:`this example <search-by-notation>`.
 
-      .. note::
+     .. note::
 
-         If the string is a substring of a valid identifier but you
-         still want to look for a reference by notation, you can put
-         it between single quotes or provide a scope explictly.
-         Cf. :ref:`this example <search-disambiguate-notation>`.
+        To refer to a string used in a notation that is a substring of a valid identifier,
+        put it between single quotes or explicitly provide a scope.
+        See :ref:`this example <search-disambiguate-notation>`.
 
    :n:`hyp:`
       The provided pattern or reference is matched against any subterm
-      of an hypothesis of the type of the objects.  Cf. :ref:`this
+      of an hypothesis of the type of the objects.  See :ref:`this
       example <search-hyp>`.
 
    :n:`headhyp:`
       The provided pattern or reference is matched against the
       subterms in head position (any partial applicative subterm) of
-      the hypotheses of the type of the objects.  Cf. :ref:`the
+      the hypotheses of the type of the objects.  See :ref:`the
       previous example <search-hyp>`.
 
    :n:`concl:`
       The provided pattern or reference is matched against any subterm
-      of the conclusion of the type of the objects.  Cf. :ref:`this
+      of the conclusion of the type of the objects.  See :ref:`this
       example <search-concl>`.
 
    :n:`headconcl:`
       The provided pattern or reference is matched against the
       subterms in head position (any partial applicative subterm) of
-      the conclusion of the type of the objects.  Cf. :ref:`the
+      the conclusion of the type of the objects.  See :ref:`the
       previous example <search-concl>`.
 
    :n:`head:`
@@ -197,24 +194,17 @@ to accessible objects.  (see Section :ref:`invocation-of-tactics`).
       .. insertprodn logical_kind logical_kind
 
       .. prodn::
-         logical_kind ::= @thm_token
-         | @assumption_token
-         | Context
-         | Definition
-         | Example
-         | Coercion
-         | Instance
-         | Scheme
-         | Canonical
-         | Field
-         | Method
-         | Primitive
+         logical_kind ::= {| @thm_token | @assumption_token }
+         | {| Definition | Example | Context | Primitive }
+         | {| Coercion | Instance | Scheme | Canonical | SubClass }
+         | {| Field | Method }
 
       Filters objects by the keyword that was used to define them
       (`Theorem`, `Lemma`, `Axiom`, `Variable`, `Context`,
       `Primitive`...) or its status (`Coercion`, `Instance`, `Scheme`,
-      `Canonical`, `Field` for record fields, `Method` for class
-      fields).  Cf. :ref:`this example <search-by-keyword>`.
+      `Canonical`, `SubClass`, Field` for record fields, `Method` for class
+      fields).  Note that `Coercion`\s, `Canonical Structure`\s, Instance`\s and `Scheme`\s can be
+      defined without using those keywords.  See :ref:`this example <search-by-keyword>`.
 
    Additional clauses:
 
@@ -415,7 +405,7 @@ to accessible objects.  (see Section :ref:`invocation-of-tactics`).
 Requests to the environment
 -------------------------------
 
-.. cmd:: Print Assumptions @smart_qualid
+.. cmd:: Print Assumptions @reference
 
    Displays all the assumptions (axioms, parameters and
    variables) a theorem or definition depends on.
@@ -423,41 +413,44 @@ Requests to the environment
    The message "Closed under the global context" indicates that the theorem or
    definition has no dependencies.
 
-.. cmd:: Print Opaque Dependencies @smart_qualid
+.. cmd:: Print Opaque Dependencies @reference
 
-   Displays the assumptions and opaque constants that :n:`@smart_qualid` depends on.
+   Displays the assumptions and opaque constants that :n:`@reference` depends on.
 
-.. cmd:: Print Transparent Dependencies @smart_qualid
+.. cmd:: Print Transparent Dependencies @reference
 
-   Displays the assumptions and  transparent constants that :n:`@smart_qualid` depends on.
+   Displays the assumptions and  transparent constants that :n:`@reference` depends on.
 
-.. cmd:: Print All Dependencies @smart_qualid
+.. cmd:: Print All Dependencies @reference
 
-   Displays all the assumptions and constants :n:`@smart_qualid` depends on.
+   Displays all the assumptions and constants :n:`@reference` depends on.
 
-.. cmd:: Locate @smart_qualid
+.. cmd:: Locate @reference
 
-   .. insertprodn smart_qualid by_notation
+   .. insertprodn reference reference
 
    .. prodn::
-      smart_qualid ::= @qualid
-      | @by_notation
-      by_notation ::= @string {? % @scope_key }
+      reference ::= @qualid
+      | @string {? % @scope_key }
 
    Displays the full name of objects from |Coq|'s various qualified namespaces such as terms,
-   modules and Ltac.  It also displays notation definitions.
+   modules and Ltac, thereby showing the module they are defined in.  It also displays notation definitions.
 
-   If the argument is:
+   :n:`@qualid`
+     refers to object names that end with :n:`@qualid`.
 
-   * :n:`@qualid` - displays the full name of objects that
-     end with :n:`@qualid`, thereby showing the module they are defined in.
-   * :n:`@string {? "%" @ident }` - displays the definition of a notation.  :n:`@string`
+   :n:`@string {? % @scope_key }`
+     refers to definitions of notations.  :n:`@string`
      can be a single token in the notation such as "`->`" or a pattern that matches the
      notation.  See :ref:`locating-notations`.
 
+     :n:`% @scope_key`, if present, limits the reference to the scope bound to the delimiting
+     key :n:`@scope_key`, such as, for example, :n:`%nat`.  (see Section
+     :ref:`LocalInterpretationRulesForNotations`)
+
    .. todo somewhere we should list all the qualified namespaces
 
-.. cmd:: Locate Term @smart_qualid
+.. cmd:: Locate Term @reference
 
    Like :cmd:`Locate`, but limits the search to terms
 
@@ -587,13 +580,13 @@ file is a particular case of a module called a *library file*.
    several files match, one of them is picked in an unspecified fashion.
    Therefore, library authors should use a unique name for each module and
    users are encouraged to use fully-qualified names
-   or the :cmd:`From ... Require` command to load files.
+   or the :cmd:`From … Require` command to load files.
 
 
    .. todo common user error on dirpaths see https://github.com/coq/coq/pull/11961#discussion_r402852390
 
    .. cmd:: From @dirpath Require {? {| Import | Export } } {+ @qualid }
-      :name: From ... Require
+      :name: From … Require
 
       Works like :cmd:`Require`, but loads, for each :n:`@qualid`,
       the library whose fully-qualified name matches :n:`@dirpath.{* @ident . }@qualid`
@@ -626,7 +619,7 @@ file is a particular case of a module called a *library file*.
    .. exn:: The file @ident.vo contains library @qualid__1 and not library @qualid__2.
 
       The library :n:`@qualid__2` is indirectly required by a :cmd:`Require` or
-      :cmd:`From ... Require` command.  The loadpath maps :n:`@qualid__2` to :n:`@ident.vo`,
+      :cmd:`From … Require` command.  The loadpath maps :n:`@qualid__2` to :n:`@ident.vo`,
       which was compiled using a loadpath that bound it to :n:`@qualid__1`.  Usually
       the appropriate solution is to recompile :n:`@ident.v` using the correct loadpath.
       See :ref:`libraries-and-filesystem`.
@@ -738,10 +731,10 @@ the toplevel, and using them in source files is discouraged.
    (cf. :cmd:`Declare ML Module`).
 
 
-.. _backtracking:
+.. _backtracking_subsection:
 
 Backtracking
-----------------
+------------
 
 The backtracking commands described in this section can only be used
 interactively, they cannot be part of a vernacular file loaded via
@@ -980,7 +973,7 @@ as numbers, and for reflection-based tactics. The commands to fine-
 tune the reduction strategies and the lazy conversion algorithm are
 described first.
 
-.. cmd:: Opaque {+ @smart_qualid }
+.. cmd:: Opaque {+ @reference }
 
    This command accepts the :attr:`global` attribute.  By default, the scope
    of :cmd:`Opaque` is limited to the current section or module.
@@ -989,7 +982,7 @@ described first.
    defined by :cmd:`Definition` or :cmd:`Let` (with an explicit body), or by a command
    assimilated to a definition such as :cmd:`Fixpoint`, :cmd:`Program Definition`, etc,
    or by a proof ended by :cmd:`Defined`. The command tells not to unfold the
-   constants in the :n:`@smart_qualid` sequence in tactics using δ-conversion (unfolding
+   constants in the :n:`@reference` sequence in tactics using δ-conversion (unfolding
    a constant is replacing it by its definition).
 
    :cmd:`Opaque` has also an effect on the conversion algorithm of |Coq|, telling
@@ -1002,7 +995,7 @@ described first.
       Sections :ref:`performingcomputations`, :ref:`tactics-automating`,
       :ref:`proof-editing-mode`
 
-.. cmd:: Transparent {+ @smart_qualid }
+.. cmd:: Transparent {+ @reference }
 
    This command accepts the :attr:`global` attribute.  By default, the scope
    of :cmd:`Transparent` is limited to the current section or module.
@@ -1029,7 +1022,7 @@ described first.
 
 .. _vernac-strategy:
 
-.. cmd:: Strategy {+ @strategy_level [ {+ @smart_qualid } ] }
+.. cmd:: Strategy {+ @strategy_level [ {+ @reference } ] }
 
    .. insertprodn strategy_level strategy_level_or_var
 
@@ -1048,7 +1041,7 @@ described first.
    This command generalizes the behavior of the :cmd:`Opaque` and :cmd:`Transparent`
    commands. It is used to fine-tune the strategy for unfolding
    constants, both at the tactic level and at the kernel level. This
-   command associates a :n:`@strategy_level` with the qualified names in the :n:`@smart_qualid`
+   command associates a :n:`@strategy_level` with the qualified names in the :n:`@reference`
    sequence. Whenever two
    expressions with two distinct head constants are compared (for
    instance, this comparison can be triggered by a type cast), the one
@@ -1069,10 +1062,10 @@ described first.
       like −∞)
     + ``transparent`` : Equivalent to level 0
 
-.. cmd:: Print Strategy @smart_qualid
+.. cmd:: Print Strategy @reference
 
-   This command prints the strategy currently associated with :n:`@smart_qualid`. It
-   fails if :n:`@smart_qualid` is not an unfoldable reference, that is, neither a
+   This command prints the strategy currently associated with :n:`@reference`. It
+   fails if :n:`@reference` is not an unfoldable reference, that is, neither a
    variable nor a constant.
 
    .. exn:: The reference is not unfoldable.
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 955f2055e4..3c92206fd2 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1747,18 +1747,18 @@ Tactic notations allow customizing the syntax of tactics.
 
    The nonterminals that can specified in the tactic notation are:
 
-   .. todo uconstr represents a type with holes.  At the moment uconstr doesn't
-      appear in the documented grammar.  Maybe worth ressurecting with a better name,
-      maybe "open_term"?
-      see https://github.com/coq/coq/pull/11718#discussion_r413721234
-
-   .. todo 'open_constr' appears to be another possible value based on the
-      the message from "Tactic Notation open_constr := idtac".
-      Also (at least) "ref", "string", "preident", "int" and "ssrpatternarg".
-      (from reading .v files).
-      Looks like any string passed to "make0" in the code is valid.  But do
-      we want to support all these?
-      @JasonGross's opinion here: https://github.com/coq/coq/pull/11718#discussion_r415387421
+     .. todo uconstr represents a type with holes.  At the moment uconstr doesn't
+        appear in the documented grammar.  Maybe worth ressurecting with a better name,
+        maybe "open_term"?
+        see https://github.com/coq/coq/pull/11718#discussion_r413721234
+
+     .. todo 'open_constr' appears to be another possible value based on the
+        the message from "Tactic Notation open_constr := idtac".
+        Also (at least) "ref", "string", "preident", "int" and "ssrpatternarg".
+        (from reading .v files).
+        Looks like any string passed to "make0" in the code is valid.  But do
+        we want to support all these?
+        @JasonGross's opinion here: https://github.com/coq/coq/pull/11718#discussion_r415387421
 
    .. list-table::
       :header-rows: 1
@@ -1789,7 +1789,7 @@ Tactic notations allow customizing the syntax of tactics.
         - :tacn:`unfold`
 
       * - ``smart_global``
-        - :token:`smart_qualid`
+        - :token:`reference`
         - a global reference of term
         - :tacn:`with_strategy`
 
@@ -1871,7 +1871,7 @@ Tactic notations allow customizing the syntax of tactics.
              entries can be used in primitive tactics or in other
              notations at places where a list of the underlying entry
              can be used: entry is either ``constr``, ``hyp``,
-             ``integer``, ``smart_qualid``, ``strategy_level``,
+             ``integer``, ``reference``, ``strategy_level``,
              ``strategy_level_or_var``, or ``int_or_var``.
 
 
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index a9a243868f..80f825358f 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -20,7 +20,7 @@ RENAME: [
 | Constr.constr_pattern constr_pattern
 | Constr.global global
 | Constr.lconstr lconstr
-| Constr.lconstr_pattern lconstr_pattern
+| Constr.lconstr_pattern cpattern
 | G_vernac.query_command query_command
 | G_vernac.section_subset_expr section_subset_expr
 | Pltac.tactic tactic
@@ -105,25 +105,24 @@ hyp: [
 | var
 ]
 
-ltac_expr_opt: [
-| OPT tactic_expr5
+tactic_then_last: [
+| REPLACE "|" LIST0 ( OPT tactic_expr5 ) SEP "|"
+| WITH LIST0 ( "|" ( OPT tactic_expr5 ) )
 ]
 
-ltac_expr_opt_list_or: [
-| ltac_expr_opt_list_or "|" ltac_expr_opt
-| ltac_expr_opt
+goal_tactics: [
+| LIST0 ( OPT tactic_expr5 ) SEP "|"
 ]
 
+tactic_then_gen: [ | DELETENT ]
+
 tactic_then_gen: [
-| EDIT ADD_OPT tactic_expr5 "|" tactic_then_gen
-| EDIT ADD_OPT tactic_expr5 ".." tactic_then_last
-| REPLACE OPT tactic_expr5 ".." tactic_then_last
-| WITH ltac_expr_opt ".." OPT "|" ltac_expr_opt_list_or
+| goal_tactics
+| OPT ( goal_tactics "|" ) OPT tactic_expr5 ".." OPT ( "|" goal_tactics )
 ]
 
-ltac_expr_opt_list_or: [
-| ltac_expr_opt_list_or "|" OPT tactic_expr5
-| OPT tactic_expr5
+tactic_then_last: [
+| OPTINREF
 ]
 
 reference: [ | DELETENT ]
@@ -240,13 +239,29 @@ scope_name: [
 ]
 
 scope: [
-| scope_name | scope_key
+| scope_name
+| scope_key
+]
+
+scope_delimiter: [
+| REPLACE "%" IDENT
+| WITH "%" scope_key
+]
+
+type: [
+| operconstr200
 ]
 
 operconstr100: [
-| MOVETO term_cast operconstr99 "<:" operconstr200
-| MOVETO term_cast operconstr99 "<<:" operconstr200
-| MOVETO term_cast operconstr99 ":" operconstr200
+| REPLACE operconstr99 "<:" operconstr200
+| WITH operconstr99 "<:" type
+| MOVETO term_cast operconstr99 "<:" type
+| REPLACE operconstr99 "<<:" operconstr200
+| WITH operconstr99 "<<:" type
+| MOVETO term_cast operconstr99 "<<:" type
+| REPLACE operconstr99 ":" operconstr200
+| WITH operconstr99 ":" type
+| MOVETO term_cast operconstr99 ":" type
 | MOVETO term_cast operconstr99 ":>"
 ]
 
@@ -335,10 +350,6 @@ open_binders: [
 | DELETE closed_binder binders
 ]
 
-type: [
-| operconstr200
-]
-
 closed_binder: [
 | name
 
@@ -468,8 +479,10 @@ gallina: [
 | WITH "Let" "CoFixpoint" corec_definition LIST0 ( "with" corec_definition )
 | REPLACE "Scheme" LIST1 scheme SEP "with"
 | WITH "Scheme" scheme LIST0 ( "with" scheme )
-| REPLACE "Primitive" identref OPT [ ":" lconstr ] ":=" register_token
-| WITH "Primitive" identref OPT [ ":" lconstr ] ":=" "#" identref
+]
+
+finite_token: [
+| DELETENT
 ]
 
 constructor_list_or_record_decl: [
@@ -583,6 +596,10 @@ gallina_ext: [
 | REPLACE "Canonical" OPT "Structure" by_notation
 | WITH "Canonical" OPT "Structure" smart_global
 
+| DELETE "Coercion" global ":" class_rawexpr ">->" class_rawexpr
+| REPLACE "Coercion" by_notation ":" class_rawexpr ">->" class_rawexpr
+| WITH "Coercion" smart_global ":" class_rawexpr ">->" class_rawexpr
+
 | REPLACE "Include" "Type" module_type_inl LIST0 ext_module_type
 | WITH "Include" "Type" LIST1 module_type_inl SEP "<+"
 
@@ -619,8 +636,20 @@ digit: [
 | "0" ".." "9"
 ]
 
+decnum: [
+| digit LIST0 [ digit | "_" ]
+]
+
+hexdigit: [
+| [ "0" ".." "9" | "a" ".." "f" | "A" ".." "F" ]
+]
+
+hexnum: [
+| [ "0x" | "0X" ] hexdigit LIST0 [ hexdigit | "_" ]
+]
+
 num: [
-| LIST1 digit
+| [ decnum | hexnum ]
 ]
 
 natural: [ | DELETENT ]
@@ -628,12 +657,13 @@ natural: [
 | num  (* todo: or should it be "nat"? *)
 ]
 
-numeral: [
-| LIST1 digit OPT ("." LIST1 digit) OPT [ [ "e" | "E" ] OPT [ "+" | "-" ] LIST1 digit ]
+int: [
+| OPT "-" num
 ]
 
-int: [
-| OPT "-" LIST1 digit
+numeral: [
+| OPT "-" decnum OPT ( "." LIST1 [ digit | "_" ] ) OPT ( [ "e" | "E" ] OPT [ "+" | "-" ] decnum )
+| OPT "-" hexnum OPT ( "." LIST1 [ hexdigit | "_" ] ) OPT ( [ "p" | "P" ] OPT [ "+" | "-" ] decnum )
 ]
 
 bigint: [
@@ -675,32 +705,100 @@ command_entry: [
 | noedit_mode
 ]
 
-tactic_expr1: [
-| EDIT match_key ADD_OPT "reverse" "goal" "with" match_context_list "end"
-| MOVETO ltac_match_goal match_key OPT "reverse" "goal" "with" match_context_list "end"
-| MOVETO ltac_match_term match_key tactic_expr5 "with" match_list "end"
-| REPLACE failkw [ int_or_var | ] LIST0 message_token
-| WITH failkw OPT int_or_var LIST0 message_token
-]
-
 DELETE: [
 | tactic_then_locality
 ]
 
+tactic_expr5: [
+(* make these look consistent with use of binder_tactic in other tactic_expr* *)
+| DELETE binder_tactic
+| DELETE tactic_expr4
+| [ tactic_expr4 | binder_tactic ]
+]
+
+ltac_constructs: [
+(* repeated in main ltac grammar - need to create a COPY edit *)
+| tactic_expr3 ";" [ tactic_expr3 | binder_tactic ]
+| tactic_expr3 ";" "[" tactic_then_gen "]"
+
+| tactic_expr1 "+" [ tactic_expr2 | binder_tactic ]
+| tactic_expr1 "||" [ tactic_expr2 | binder_tactic ]
+
+(* | qualid LIST0 tactic_arg  add later due renaming tactic_arg *)
+
+| "[>" tactic_then_gen "]"
+| toplevel_selector tactic_expr5
+]
+
 tactic_expr4: [
 | REPLACE tactic_expr3 ";" tactic_then_gen "]"
 | WITH tactic_expr3 ";" "[" tactic_then_gen "]"
-| tactic_expr3 ";" "[" ">" tactic_then_gen "]"
+| REPLACE tactic_expr3 ";" binder_tactic
+| WITH tactic_expr3 ";" [ tactic_expr3 | binder_tactic ]
+| DELETE tactic_expr3 ";" tactic_expr3
 ]
 
-match_context_list: [
-| EDIT ADD_OPT "|" LIST1 match_context_rule SEP "|"
+l3_tactic: [ ]
+
+tactic_expr3: [
+| DELETE "abstract" tactic_expr2
+| REPLACE "abstract" tactic_expr2 "using" ident
+| WITH "abstract" tactic_expr2 OPT ( "using" ident )
+| l3_tactic
+| MOVEALLBUT ltac_builtins
+| l3_tactic
+| tactic_expr2
+]
+
+l2_tactic: [ ]
+
+tactic_expr2: [
+| REPLACE tactic_expr1 "+" binder_tactic
+| WITH tactic_expr1 "+"  [ tactic_expr2 | binder_tactic ]
+| DELETE tactic_expr1 "+" tactic_expr2
+| REPLACE tactic_expr1 "||" binder_tactic
+| WITH tactic_expr1 "||" [ tactic_expr2 | binder_tactic ]
+| DELETE tactic_expr1 "||" tactic_expr2
+| MOVETO ltac_builtins "tryif" tactic_expr5 "then" tactic_expr5 "else" tactic_expr2
+| l2_tactic
+| DELETE ltac_builtins
 ]
 
-match_hyps: [
-| REPLACE name ":=" "[" match_pattern "]" ":" match_pattern
-| WITH name ":=" OPT ("[" match_pattern "]" ":") match_pattern
-| DELETE name ":=" match_pattern
+l1_tactic: [ ]
+
+tactic_expr1: [
+| EDIT match_key ADD_OPT "reverse" "goal" "with" match_context_list "end"
+| MOVETO simple_tactic match_key OPT "reverse" "goal" "with" match_context_list "end"
+| MOVETO simple_tactic match_key tactic_expr5 "with" match_list "end"
+| REPLACE failkw [ int_or_var | ] LIST0 message_token
+| WITH failkw OPT int_or_var LIST0 message_token
+| REPLACE reference LIST0 tactic_arg_compat
+| WITH reference LIST1 tactic_arg_compat
+| l1_tactic
+| DELETE simple_tactic
+| MOVEALLBUT ltac_builtins
+| l1_tactic
+| tactic_arg
+| reference LIST1 tactic_arg_compat
+| tactic_expr0
+]
+
+(* split match_context_rule *)
+goal_pattern: [
+| LIST0 match_hyps SEP "," "|-" match_pattern
+| "[" LIST0 match_hyps SEP "," "|-" match_pattern "]"
+| "_"
+]
+
+match_context_rule: [
+| DELETE LIST0 match_hyps SEP "," "|-" match_pattern "=>" tactic_expr5
+| DELETE "[" LIST0 match_hyps SEP "," "|-" match_pattern "]" "=>" tactic_expr5
+| DELETE "_" "=>" tactic_expr5
+| goal_pattern "=>" tactic_expr5
+]
+
+match_context_list: [
+| EDIT ADD_OPT "|" LIST1 match_context_rule SEP "|"
 ]
 
 match_list: [
@@ -708,12 +806,10 @@ match_list: [
 ]
 
 match_rule: [
-| REPLACE match_pattern "=>" tactic_expr5
-| WITH [ match_pattern | "_" ] "=>" tactic_expr5
+(* redundant; match_pattern -> term -> _ *)
 | DELETE "_" "=>" tactic_expr5
 ]
 
-
 selector_body: [
 | REPLACE range_selector_or_nth  (* depends on whether range_selector_or_nth is deleted first *)
 | WITH LIST1 range_selector SEP ","
@@ -892,7 +988,14 @@ simple_tactic: [
 | DELETE "congruence" "with" LIST1 constr
 | REPLACE "congruence" int "with" LIST1 constr
 | WITH "congruence" OPT int OPT ( "with" LIST1 constr )
-
+| DELETE "show" "ltac" "profile"
+| REPLACE "show" "ltac" "profile" "cutoff" int
+| WITH "show" "ltac" "profile" OPT [ "cutoff" int | string ]
+| DELETE "show" "ltac" "profile" string
+(* perversely, the mlg uses "tactic3" instead of "tactic_expr3" *)
+| DELETE "transparent_abstract" tactic3
+| REPLACE "transparent_abstract" tactic3 "using" ident
+| WITH "transparent_abstract" tactic_expr3 OPT ( "using" ident )
 ]
 
 (* todo: don't use DELETENT for this *)
@@ -1112,10 +1215,7 @@ numnotoption: [
 binder_tactic: [
 | REPLACE "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" tactic_expr5
 | WITH "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" tactic_expr5
-]
-
-tactic_then_gen: [
-| OPTINREF
+| MOVEALLBUT ltac_builtins
 ]
 
 record_binder_body: [
@@ -1496,11 +1596,6 @@ by_notation: [
 | WITH ne_string OPT [ "%" scope_key ]
 ]
 
-scope_delimiter: [
-| REPLACE "%" IDENT
-| WITH "%" scope_key
-]
-
 decl_notation: [
 | REPLACE ne_lstring ":=" constr only_parsing OPT [ ":" IDENT ]
 | WITH ne_lstring ":=" constr only_parsing OPT [ ":" scope_name ]
@@ -1517,6 +1612,186 @@ ltac_production_item: [
 | DELETE ident
 ]
 
+input_fun: [
+| DELETE ident
+| DELETE "_"
+| name
+]
+
+let_clause: [
+| DELETE identref ":=" tactic_expr5
+| REPLACE "_" ":=" tactic_expr5
+| WITH name  ":=" tactic_expr5
+]
+
+tactic_mode: [
+(* todo: make sure to document this production! *)
+(* deleting to allow splicing query_command into command *)
+| DELETE OPT toplevel_selector query_command
+| DELETE OPT ltac_selector OPT ltac_info tactic ltac_use_default
+| DELETE "par" ":" OPT ltac_info tactic ltac_use_default
+(* Ignore attributes (none apply) and "...". *)
+| ltac_info tactic
+| MOVETO command ltac_info tactic
+| DELETE command
+]
+
+RENAME: [
+| toplevel_selector toplevel_selector_temp
+]
+
+toplevel_selector: [
+| selector_body
+| "all"
+| "!"
+(* par is accepted even though it's not in the .mlg *)
+| "par"
+]
+
+toplevel_selector_temp: [
+| DELETE selector_body ":"
+| DELETE "all" ":"
+| DELETE "!" ":"
+| toplevel_selector ":"
+]
+
+(* not included in insertprodn; defined in rst with :production: *)
+control_command: [ ]
+
+(* move all commands under "command" *)
+
+DELETE: [
+| vernac
+]
+
+vernac_aux: [
+| DELETE gallina "."
+| DELETE gallina_ext "."
+| DELETE syntax "."
+| DELETE command_entry
+]
+
+command: [
+| gallina
+| gallina_ext
+| syntax
+| query_command
+| vernac_control
+| vernac_toplevel
+| command_entry
+]
+
+SPLICE: [
+| query_command
+]
+
+query_command: [ ] (* re-add as a placeholder *)
+
+sentence: [
+| OPT attributes command "."
+| OPT attributes OPT ( num ":" ) query_command "."
+| OPT attributes OPT ( toplevel_selector ":" ) tactic_expr5 [ "." | "..." ]
+| control_command
+]
+
+document: [
+| LIST0 sentence
+]
+
+(* add in ltac and Tactic Notation tactics that appear in the doc: *)
+ltac_defined_tactics: [
+| "classical_left"
+| "classical_right"
+| "contradict" ident
+| "discrR"
+| "easy"
+| "exfalso"
+| "inversion_sigma"
+| "lia"
+| "lra"
+| "nia"
+| "nra"
+| "split_Rabs"
+| "split_Rmult"
+| "tauto"
+| "time_constr" tactic_expr5
+| "zify"
+]
+
+(* todo: need careful review; assume that "[" ... "]" are literals *)
+tactic_notation_tactics: [
+| "assert_fails" tactic_expr3
+| "assert_succeeds" tactic_expr3
+| "field" OPT ( "[" LIST1 operconstr200 "]" )
+| "field_simplify" OPT ( "[" LIST1 operconstr200 "]" ) LIST1 operconstr200 OPT ( "in" ident )
+| "field_simplify_eq" OPT ( "[" LIST1 operconstr200 "]" ) OPT ( "in" ident )
+| "intuition" OPT tactic_expr5
+| "nsatz" OPT ( "with" "radicalmax" ":=" operconstr200 "strategy" ":=" operconstr200 "parameters" ":=" operconstr200 "variables" ":=" operconstr200 )
+| "psatz" operconstr200 OPT int_or_var
+| "ring" OPT ( "[" LIST1 operconstr200 "]" )
+| "ring_simplify" OPT ( "[" LIST1 operconstr200 "]" ) LIST1 operconstr200 OPT ( "in" ident )  (* todo: ident was "hyp", worth keeping? *)
+]
+
+(* defined in OCaml outside of mlgs *)
+tactic_arg: [
+| "uconstr" ":" "(" operconstr200 ")"
+| MOVEALLBUT simple_tactic
+]
+
+nonterminal: [ ]
+
+value_tactic: [ ]
+
+RENAME: [
+| tactic_arg tactic_value
+]
+
+syn_value: [
+| IDENT; ":" "(" nonterminal ")"
+]
+
+tactic_value: [
+| [ value_tactic | syn_value ]
+]
+
+simple_tactic: [
+| ltac_builtins
+| ltac_constructs
+| ltac_defined_tactics
+| tactic_notation_tactics
+]
+
+tacdef_body: [
+| REPLACE global LIST1 input_fun ltac_def_kind tactic_expr5
+| WITH global LIST0 input_fun ltac_def_kind tactic_expr5
+| DELETE global ltac_def_kind tactic_expr5
+]
+
+SPLICE: [
+| def_token
+| extended_def_token
+]
+
+logical_kind: [
+| DELETE thm_token
+| DELETE assumption_token
+| [ thm_token | assumption_token ]
+| DELETE "Definition"
+| DELETE "Example"
+| DELETE "Context"
+| DELETE "Primitive"
+(* SubClass was deleted from def_token *)
+| [ "Definition" | "Example" | "Context" | "Primitive" ]
+| DELETE "Coercion"
+| DELETE "Instance"
+| DELETE "Scheme"
+| DELETE "Canonical"
+| [  "Coercion" | "Instance" | "Scheme" | "Canonical" | "SubClass" ]
+| DELETE "Field"
+| DELETE "Method"
+| [ "Field" | "Method" ]
+]
+
 SPLICE: [
 | noedit_mode
 | bigint
@@ -1595,7 +1870,6 @@ SPLICE: [
 | glob
 | glob_constr_with_bindings
 | id_or_meta
-| lconstr_pattern
 | lglob
 | ltac_tacdef_body
 | mode
@@ -1640,7 +1914,6 @@ SPLICE: [
 | quoted_attributes  (* todo: splice or not? *)
 | printable
 | only_parsing
-| def_token
 | record_fields
 | constructor_type
 | record_binder
@@ -1678,15 +1951,25 @@ SPLICE: [
 | ltac_def_kind
 | intropatterns
 | instance_name
+| failkw
+| selector
 | ne_in_or_out_modules
 | search_queries
 | locatable
 | scope_delimiter
 | bignat
 | one_import_filter_name
-| register_token
 | search_where
-| extended_def_token
+| message_token
+| input_fun
+| tactic_then_last
+| ltac_use_default
+| toplevel_selector_temp
+| comment
+| register_token
+| match_context_rule
+| match_rule
+| by_notation
 ] (* end SPLICE *)
 
 RENAME: [
@@ -1714,15 +1997,14 @@ RENAME: [
 (*| impl_ident_tail impl_ident*)
 | ssexpr35 ssexpr (* strange in mlg, ssexpr50 is after this *)
 
-| tactic_then_gen multi_goal_tactics
-| selector only_selector
+| tactic_then_gen for_each_goal
 | selector_body selector
-| input_fun fun_var
 | match_hyps match_hyp
 
 | BULLET bullet
 | fix_decl fix_body
 | cofix_decl cofix_body
+(* todo: it's confusing that Constr.constr and constr are different things *)
 | constr one_term
 | appl_arg arg
 | rec_definition fix_definition
@@ -1734,7 +2016,7 @@ RENAME: [
 | constructor_list_or_record_decl constructors_or_record
 | record_binder_body field_body
 | class_rawexpr class
-| smart_global smart_qualid
+| smart_global reference
 (*
 | searchabout_query search_item
 *)
@@ -1745,109 +2027,47 @@ RENAME: [
 | constr_as_binder_kind binder_interp
 | syntax_extension_type explicit_subentry
 | numnotoption numeral_modifier
-]
-
-(* todo: doesn't work if up above... maybe because 'clause' doesn't exist? *)
-clause_dft_concl: [
-| OPTINREF
-]
-
-(* add in ltac and Tactic Notation tactics that appear in the doc: *)
-ltac_defined_tactics: [
-| "classical_left"
-| "classical_right"
-| "contradict" ident
-| "discrR"
-| "easy"
-| "exfalso"
-| "inversion_sigma"
-| "lia"
-| "lra"
-| "nia"
-| "nra"
-| "split_Rabs"
-| "split_Rmult"
-| "tauto"
-| "zify"
-]
-
-(* todo: need careful review; assume that "[" ... "]" are literals *)
-tactic_notation_tactics: [
-| "assert_fails" ltac_expr3
-| "assert_succeeds" ltac_expr3
-| "field" OPT ( "[" LIST1 term "]" )
-| "field_simplify" OPT ( "[" LIST1 term "]" ) LIST1 term OPT ( "in" ident )
-| "field_simplify_eq" OPT ( "[" LIST1 term "]" ) OPT ( "in" ident )
-| "intuition" OPT ltac_expr
-| "nsatz" OPT ( "with" "radicalmax" ":=" term "strategy" ":=" term "parameters" ":=" term "variables" ":=" term )
-| "psatz" term OPT int_or_var
-| "ring" OPT ( "[" LIST1 term "]" )
-| "ring_simplify" OPT ( "[" LIST1 term "]" ) LIST1 term OPT ( "in" ident )  (* todo: ident was "hyp", worth keeping? *)
-]
-
-tacticals: [
+| tactic_arg_compat tactic_arg
+| lconstr_pattern cpattern
 ]
 
 simple_tactic: [
-| ltac_defined_tactics
-| tactic_notation_tactics
-]
-
-(* move all commands under "command" *)
-
-DELETE: [
-| vernac
+(* due to renaming of tactic_arg; Use LIST1 for function application *)
+| qualid LIST1 tactic_arg
 ]
 
-tactic_mode: [
-(* todo: make sure to document this production! *)
-(* deleting to allow splicing query_command into command *)
-| DELETE OPT toplevel_selector query_command
-]
-
-vernac_aux: [
-| DELETE gallina "."
-| DELETE gallina_ext "."
-| DELETE syntax "."
-| DELETE command_entry
-]
-
-command: [
-| gallina
-| gallina_ext
-| syntax
-| query_command
-| vernac_control
-| vernac_toplevel
-| command_entry
+(* todo: doesn't work if up above... maybe because 'clause' doesn't exist? *)
+clause_dft_concl: [
+| OPTINREF
 ]
 
 SPLICE: [
 | gallina
 | gallina_ext
 | syntax
-| query_command
 | vernac_control
 | vernac_toplevel
 | command_entry
+| ltac_builtins
+| ltac_constructs
 | ltac_defined_tactics
 | tactic_notation_tactics
 ]
 (* todo: ssrreflect*.rst ref to fix_body is incorrect *)
 
-(* not included in insertprodn; defined in rst with :production: *)
-control_command: [ ]
-query_command: [ ] (* re-add since previously spliced *)
+REACHABLE: [
+| command
+| simple_tactic
+]
 
-sentence: [
-| OPT attributes command "."
-| OPT attributes OPT ( num ":" ) query_command "."
-| OPT attributes OPT toplevel_selector ltac_expr [ "." | "..." ]
-| control_command
+NOTINRSTS: [
+| simple_tactic
+| REACHABLE
+| NOTINRSTS
 ]
 
-document: [
-| LIST0 sentence
+REACHABLE: [
+| NOTINRSTS
 ]
 
 strategy_level: [
diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml
index 4d4ba28318..33c4bd3e01 100644
--- a/doc/tools/docgram/doc_grammar.ml
+++ b/doc/tools/docgram/doc_grammar.ml
@@ -779,7 +779,7 @@ let rec edit_prod g top edit_map prod =
         begin
           try let splice_prods = NTMap.find nt !g.map in
             match splice_prods with
-            | [] -> assert false
+            | [] -> error "Empty splice for '%s'\n" nt; []
             | [p] -> List.rev (remove_Sedit2 p)
             | _ -> [Sprod (List.map remove_Sedit2 splice_prods)]
           with Not_found -> error "Missing nt '%s' for splice\n" nt; [Snterm nt]
@@ -1828,10 +1828,10 @@ let process_rst g file args seen tac_prods cmd_prods =
     "doc/sphinx/language/core/sections.rst";
     "doc/sphinx/language/extensions/implicit-arguments.rst";
     "doc/sphinx/language/extensions/arguments-command.rst";
-    "doc/sphinx/language/using/libraries/funind.rst";
-
-    "doc/sphinx/language/gallina-specification-language.rst";
     "doc/sphinx/language/gallina-extensions.rst";
+    "doc/sphinx/language/gallina-specification-language.rst";
+    "doc/sphinx/language/using/libraries/funind.rst";
+    "doc/sphinx/proof-engine/ltac.rst";
     "doc/sphinx/proof-engine/vernacular-commands.rst";
     "doc/sphinx/user-extensions/syntax-extensions.rst"
   ]
@@ -2059,10 +2059,12 @@ let process_grammar args =
 
       let cmd_nts = ["command"] in
       (* TODO: need to handle tactic_mode (overlaps with query_command) and subprf *)
-      cmdReport "prodnCommands" "cmds" cmd_nts !seen.cmds !seen.cmdvs;
+      if args.check_cmds then
+        cmdReport "prodnCommands" "cmds" cmd_nts !seen.cmds !seen.cmdvs;
 
       let tac_nts = ["simple_tactic"] in
-      cmdReport "prodnTactics" "tacs" tac_nts !seen.tacs !seen.tacvs
+      if args.check_tacs then
+        cmdReport "prodnTactics" "tacs" tac_nts !seen.tacs !seen.tacvs
     end;
 
     (* generate prodnGrammar for reference *)
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 1b0a5c28ee..c5edb538b7 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -1425,7 +1425,7 @@ simple_tactic: [
 | "firstorder" OPT tactic firstorder_using "with" LIST1 preident
 | "gintuition" OPT tactic
 | "functional" "inversion" quantified_hypothesis OPT reference      (* funind plugin *)
-| "functional" "induction" LIST1 constr fun_ind_using with_names      (* funind plugin *)
+| "functional" "induction" lconstr fun_ind_using with_names      (* funind plugin *)
 | "soft" "functional" "induction" LIST1 constr fun_ind_using with_names      (* funind plugin *)
 | "reflexivity"
 | "exact" casted_constr
@@ -1591,7 +1591,6 @@ simple_tactic: [
 | "auto" OPT int_or_var auto_using hintbases
 | "info_auto" OPT int_or_var auto_using hintbases
 | "debug" "auto" OPT int_or_var auto_using hintbases
-| "prolog" "[" LIST0 uconstr "]" int_or_var
 | "eauto" OPT int_or_var OPT int_or_var auto_using hintbases
 | "new" "auto" OPT int_or_var auto_using hintbases
 | "debug" "eauto" OPT int_or_var OPT int_or_var auto_using hintbases
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 3a327fc748..f4bf51b6ba 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -4,14 +4,7 @@ to match editedGrammar, which will remove comments.  Not compiled into Coq *)
 DOC_GRAMMAR
 
 tactic_mode: [
-| OPT toplevel_selector "{"
-| OPT toplevel_selector OPT ( "Info" num ) ltac_expr ltac_use_default
-| "par" ":" OPT ( "Info" num ) ltac_expr ltac_use_default
-]
-
-ltac_use_default: [
-| "."
-| "..."
+| OPT ( toplevel_selector ":" ) "{"
 ]
 
 term: [
@@ -136,21 +129,34 @@ type: [
 ]
 
 numeral: [
-| LIST1 digit OPT ( "." LIST1 digit ) OPT [ [ "e" | "E" ] OPT [ "+" | "-" ] LIST1 digit ]
+| OPT "-" decnum OPT ( "." LIST1 [ digit | "_" ] ) OPT ( [ "e" | "E" ] OPT [ "+" | "-" ] decnum )
+| OPT "-" hexnum OPT ( "." LIST1 [ hexdigit | "_" ] ) OPT ( [ "p" | "P" ] OPT [ "+" | "-" ] decnum )
 ]
 
 int: [
-| OPT "-" LIST1 digit
+| OPT "-" num
 ]
 
 num: [
-| LIST1 digit
+| [ decnum | hexnum ]
+]
+
+decnum: [
+| digit LIST0 [ digit | "_" ]
 ]
 
 digit: [
 | "0" ".." "9"
 ]
 
+hexnum: [
+| [ "0x" | "0X" ] hexdigit LIST0 [ hexdigit | "_" ]
+]
+
+hexdigit: [
+| [ "0" ".." "9" | "a" ".." "f" | "A" ".." "F" ]
+]
+
 ident: [
 | first_letter LIST0 subsequent_letter
 ]
@@ -176,14 +182,29 @@ where: [
 | "before" ident
 ]
 
+REACHABLE: [
+| command
+| simple_tactic
+| NOTINRSTS
+]
+
+NOTINRSTS: [
+| simple_tactic
+| REACHABLE
+| NOTINRSTS
+]
+
 document: [
 | LIST0 sentence
 ]
 
+nonterminal: [
+]
+
 sentence: [
 | OPT attributes command "."
 | OPT attributes OPT ( num ":" ) query_command "."
-| OPT attributes OPT toplevel_selector ltac_expr [ "." | "..." ]
+| OPT attributes OPT ( toplevel_selector ":" ) ltac_expr [ "." | "..." ]
 | control_command
 ]
 
@@ -193,9 +214,6 @@ control_command: [
 query_command: [
 ]
 
-tacticals: [
-]
-
 attributes: [
 | LIST0 ( "#[" LIST0 attribute SEP "," "]" ) LIST0 legacy_attr
 ]
@@ -345,9 +363,9 @@ term_generalizing: [
 ]
 
 term_cast: [
-| term10 "<:" term
-| term10 "<<:" term
-| term10 ":" term
+| term10 "<:" type
+| term10 "<<:" type
+| term10 ":" type
 | term10 ":>"
 ]
 
@@ -440,7 +458,7 @@ red_expr: [
 ]
 
 delta_flag: [
-| OPT "-" "[" LIST1 smart_qualid "]"
+| OPT "-" "[" LIST1 reference "]"
 ]
 
 strategy_flag: [
@@ -459,7 +477,7 @@ red_flags: [
 ]
 
 ref_or_pattern_occ: [
-| smart_qualid OPT ( "at" occs_nums )
+| reference OPT ( "at" occs_nums )
 | one_term OPT ( "at" occs_nums )
 ]
 
@@ -474,22 +492,13 @@ int_or_var: [
 ]
 
 unfold_occ: [
-| smart_qualid OPT ( "at" occs_nums )
+| reference OPT ( "at" occs_nums )
 ]
 
 pattern_occ: [
 | one_term OPT ( "at" occs_nums )
 ]
 
-finite_token: [
-| "Inductive"
-| "CoInductive"
-| "Variant"
-| "Record"
-| "Structure"
-| "Class"
-]
-
 variant_definition: [
 | ident_decl LIST0 binder OPT [ "|" LIST0 binder ] OPT [ ":" type ] ":=" OPT "|" LIST1 constructor SEP "|" OPT decl_notations
 ]
@@ -538,11 +547,11 @@ cofix_definition: [
 ]
 
 scheme_kind: [
-| "Induction" "for" smart_qualid "Sort" sort_family
-| "Minimality" "for" smart_qualid "Sort" sort_family
-| "Elimination" "for" smart_qualid "Sort" sort_family
-| "Case" "for" smart_qualid "Sort" sort_family
-| "Equality" "for" smart_qualid
+| "Induction" "for" reference "Sort" sort_family
+| "Minimality" "for" reference "Sort" sort_family
+| "Elimination" "for" reference "Sort" sort_family
+| "Case" "for" reference "Sort" sort_family
+| "Equality" "for" reference
 ]
 
 sort_family: [
@@ -597,12 +606,8 @@ module_expr_inl: [
 | LIST1 module_expr_atom OPT functor_app_annot
 ]
 
-smart_qualid: [
+reference: [
 | qualid
-| by_notation
-]
-
-by_notation: [
 | string OPT [ "%" scope_key ]
 ]
 
@@ -679,9 +684,10 @@ command: [
 | "Cd" OPT string
 | "Load" OPT "Verbose" [ string | ident ]
 | "Declare" "ML" "Module" LIST1 string
-| "Locate" smart_qualid
-| "Locate" "Term" smart_qualid
+| "Locate" reference
+| "Locate" "Term" reference
 | "Locate" "Module" qualid
+| "Info" num ltac_expr
 | "Locate" "Ltac" qualid
 | "Locate" "Library" qualid
 | "Locate" "File" string
@@ -702,30 +708,30 @@ command: [
 | "Print" "Graph"
 | "Print" "Classes"
 | "Print" "TypeClasses"
-| "Print" "Instances" smart_qualid
+| "Print" "Instances" reference
 | "Print" "Coercions"
 | "Print" "Coercion" "Paths" class class
-| "Print" "Canonical" "Projections" LIST0 smart_qualid
+| "Print" "Canonical" "Projections" LIST0 reference
 | "Print" "Typing" "Flags"
 | "Print" "Tables"
 | "Print" "Options"
 | "Print" "Hint"
-| "Print" "Hint" smart_qualid
+| "Print" "Hint" reference
 | "Print" "Hint" "*"
 | "Print" "HintDb" ident
 | "Print" "Scopes"
 | "Print" "Scope" scope_name
 | "Print" "Visibility" OPT scope_name
-| "Print" "Implicit" smart_qualid
+| "Print" "Implicit" reference
 | "Print" OPT "Sorted" "Universes" OPT ( "Subgraph" "(" LIST0 qualid ")" ) OPT string
-| "Print" "Assumptions" smart_qualid
-| "Print" "Opaque" "Dependencies" smart_qualid
-| "Print" "Transparent" "Dependencies" smart_qualid
-| "Print" "All" "Dependencies" smart_qualid
-| "Print" "Strategy" smart_qualid
+| "Print" "Assumptions" reference
+| "Print" "Opaque" "Dependencies" reference
+| "Print" "Transparent" "Dependencies" reference
+| "Print" "All" "Dependencies" reference
+| "Print" "Strategy" reference
 | "Print" "Strategies"
 | "Print" "Registered"
-| "Print" OPT "Term" smart_qualid OPT univ_name_list
+| "Print" OPT "Term" reference OPT univ_name_list
 | "Print" "Module" "Type" qualid
 | "Print" "Module" qualid
 | "Print" "Namespace" dirpath
@@ -771,7 +777,7 @@ command: [
 | "Create" "HintDb" ident OPT "discriminated"
 | "Remove" "Hints" LIST1 qualid OPT ( ":" LIST1 ident )
 | "Hint" hint OPT ( ":" LIST1 ident )
-| "Comments" LIST0 comment
+| "Comments" LIST0 [ one_term | string | num ]
 | "Declare" "Instance" ident_decl LIST0 binder ":" term OPT hint_info
 | "Declare" "Scope" scope_name
 | "Obligation" int OPT ( "of" ident ) OPT ( ":" term OPT ( "with" ltac_expr ) )
@@ -903,21 +909,20 @@ command: [
 | "Export" LIST1 filtered_import
 | "Include" module_type_inl LIST0 ( "<+" module_expr_inl )
 | "Include" "Type" LIST1 module_type_inl SEP "<+"
-| "Transparent" LIST1 smart_qualid
-| "Opaque" LIST1 smart_qualid
-| "Strategy" LIST1 [ strategy_level "[" LIST1 smart_qualid "]" ]
+| "Transparent" LIST1 reference
+| "Opaque" LIST1 reference
+| "Strategy" LIST1 [ strategy_level "[" LIST1 reference "]" ]
 | "Canonical" OPT "Structure" ident_decl def_body
-| "Canonical" OPT "Structure" smart_qualid
+| "Canonical" OPT "Structure" reference
 | "Coercion" qualid OPT univ_decl def_body
 | "Identity" "Coercion" ident ":" class ">->" class
-| "Coercion" qualid ":" class ">->" class
-| "Coercion" by_notation ":" class ">->" class
+| "Coercion" reference ":" class ">->" class
 | "Context" LIST1 binder
 | "Instance" OPT ( ident_decl LIST0 binder ) ":" term OPT hint_info OPT [ ":=" "{" LIST0 field_def "}" | ":=" term ]
 | "Existing" "Instance" qualid OPT hint_info
 | "Existing" "Instances" LIST1 qualid OPT [ "|" num ]
 | "Existing" "Class" qualid
-| "Arguments" smart_qualid LIST0 arg_specs LIST0 [ "," LIST0 implicits_alt ] OPT [ ":" LIST1 args_modifier SEP "," ]
+| "Arguments" reference LIST0 arg_specs LIST0 [ "," LIST0 implicits_alt ] OPT [ ":" LIST1 args_modifier SEP "," ]
 | "Implicit" [ "Type" | "Types" ] reserv_list
 | "Generalizable" [ [ "Variable" | "Variables" ] LIST1 ident | "All" "Variables" | "No" "Variables" ]
 | "Set" setting_name OPT [ int | string ]
@@ -936,7 +941,7 @@ command: [
 | "Eval" red_expr "in" term
 | "Compute" term
 | "Check" term
-| "About" smart_qualid OPT univ_name_list
+| "About" reference OPT univ_name_list
 | "SearchHead" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
 | "SearchPattern" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
 | "SearchRewrite" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
@@ -990,12 +995,6 @@ setting_name: [
 | LIST1 ident
 ]
 
-comment: [
-| one_term
-| string
-| num
-]
-
 search_query: [
 | search_item
 | "-" search_query
@@ -1009,18 +1008,10 @@ search_item: [
 ]
 
 logical_kind: [
-| thm_token
-| assumption_token
-| "Context"
-| "Definition"
-| "Example"
-| "Coercion"
-| "Instance"
-| "Scheme"
-| "Canonical"
-| "Field"
-| "Method"
-| "Primitive"
+| [ thm_token | assumption_token ]
+| [ "Definition" | "Example" | "Context" | "Primitive" ]
+| [ "Coercion" | "Instance" | "Scheme" | "Canonical" | "SubClass" ]
+| [ "Field" | "Method" ]
 ]
 
 univ_name_list: [
@@ -1045,8 +1036,7 @@ hint: [
 ]
 
 tacdef_body: [
-| qualid LIST1 fun_var [ ":=" | "::=" ] ltac_expr
-| qualid [ ":=" | "::=" ] ltac_expr
+| qualid LIST0 name [ ":=" | "::=" ] ltac_expr
 ]
 
 ltac_production_item: [
@@ -1115,7 +1105,7 @@ eauto_search_strategy_name: [
 class: [
 | "Funclass"
 | "Sortclass"
-| smart_qualid
+| reference
 ]
 
 syntax_modifier: [
@@ -1204,6 +1194,38 @@ simple_tactic: [
 | "generalize" "dependent" one_term
 | "replace" one_term "with" one_term OPT clause_dft_concl OPT ( "by" ltac_expr3 )
 | "replace" OPT [ "->" | "<-" ] one_term OPT clause_dft_concl
+| "try" ltac_expr3
+| "do" int_or_var ltac_expr3
+| "timeout" int_or_var ltac_expr3
+| "time" OPT string ltac_expr3
+| "repeat" ltac_expr3
+| "progress" ltac_expr3
+| "once" ltac_expr3
+| "exactly_once" ltac_expr3
+| "infoH" ltac_expr3
+| "abstract" ltac_expr2 OPT ( "using" ident )
+| "only" selector ":" ltac_expr3
+| "tryif" ltac_expr "then" ltac_expr "else" ltac_expr2
+| "first" "[" LIST0 ltac_expr SEP "|" "]"
+| "solve" "[" LIST0 ltac_expr SEP "|" "]"
+| "idtac" LIST0 [ ident | string | int ]
+| [ "fail" | "gfail" ] OPT int_or_var LIST0 [ ident | string | int ]
+| "eval" red_expr "in" term
+| "context" ident "[" term "]"
+| "type" "of" term
+| "fresh" LIST0 [ string | qualid ]
+| "type_term" one_term
+| "numgoals"
+| "uconstr" ":" "(" term ")"
+| "fun" LIST1 name "=>" ltac_expr
+| "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" ltac_expr
+| "info" ltac_expr
+| ltac_expr3 ";" [ ltac_expr3 | binder_tactic ]
+| ltac_expr3 ";" "[" for_each_goal "]"
+| ltac_expr1 "+" [ ltac_expr2 | binder_tactic ]
+| ltac_expr1 "||" [ ltac_expr2 | binder_tactic ]
+| "[>" for_each_goal "]"
+| toplevel_selector ":" ltac_expr
 | "simplify_eq" OPT destruction_arg
 | "esimplify_eq" OPT destruction_arg
 | "discriminate" OPT destruction_arg
@@ -1242,8 +1264,7 @@ simple_tactic: [
 | "hresolve_core" "(" ident ":=" one_term ")" OPT ( "at" int_or_var ) "in" one_term
 | "hget_evar" int_or_var
 | "destauto" OPT ( "in" ident )
-| "transparent_abstract" ltac_expr3
-| "transparent_abstract" ltac_expr3 "using" ident
+| "transparent_abstract" ltac_expr3 OPT ( "using" ident )
 | "constr_eq" one_term one_term
 | "constr_eq_strict" one_term one_term
 | "constr_eq_nounivs" one_term one_term
@@ -1266,13 +1287,11 @@ simple_tactic: [
 | "guard" int_or_var comparison int_or_var
 | "decompose" "[" LIST1 one_term "]" one_term
 | "optimize_heap"
-| "with_strategy" strategy_level_or_var "[" LIST1 smart_qualid "]" ltac_expr3
+| "with_strategy" strategy_level_or_var "[" LIST1 reference "]" ltac_expr3
 | "start" "ltac" "profiling"
 | "stop" "ltac" "profiling"
 | "reset" "ltac" "profile"
-| "show" "ltac" "profile"
-| "show" "ltac" "profile" "cutoff" int
-| "show" "ltac" "profile" string
+| "show" "ltac" "profile" OPT [ "cutoff" int | string ]
 | "restart_timer" OPT string
 | "finish_timing" OPT ( "(" string ")" ) OPT string
 | "eassumption"
@@ -1283,7 +1302,6 @@ simple_tactic: [
 | "auto" OPT int_or_var OPT auto_using OPT hintbases
 | "info_auto" OPT int_or_var OPT auto_using OPT hintbases
 | "debug" "auto" OPT int_or_var OPT auto_using OPT hintbases
-| "prolog" "[" LIST0 one_term "]" int_or_var
 | "eauto" OPT int_or_var OPT int_or_var OPT auto_using OPT hintbases
 | "new" "auto" OPT int_or_var OPT auto_using OPT hintbases
 | "debug" "eauto" OPT int_or_var OPT int_or_var OPT auto_using OPT hintbases
@@ -1383,7 +1401,7 @@ simple_tactic: [
 | "firstorder" OPT ltac_expr firstorder_rhs
 | "gintuition" OPT ltac_expr
 | "functional" "inversion" [ ident | num ] OPT qualid      (* funind plugin *)
-| "functional" "induction" LIST1 one_term OPT fun_ind_using OPT with_names      (* funind plugin *)
+| "functional" "induction" term OPT fun_ind_using OPT with_names      (* funind plugin *)
 | "soft" "functional" "induction" LIST1 one_term OPT fun_ind_using OPT with_names      (* funind plugin *)
 | "psatz_Z" OPT int_or_var ltac_expr
 | "xlia" ltac_expr      (* micromega plugin *)
@@ -1407,6 +1425,8 @@ simple_tactic: [
 | "protect_fv" string OPT ( "in" ident )
 | "ring_lookup" ltac_expr0 "[" LIST0 one_term "]" LIST1 one_term      (* setoid_ring plugin *)
 | "field_lookup" ltac_expr "[" LIST0 one_term "]" LIST1 one_term      (* setoid_ring plugin *)
+| match_key OPT "reverse" "goal" "with" OPT "|" LIST1 ( goal_pattern "=>" ltac_expr ) SEP "|" "end"
+| match_key ltac_expr "with" OPT "|" LIST1 ( match_pattern "=>" ltac_expr ) SEP "|" "end"
 | "classical_left"
 | "classical_right"
 | "contradict" ident
@@ -1421,6 +1441,7 @@ simple_tactic: [
 | "split_Rabs"
 | "split_Rmult"
 | "tauto"
+| "time_constr" ltac_expr
 | "zify"
 | "assert_fails" ltac_expr3
 | "assert_succeeds" ltac_expr3
@@ -1432,6 +1453,7 @@ simple_tactic: [
 | "psatz" term OPT int_or_var
 | "ring" OPT ( "[" LIST1 term "]" )
 | "ring_simplify" OPT ( "[" LIST1 term "]" ) LIST1 term OPT ( "in" ident )
+| qualid LIST1 tactic_arg
 ]
 
 hloc: [
@@ -1676,134 +1698,67 @@ rewstrategy: [
 | "old_hints" ident
 ]
 
-ltac_expr: [
-| binder_tactic
-| ltac_expr4
+l3_tactic: [
 ]
 
-binder_tactic: [
-| "fun" LIST1 fun_var "=>" ltac_expr
-| "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" ltac_expr
-| "info" ltac_expr
+l2_tactic: [
 ]
 
-fun_var: [
-| ident
-| "_"
+l1_tactic: [
 ]
 
-let_clause: [
-| ident ":=" ltac_expr
-| "_" ":=" ltac_expr
-| ident LIST1 fun_var ":=" ltac_expr
+binder_tactic: [
 ]
 
-ltac_expr4: [
-| ltac_expr3 ";" binder_tactic
-| ltac_expr3 ";" ltac_expr3
-| ltac_expr3 ";" "[" OPT multi_goal_tactics "]"
-| ltac_expr3
-| ltac_expr3 ";" "[" ">" OPT multi_goal_tactics "]"
+value_tactic: [
 ]
 
-multi_goal_tactics: [
-| OPT ltac_expr "|" multi_goal_tactics
-| ltac_expr_opt ".." OPT "|" ltac_expr_opt_list_or
-| ltac_expr
+syn_value: [
+| ident ":" "(" nonterminal ")"
 ]
 
-ltac_expr_opt: [
-| OPT ltac_expr
+ltac_expr: [
+| [ ltac_expr4 | binder_tactic ]
 ]
 
-ltac_expr_opt_list_or: [
-| ltac_expr_opt_list_or "|" ltac_expr_opt
-| ltac_expr_opt
-| ltac_expr_opt_list_or "|" OPT ltac_expr
-| OPT ltac_expr
+ltac_expr4: [
+| ltac_expr3 ";" [ ltac_expr3 | binder_tactic ]
+| ltac_expr3 ";" "[" for_each_goal "]"
+| ltac_expr3
 ]
 
 ltac_expr3: [
-| "try" ltac_expr3
-| "do" int_or_var ltac_expr3
-| "timeout" int_or_var ltac_expr3
-| "time" OPT string ltac_expr3
-| "repeat" ltac_expr3
-| "progress" ltac_expr3
-| "once" ltac_expr3
-| "exactly_once" ltac_expr3
-| "infoH" ltac_expr3
-| "abstract" ltac_expr2
-| "abstract" ltac_expr2 "using" ident
-| only_selector ltac_expr3
+| l3_tactic
 | ltac_expr2
 ]
 
-only_selector: [
-| "only" selector ":"
-]
-
-selector: [
-| LIST1 range_selector SEP ","
-| "[" ident "]"
-]
-
-range_selector: [
-| num "-" num
-| num
-]
-
 ltac_expr2: [
-| ltac_expr1 "+" binder_tactic
-| ltac_expr1 "+" ltac_expr2
-| "tryif" ltac_expr "then" ltac_expr "else" ltac_expr2
-| ltac_expr1 "||" binder_tactic
-| ltac_expr1 "||" ltac_expr2
+| ltac_expr1 "+" [ ltac_expr2 | binder_tactic ]
+| ltac_expr1 "||" [ ltac_expr2 | binder_tactic ]
+| l2_tactic
 | ltac_expr1
 ]
 
 ltac_expr1: [
-| ltac_match_term
-| "first" "[" LIST0 ltac_expr SEP "|" "]"
-| "solve" "[" LIST0 ltac_expr SEP "|" "]"
-| "idtac" LIST0 message_token
-| failkw OPT int_or_var LIST0 message_token
-| ltac_match_goal
-| simple_tactic
-| tactic_arg
-| qualid LIST0 tactic_arg_compat
+| tactic_value
+| qualid LIST1 tactic_arg
+| l1_tactic
 | ltac_expr0
 ]
 
-message_token: [
-| ident
-| string
-| int
-]
-
-failkw: [
-| "fail"
-| "gfail"
+tactic_value: [
+| [ value_tactic | syn_value ]
 ]
 
 tactic_arg: [
-| "eval" red_expr "in" term
-| "context" ident "[" term "]"
-| "type" "of" term
-| "fresh" LIST0 [ string | qualid ]
-| "type_term" one_term
-| "numgoals"
-]
-
-tactic_arg_compat: [
-| tactic_arg
+| tactic_value
 | term
 | "()"
 ]
 
 ltac_expr0: [
 | "(" ltac_expr ")"
-| "[>" OPT multi_goal_tactics "]"
+| "[>" for_each_goal "]"
 | tactic_atom
 ]
 
@@ -1813,43 +1768,61 @@ tactic_atom: [
 | "()"
 ]
 
+let_clause: [
+| name ":=" ltac_expr
+| ident LIST1 name ":=" ltac_expr
+]
+
+for_each_goal: [
+| goal_tactics
+| OPT ( goal_tactics "|" ) OPT ltac_expr ".." OPT ( "|" goal_tactics )
+]
+
+goal_tactics: [
+| LIST0 ( OPT ltac_expr ) SEP "|"
+]
+
 toplevel_selector: [
-| selector ":"
-| "all" ":"
-| "!" ":"
+| selector
+| "all"
+| "!"
+| "par"
 ]
 
-ltac_match_term: [
-| match_key ltac_expr "with" OPT "|" LIST1 match_rule SEP "|" "end"
+selector: [
+| LIST1 range_selector SEP ","
+| "[" ident "]"
+]
+
+range_selector: [
+| num "-" num
+| num
 ]
 
 match_key: [
+| "lazymatch"
 | "match"
 | "multimatch"
-| "lazymatch"
-]
-
-match_rule: [
-| [ match_pattern | "_" ] "=>" ltac_expr
 ]
 
 match_pattern: [
-| "context" OPT ident "[" term "]"
-| term
+| cpattern
+| "context" OPT ident "[" cpattern "]"
 ]
 
-ltac_match_goal: [
-| match_key OPT "reverse" "goal" "with" OPT "|" LIST1 match_context_rule SEP "|" "end"
+cpattern: [
+| term
 ]
 
-match_context_rule: [
-| LIST0 match_hyp SEP "," "|-" match_pattern "=>" ltac_expr
-| "[" LIST0 match_hyp SEP "," "|-" match_pattern "]" "=>" ltac_expr
-| "_" "=>" ltac_expr
+goal_pattern: [
+| LIST0 match_hyp SEP "," "|-" match_pattern
+| "[" LIST0 match_hyp SEP "," "|-" match_pattern "]"
+| "_"
 ]
 
 match_hyp: [
 | name ":" match_pattern
-| name ":=" OPT ( "[" match_pattern "]" ":" ) match_pattern
+| name ":=" match_pattern
+| name ":=" "[" match_pattern "]" ":" match_pattern
 ]