Convert ltac2 chapter to use prodn, update syntax

14 files changed, 2835 insertions, 356 deletions

diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index e5c2056c40..985aebd1ed 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -455,7 +455,7 @@ Tactic language
   (`#11882 <https://github.com/coq/coq/pull/11882>`_,
   by Hugo Herbelin).
 - **Added:**
-  Ltac2 notations for reductions in terms: :n:`eval @red_expr in @ltac2_term`
+  Ltac2 notations for reductions in terms: :n:`eval @red_expr in @term`
   (`#11981 <https://github.com/coq/coq/pull/11981>`_,
   by Michael Soegtrop).
 - **Fixed:**
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index 99762c7a0e..ee8784fc02 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -187,6 +187,16 @@ nitpick_ignore = [ ('token', token) for token in [
     'collection',
     'modpath',
     'tactic',
+    'destruction_arg',
+    'bindings',
+    'induction_clause',
+    'conversion',
+    'where',
+    'oriented_rewriter',
+    'hintbases',
+    'bindings_with_parameters',
+    'destruction_arg',
+    'clause_dft_concl'
 ]]
 
 # -- Options for HTML output ----------------------------------------------
diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst
index 64b29c1c0b..1f0d696d99 100644
--- a/doc/sphinx/language/core/basic.rst
+++ b/doc/sphinx/language/core/basic.rst
@@ -227,6 +227,7 @@ rest of the |Coq| manual: :term:`terms <term>` and :term:`types
         | @term_match
         | @term_record
         | @term_generalizing
+        | [| {*; @term } %| @term {? : @type } |] {? @univ_annot }
         | @term_ltac
         | ( @term )
         qualid_annotated ::= @qualid {? @univ_annot }
diff --git a/doc/sphinx/language/core/conversion.rst b/doc/sphinx/language/core/conversion.rst
index 0f27b65107..6b031cfea3 100644
--- a/doc/sphinx/language/core/conversion.rst
+++ b/doc/sphinx/language/core/conversion.rst
@@ -5,8 +5,14 @@ Conversion rules
 
 In |Cic|, there is an internal reduction mechanism. In particular, it
 can decide if two programs are *intentionally* equal (one says
-*convertible*). Convertibility is described in this section.
+:term:`convertible`). Convertibility is described in this section.
 
+α-conversion
+~~~~~~~~~~~~
+
+Two terms are :gdef:`α-convertible <alpha-convertible>` if they are syntactically
+equal ignoring differences in the names of variables bound within the expression.
+For example `forall x, x + 0 = x` is α-convertible with `forall y, y + 0 = y`.
 
 .. _beta-reduction:
 
@@ -153,7 +159,7 @@ relation :math:`t` reduces to :math:`u` in the global environment
 reductions β, δ, ι or ζ.
 
 We say that two terms :math:`t_1` and :math:`t_2` are
-*βδιζη-convertible*, or simply *convertible*, or *equivalent*, in the
+*βδιζη-convertible*, or simply :gdef:`convertible`, or *equivalent*, in the
 global environment :math:`E` and local context :math:`Γ` iff there
 exist terms :math:`u_1` and :math:`u_2` such that :math:`E[Γ] ⊢ t_1 \triangleright
 … \triangleright u_1` and :math:`E[Γ] ⊢ t_2 \triangleright … \triangleright u_2` and either :math:`u_1` and
diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst
index b4558ef07f..34752a4c4d 100644
--- a/doc/sphinx/language/extensions/match.rst
+++ b/doc/sphinx/language/extensions/match.rst
@@ -90,11 +90,15 @@ constructions. There are two variants of them.
 First destructuring let syntax
 ++++++++++++++++++++++++++++++
 
+.. todo explain that this applies to all of the "let" constructs (Gallina, Ltac1 and Ltac2)
+   also add "irrefutable pattern" to the glossary
+   note that in Ltac2 an upper case ident is a constructor, lower case is a variable
+
 The expression :n:`let ( {*, @ident__i } ) := @term__0 in @term__1`
 performs case analysis on :n:`@term__0` whose type must be an
 inductive type with exactly one constructor.  The number of variables
 :n:`@ident__i` must correspond to the number of arguments of this
-contrustor.  Then, in :n:`@term__1`, these variables are bound to the
+constructor.  Then, in :n:`@term__1`, these variables are bound to the
 arguments of the constructor in :n:`@term__0`.  For instance, the
 definition
 
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index b0b0367d6d..e7ba82fb31 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -1122,12 +1122,14 @@ Pattern matching on terms: match
    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?
+   .. todo how does this differ from the 1-2 other unification routines elsewhere in Coq?
+      Does it use constr_eq or eq_constr_nounivs?
 
    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`
+   expression.  Expressions match if they are syntactically equal or are
+   :term:`α-convertible <alpha-convertible>`.
+   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.
 
@@ -1305,20 +1307,20 @@ Pattern matching on terms: match
 
    .. example:: Multiple matches for a "context" pattern.
 
-      Internally "x <> y" is represented as "(not x y)", which produces the
+      Internally "x <> y" is represented as "(~ (x = y))", which produces the
       first match.
 
       .. coqtop:: in reset
 
          Ltac f t := match t with
-                    | context [ (not ?t) ] => idtac "?t = " t; fail
+                    | context [ (~ ?t) ] => idtac "?t = " t; fail
                     | _ => idtac
                     end.
          Goal True.
 
       .. coqtop:: all
 
-         f ((not True) <> (not False)).
+         f ((~ True) <> (~ False)).
 
 .. _ltac-match-goal:
 
@@ -1345,6 +1347,13 @@ Pattern matching on goals and hypotheses: match goal
    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.
 
+   Matching is non-linear: if a
+   metavariable occurs more than once, each occurrence must match the same
+   expression.  Within a single term, expressions match if they are syntactically equal or
+   :term:`α-convertible <alpha-convertible>`.  When a metavariable is used across
+   multiple hypotheses or across a hypothesis and the current goal, the expressions match if
+   they are :term:`convertible`.
+
    :n:`{*, @match_hyp }`
       Patterns to match with hypotheses.  Each pattern must match a distinct hypothesis in order
       for the branch to match.
@@ -1381,7 +1390,7 @@ Pattern matching on goals and hypotheses: match goal
            :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
+         :n:`@term__binder`\s in the form `[?x ; ?y]` for a list are 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.
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index 1e35160205..b217448711 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -27,6 +27,50 @@ especially wherever an advanced tactic language is needed. The previous
 implementation of Ltac, described in the previous chapter, will be referred to
 as Ltac1.
 
+Current limitations include:
+
+- There are a number of tactics that are not yet supported in Ltac2 because
+  the interface OCaml and/or Ltac2 notations haven't been written.  See
+  :ref:`defining_tactics`.
+
+- Missing usability features such as:
+
+  - Printing functions are limited and awkward to use.  Only a few data types are
+    printable.
+  - Deep pattern matching and matching on tuples don't work.
+  - If statements on Ltac2 boolean values
+  - A convenient way to build terms with casts through the low-level API. Because the
+    cast type is opaque, building terms with casts currently requires an awkward construction like the
+    following, which also incurs extra overhead to repeat typechecking for each
+    call to `get_vm_cast`:
+
+    .. coqdoc::
+
+       Constr.Unsafe.make (Constr.Unsafe.Cast 'I (get_vm_cast ()) 'True)
+
+    with:
+
+    .. coqtop:: none
+
+       From Ltac2 Require Import Ltac2.
+
+    .. coqtop:: in
+
+       Ltac2 get_vm_cast () :=
+         match Constr.Unsafe.kind '(I <: True) with
+         | Constr.Unsafe.Cast _ cst _ => cst
+         | _ => Control.throw Not_found
+         end.
+
+- Missing low-level primitives that are convenient for writing automation, such as:
+
+  - An easy way to get the number of constructors of an inductive type.
+    Currently only way to do this is to destruct a variable of the inductive type
+    and count the number of goals that result.
+- The :attr:`deprecated` attribute is not supported for Ltac2 definitions.
+
+- Error messages may be cryptic.
+
 .. _ltac2_design:
 
 General design
@@ -49,7 +93,7 @@ In particular, Ltac2 is:
   Coq-side terms
 - a language featuring notation facilities to help write palatable scripts
 
-We describe more in details each point in the remainder of this document.
+We describe these in more detail in the remainder of this document.
 
 ML component
 ------------
@@ -84,7 +128,7 @@ which allows to ensure that Ltac2 satisfies the same equations as a generic ML
 with unspecified effects would do, e.g. function reduction is substitution
 by a value.
 
-To import Ltac2, use the following command:
+Use the following command to import Ltac2:
 
 .. coqtop:: in
 
@@ -96,17 +140,20 @@ Type Syntax
 At the level of terms, we simply elaborate on Ltac1 syntax, which is quite
 close to OCaml. Types follow the simply-typed syntax of OCaml.
 
-The non-terminal :production:`lident` designates identifiers starting with a
-lowercase.
+.. insertprodn ltac2_type ltac2_typevar
 
-.. productionlist:: coq
-   ltac2_type             : ( `ltac2_type`, ... , `ltac2_type` ) `ltac2_typeconst`
-                    : ( `ltac2_type` * ... * `ltac2_type` )
-                    : `ltac2_type` -> `ltac2_type`
-                    : `ltac2_typevar`
-   ltac2_typeconst        : ( `modpath` . )* `lident`
-   ltac2_typevar          : '`lident`
-   ltac2_typeparams       : ( `ltac2_typevar`, ... , `ltac2_typevar` )
+.. prodn::
+   ltac2_type ::= @ltac2_type2 -> @ltac2_type
+   | @ltac2_type2
+   ltac2_type2 ::= @ltac2_type1 * {+* @ltac2_type1 }
+   | @ltac2_type1
+   ltac2_type1 ::= @ltac2_type0 @qualid
+   | @ltac2_type0
+   ltac2_type0 ::= ( {+, @ltac2_type } ) {? @qualid }
+   | @ltac2_typevar
+   | _
+   | @qualid
+   ltac2_typevar ::= ' @ident
 
 The set of base types can be extended thanks to the usual ML type
 declarations such as algebraic datatypes and records.
@@ -126,114 +173,156 @@ Type declarations
 
 One can define new types with the following commands.
 
-.. cmd:: Ltac2 Type {? @ltac2_typeparams } @lident
+.. cmd:: Ltac2 Type {? rec } @tac2typ_def {* with @tac2typ_def }
    :name: Ltac2 Type
 
-   This command defines an abstract type. It has no use for the end user and
-   is dedicated to types representing data coming from the OCaml world.
+   .. insertprodn tac2typ_def tac2rec_field
 
-.. cmdv:: Ltac2 Type {? rec} {? @ltac2_typeparams } @lident := @ltac2_typedef
+   .. prodn::
+      tac2typ_def ::= {? @tac2typ_prm } @qualid {? {| := | ::= } @tac2typ_knd }
+      tac2typ_prm ::= @ltac2_typevar
+      | ( {+, @ltac2_typevar } )
+      tac2typ_knd ::= @ltac2_type
+      | [ {? {? %| } {+| @tac2alg_constructor } } ]
+      | [ .. ]
+      | %{ {? {+; @tac2rec_field } {? ; } } %}
+      tac2alg_constructor ::= @ident
+      | @ident ( {*, @ltac2_type } )
+      tac2rec_field ::= {? mutable } @ident : @ltac2_type
 
-   This command defines a type with a manifest. There are four possible
-   kinds of such definitions: alias, variant, record and open variant types.
+   :n:`:=`
+     Defines a type with with an explicit set of constructors
 
-   .. productionlist:: coq
-      ltac2_typedef    : `ltac2_type`
-                       : [ `ltac2_constructordef` | ... | `ltac2_constructordef` ]
-                       : { `ltac2_fielddef` ; ... ; `ltac2_fielddef` }
-                       : [ .. ]
-      ltac2_constructordef   : `uident` [ ( `ltac2_type` , ... , `ltac2_type` ) ]
-      ltac2_fielddef         : [ mutable ] `ident` : `ltac2_type`
+   :n:`::=`
+     Extends an existing open variant type, a special kind of variant type whose constructors are not
+     statically defined, but can instead be extended dynamically. A typical example
+     is the standard `exn` type for exceptions. Pattern matching on open variants must always
+     include a catch-all clause. They can be extended with this form, in which case
+     :token:`tac2typ_knd` should be in the form :n:`[ {? {? %| } {+| @tac2alg_constructor } } ]`.
 
-   Aliases are just a name for a given type expression and are transparently
-   unfoldable to it. They cannot be recursive. The non-terminal
-   :production:`uident` designates identifiers starting with an uppercase.
+   Without :n:`{| := | ::= }`
+     Defines an abstract type for use representing data from OCaml.  Not for
+     end users.
+
+   :n:`with @tac2typ_def`
+     Permits definition of mutually recursive type definitions.
+
+   Each production of :token:`tac2typ_knd` defines one of four possible kinds
+   of definitions, respectively: alias, variant, open variant and record types.
+
+   Aliases are names for a given type expression and are transparently
+   unfoldable to that expression. They cannot be recursive.
+
+   .. The non-terminal :token:`uident` designates identifiers starting with an uppercase.
 
    Variants are sum types defined by constructors and eliminated by
    pattern-matching. They can be recursive, but the `rec` flag must be
    explicitly set. Pattern matching must be exhaustive.
 
+   Open variants can be extended with additional constructors using the `::=` form.
+
    Records are product types with named fields and eliminated by projection.
    Likewise they can be recursive if the `rec` flag is set.
 
-   .. cmdv:: Ltac2 Type {? @ltac2_typeparams } @ltac2_qualid ::= [ @ltac2_constructordef ]
+.. cmd:: Ltac2 @ external @ident : @ltac2_type := @string @string
+   :name: Ltac2 external
+
+   Declares abstract terms.  Frequently, these declare OCaml functions
+   defined in |Coq| and give their type information.  They can also declare
+   data structures from OCaml.  This command has no use for the end user.
+
+APIs
+~~~~
+
+Ltac2 provides over 150 API functions that provide various capabilities.  These
+are declared with :cmd:`Ltac2 external` in :n:`lib/coq/user-contrib/Ltac2/*.v`.
+For example, `Message.print` defined in `Message.v` is used to print messages:
 
-      Open variants are a special kind of variant types whose constructors are not
-      statically defined, but can instead be extended dynamically. A typical example
-      is the standard `exn` type. Pattern matching on open variants must always include a catch-all
-      clause. They can be extended with this command.
+.. coqtop:: none
+
+   Goal True.
+
+.. coqtop:: all abort
+
+   Message.print (Message.of_string "fully qualified calls").
+   From Ltac2 Require Import Message.
+   print (of_string "unqualified calls").
 
 Term Syntax
 ~~~~~~~~~~~
 
-The syntax of the functional fragment is very close to the one of Ltac1, except
+The syntax of the functional fragment is very close to that of Ltac1, except
 that it adds a true pattern-matching feature, as well as a few standard
 constructs from ML.
 
-.. productionlist:: coq
-   ltac2_var        : `lident`
-   ltac2_qualid     : ( `modpath` . )* `lident`
-   ltac2_constructor: `uident`
-   ltac2_term       : `ltac2_qualid`
-                    : `ltac2_constructor`
-                    : `ltac2_term` `ltac2_term` ... `ltac2_term`
-                    : fun `ltac2_var` => `ltac2_term`
-                    : let `ltac2_var` := `ltac2_term` in `ltac2_term`
-                    : let rec `ltac2_var` := `ltac2_term` in `ltac2_term`
-                    : match `ltac2_term` with `ltac2_branch` ... `ltac2_branch` end
-                    : `int`
-                    : `string`
-                    : `ltac2_term` ; `ltac2_term`
-                    : [| `ltac2_term` ; ... ; `ltac2_term` |]
-                    : ( `ltac2_term` , ... , `ltac2_term` )
-                    : { `ltac2_field` `ltac2_field` ... `ltac2_field` }
-                    : `ltac2_term` . ( `ltac2_qualid` )
-                    : `ltac2_term` . ( `ltac2_qualid` ) := `ltac2_term`
-                    : [; `ltac2_term` ; ... ; `ltac2_term` ]
-                    : `ltac2_term` :: `ltac2_term`
-                    : ...
-   ltac2_branch     : `ltac2_pattern` => `ltac2_term`
-   ltac2_pattern    : `ltac2_var`
-                    : _
-                    : ( `ltac2_pattern` , ... , `ltac2_pattern` )
-                    : `ltac2_constructor` `ltac2_pattern` ... `ltac2_pattern`
-                    : [ ]
-                    : `ltac2_pattern` :: `ltac2_pattern`
-   ltac2_field      : `ltac2_qualid` := `ltac2_term`
-
-In practice, there is some additional syntactic sugar that allows e.g. to
-bind a variable and match on it at the same time, in the usual ML style.
+In practice, there is some additional syntactic sugar that allows the
+user to bind a variable and match on it at the same time, in the usual ML style.
 
 There is dedicated syntax for list and array literals.
 
-.. note::
+.. insertprodn ltac2_expr ltac2_tactic_atom
+
+.. prodn::
+   ltac2_expr ::= @ltac2_expr5 ; @ltac2_expr
+   | @ltac2_expr5
+   ltac2_expr5 ::= fun {+ @tac2pat0 } => @ltac2_expr
+   | let {? rec } @ltac2_let_clause {* with @ltac2_let_clause } in @ltac2_expr
+   | @ltac2_expr3
+   ltac2_let_clause ::= {+ @tac2pat0 } := @ltac2_expr
+   ltac2_expr3 ::= {+, @ltac2_expr2 }
+   ltac2_expr2 ::= @ltac2_expr1 :: @ltac2_expr2
+   | @ltac2_expr1
+   ltac2_expr1 ::= @ltac2_expr0 {+ @ltac2_expr0 }
+   | @ltac2_expr0 .( @qualid )
+   | @ltac2_expr0 .( @qualid ) := @ltac2_expr5
+   | @ltac2_expr0
+   tac2rec_fieldexpr ::= @qualid := @ltac2_expr1
+   ltac2_expr0 ::= ( @ltac2_expr )
+   | ( @ltac2_expr : @ltac2_type )
+   | ()
+   | [ {*; @ltac2_expr5 } ]
+   | %{ {? {+ @tac2rec_fieldexpr } {? ; } } %}
+   | @ltac2_tactic_atom
+   ltac2_tactic_atom ::= @int
+   | @string
+   | @qualid
+   | @ @ident
+   | & @lident
+   | ' @term
+   | @ltac2_quotations
+
+The non-terminal :production:`lident` designates identifiers starting with a
+lowercase letter.
+
+:n:`'@term` is equivalent to :n:`open_constr:(@term)`.
 
-   For now, deep pattern matching is not implemented.
 
-Ltac Definitions
-~~~~~~~~~~~~~~~~
 
-.. cmd:: Ltac2 {? mutable} {? rec} @lident := @ltac2_value
+Ltac2 Definitions
+~~~~~~~~~~~~~~~~~
+
+.. cmd:: Ltac2 {? mutable } {? rec } @tac2def_body {* with @tac2def_body }
    :name: Ltac2
 
-   This command defines a new global Ltac2 value.
+   .. insertprodn tac2def_body tac2def_body
+
+   .. prodn::
+      tac2def_body ::= {| _ | @ident } {* @tac2pat0 } := @ltac2_expr
+
+   This command defines a new global Ltac2 value.  If one or more :token:`tac2pat0`
+   are specified, the new value is a function.  This is a shortcut for one of the
+   :token:`ltac2_expr5` productions.  For example: :n:`Ltac2 foo a b := …` is equivalent
+   to :n:`Ltac2 foo := fun a b => …`.
 
    The body of an Ltac2 definition is required to be a syntactical value
    that is, a function, a constant, a pure constructor recursively applied to
    values or a (non-recursive) let binding of a value in a value.
 
-   .. productionlist:: coq
-      ltac2_value: fun `ltac2_var` => `ltac2_term`
-                       : `ltac2_qualid`
-                       : `ltac2_constructor` `ltac2_value` ... `ltac2_value`
-                       : `ltac2_var`
-                       : let `ltac2_var` := `ltac2_value` in `ltac2_value`
-
    If ``rec`` is set, the tactic is expanded into a recursive binding.
 
    If ``mutable`` is set, the definition can be redefined at a later stage (see below).
 
-.. cmd:: Ltac2 Set @qualid {? as @lident} := @ltac2_term
+.. cmd:: Ltac2 Set @qualid {? as @ident } := @ltac2_expr
    :name: Ltac2 Set
 
    This command redefines a previous ``mutable`` definition.
@@ -254,7 +343,6 @@ Ltac Definitions
 
    .. example:: Interaction with recursive calls
 
-
       .. coqtop:: all
 
          Ltac2 mutable rec f b := match b with true => 0 | _ => f true end.
@@ -334,7 +422,7 @@ Intuitively a thunk of type :n:`unit -> 'a` can do the following:
   i.e. thunks can produce a lazy list of results where each
   tail is waiting for a continuation exception.
 - It can access a backtracking proof state, consisting among other things of
-  the current evar assignation and the list of goals under focus.
+  the current evar assignment and the list of goals under focus.
 
 We now describe more thoroughly the various effects in Ltac2.
 
@@ -348,8 +436,8 @@ Mutable fields of records can be modified using the set syntax. Likewise,
 built-in types like `string` and `array` feature imperative assignment. See
 modules `String` and `Array` respectively.
 
-A few printing primitives are provided in the `Message` module, allowing to
-display information to the user.
+A few printing primitives are provided in the `Message` module for
+displaying information to the user.
 
 Fatal errors
 ++++++++++++
@@ -458,20 +546,27 @@ Ltac2 makes these explicit using quoting and unquoting notation, although there
 are notations to do it in a short and elegant way so as not to be too cumbersome
 to the user.
 
-Generic Syntax for Quotations
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-In general, quotations can be introduced in terms using the following syntax, where
-:production:`quotentry` is some parsing entry.
-
-.. prodn::
-   ltac2_term += @ident : ( @quotentry )
+Quotations
+~~~~~~~~~~
 
 .. _ltac2_built-in-quotations:
 
 Built-in quotations
 +++++++++++++++++++
 
+.. insertprodn ltac2_quotations ltac1_expr_in_env
+
+.. prodn::
+   ltac2_quotations ::= ident : ( @lident )
+   | constr : ( @term )
+   | open_constr : ( @term )
+   | pattern : ( @cpattern )
+   | reference : ( {| & @ident | @qualid } )
+   | ltac1 : ( @ltac1_expr_in_env )
+   | ltac1val : ( @ltac1_expr_in_env )
+   ltac1_expr_in_env ::= @ltac_expr
+   | {* @ident } |- @ltac_expr
+
 The current implementation recognizes the following built-in quotations:
 
 - ``ident``, which parses identifiers (type ``Init.ident``).
@@ -481,16 +576,17 @@ The current implementation recognizes the following built-in quotations:
   holes at runtime (type ``Init.constr`` as well).
 - ``pattern``, which parses Coq patterns and produces a pattern used for term
   matching (type ``Init.pattern``).
-- ``reference``, which parses either a :n:`@qualid` or :n:`&@ident`. Qualified names
+- ``reference``  Qualified names
   are globalized at internalization into the corresponding global reference,
   while ``&id`` is turned into ``Std.VarRef id``. This produces at runtime a
-  ``Std.reference``. There shall be no white space between the ampersand
-  symbol (``&``) and the identifier (:n:`@ident`).
+  ``Std.reference``.
+- ``ltac1``, for calling Ltac1 code, described in :ref:`simple_api`.
+- ``ltac1val``, for manipulating Ltac1 values, described in :ref:`low_level_api`.
 
-The following syntactic sugar is provided for two common cases.
+The following syntactic sugar is provided for two common cases:
 
 - ``@id`` is the same as ``ident:(id)``
-- ``'t`` is the same as ``open_constr:(t)``
+- :n:`'@term` is the same as :n:`open_constr:(@term)`
 
 Strict vs. non-strict mode
 ++++++++++++++++++++++++++
@@ -521,11 +617,11 @@ Term Antiquotations
 Syntax
 ++++++
 
-One can also insert Ltac2 code into Coq terms, similarly to what is possible in
+One can also insert Ltac2 code into Coq terms, similar to what is possible in
 Ltac1.
 
 .. prodn::
-   term += ltac2:( @ltac2_term )
+   term += ltac2:( @ltac2_expr )
 
 Antiquoted terms are expected to have type ``unit``, as they are only evaluated
 for their side-effects.
@@ -659,168 +755,473 @@ insert in a concise way an Ltac2 variable of type :n:`constr` into a Coq term.
 Match over terms
 ~~~~~~~~~~~~~~~~
 
-Ltac2 features a construction similar to Ltac1 :n:`match` over terms, although
+Ltac2 features a construction similar to Ltac1 :tacn:`match` over terms, although
 in a less hard-wired way.
 
-.. productionlist:: coq
-   ltac2_term       : match! `ltac2_term` with `constrmatching` .. `constrmatching` end
-                    : lazy_match! `ltac2_term` with `constrmatching` .. `constrmatching` end
-                    : multi_match! `ltac2_term` with `constrmatching` .. `constrmatching` end
-   constrmatching  : | `constrpattern` => `ltac2_term`
-   constrpattern   : `term`
-                   : context  [ `term` ]
-                   : context `lident` [ `term` ]
-
-This construction is not primitive and is desugared at parsing time into
-calls to term matching functions from the `Pattern` module. Internally, it is
-implemented thanks to a specific scope accepting the :n:`@constrmatching` syntax.
-
-Variables from the :n:`@constrpattern` are statically bound in the body of the branch, to
-values of type `constr` for the variables from the :n:`@term` pattern and to a
-value of type `Pattern.context` for the variable :n:`@lident`.
-
-Note that unlike Ltac, only lowercase identifiers are valid as Ltac2
-bindings, so that there will be a syntax error if one of the bound variables
+.. tacn:: @ltac2_match_key @ltac2_expr__term with @ltac2_match_list end
+   :name: lazy_match!; match!; multi_match!
+
+   .. insertprodn ltac2_match_key ltac2_match_pattern
+
+   .. prodn::
+      ltac2_match_key ::= lazy_match!
+      | match!
+      | multi_match!
+      ltac2_match_list ::= {? %| } {+| @ltac2_match_rule }
+      ltac2_match_rule ::= @ltac2_match_pattern => @ltac2_expr
+      ltac2_match_pattern ::= @cpattern
+      | context {? @ident } [ @cpattern ]
+
+   Evaluates :n:`@ltac2_expr__term`, which must yield a term, and matches it
+   sequentially with the :token:`ltac2_match_pattern`\s, which may contain
+   metavariables.  When a match is found, metavariable values are substituted
+   into :n:`@ltac2_expr`, which is then applied.
+
+   Matching may continue depending on whether  `lazy_match!`, `match!` or `multi_match!`
+   is specified.
+
+   In the :token:`ltac2_match_pattern`\s, metavariables have the form :n:`?@ident`, whereas
+   in the :n:`@ltac2_expr`\s, the question mark is omitted.
+
+   .. todo how does this differ from the 1-2 other unification routines elsewhere in Coq?
+
+   Matching is non-linear: if a
+   metavariable occurs more than once, each occurrence must match the same
+   expression.  Expressions match if they are syntactically equal or are
+   :term:`α-convertible <alpha-convertible>`.
+   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.
+
+   .. todo the `@?ident` form is in dangling_pattern_extension_rule, not included in the doc yet
+      maybe belongs with "Applications"
+
+   `lazy_match!`
+      Causes the match to commit to the first matching branch
+      rather than trying a new match if :n:`@ltac2_expr` fails.
+      :ref:`Example<ltac2_match_vs_lazymatch_ex>`.
+
+   `match!`
+      If :n:`@ltac2_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<ltac2_match_vs_lazymatch_ex>` and
+      :ref:`here<ltac2_match_vs_multimatch_ex>`.
+
+   `multi_match!`
+      If :n:`@ltac2_expr` fails, continue matching with the next branch.
+      When a :n:`@ltac2_expr` succeeds for a branch, subsequent failures
+      (after the `multi_match!`) causing consumption of all the successes
+      of :n:`@ltac2_expr` trigger selection of a new matching branch.
+      :ref:`Example<ltac2_match_vs_multimatch_ex>`.
+
+   :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` and :n:`@?@ident`.  :g:`_` can be used to match
+      irrelevant terms.
+
+      .. todo more on @?@ident here: https://github.com/coq/coq/pull/12085#discussion_r467504046
+      .. todo Example is broken :ref:`Example<ltac2_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
+
+      Unlike Ltac1, Ltac2 :n:`?id` metavariables only match closed terms.
+
+      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.  This hole in the matched context can be filled with the expression
+      :n:`Pattern.instantiate @ident @cpattern`.
+
+      For :tacn:`match!` and :tacn:`multi_match!`, if the evaluation of the :token:`ltac2_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<ltac2_match_term_context_ex>`.
+
+   .. todo There's a more realistic example from @JasonGross here:
+      https://github.com/coq/coq/pull/12103#discussion_r432996954
+
+   :n:`@ltac2_expr`
+      The tactic to apply if the construct matches.  Metavariable values from the pattern
+      match are statically bound as Ltac2 variables in :n:`@ltac2_expr` before
+      it is applied.
+
+      If :n:`@ltac2_expr` is a tactic with backtracking points, then subsequent
+      failures after a :tacn:`lazy_match!` or :tacn:`multi_match!` (but not :tacn:`match!`) can cause
+      backtracking into :n:`@ltac2_expr` to select its next success.
+
+   Variables from the :n:`@tac2pat1` are statically bound in the body of the branch.
+   Variables from the :n:`@term` pattern have values of type `constr`.
+   Variables from the :n:`@ident` in the `context` construct have values of type
+   `Pattern.context` (defined in `Pattern.v`).
+
+Note that unlike Ltac1, only lowercase identifiers are valid as Ltac2
+bindings.  Ltac2 will report an error if one of the bound variables
 starts with an uppercase character.
 
-The semantics of this construction is otherwise the same as the corresponding
+The semantics of this construction are otherwise the same as the corresponding
 one from Ltac1, except that it requires the goal to be focused.
 
+.. _ltac2_match_vs_lazymatch_ex:
+
+.. example:: Ltac2 Comparison of lazy_match! and match!
+
+   (Equivalent to this :ref:`Ltac1 example<match_vs_lazymatch_ex>`.)
+
+   These lines define a `msg` tactic that's used in several examples as a more-succinct
+   alternative to `print (to_string "...")`:
+
+   .. coqtop:: in
+
+      From Ltac2 Require Import Message.
+      Ltac2 msg x := print (of_string x).
+
+   .. coqtop:: none
+
+      Goal True.
+
+   In :tacn:`lazy_match!`, if :token:`ltac2_expr` fails, the :tacn:`lazy_match!` fails;
+   it doesn't look for further matches.  In :tacn:`match!`, if :token:`ltac2_expr` fails
+   in a matching branch, it will try to match on subsequent branches.  Note that
+   :n:`'@term` below is equivalent to :n:`open_constr:(@term)`.
+
+   .. coqtop:: all
+
+      Fail lazy_match! 'True with
+      | True => msg "branch 1"; fail
+      | _ => msg "branch 2"
+      end.
+
+      match! 'True with
+      | True => msg "branch 1"; fail
+      | _ => msg "branch 2"
+      end.
+
+.. _ltac2_match_vs_multimatch_ex:
+
+.. example:: Ltac2 Comparison of match! and multi_match!
+
+   (Equivalent to this :ref:`Ltac1 example<match_vs_multimatch_ex>`.)
+
+   :tacn:`match!` tactics are only evaluated once, whereas :tacn:`multi_match!`
+   tactics may be evaluated more than once if the following constructs trigger backtracking:
+
+   .. coqtop:: all
+
+      Fail match! 'True with
+      | True => msg "branch 1"
+      | _ => msg "branch 2"
+      end ;
+      msg "branch A"; fail.
+
+   .. coqtop:: all
+
+      Fail multi_match! 'True with
+      | True => msg "branch 1"
+      | _ => msg "branch 2"
+      end ;
+      msg "branch A"; fail.
+
+.. _ltac2_match_with_holes_ex:
+
+.. todo EXAMPLE DOESN'T WORK: Ltac2 does not (yet?) handle pattern variables matching open terms.
+   Matching a pattern with holes
+
+   (Equivalent to this :ref:`Ltac1 example<match_with_holes_ex>`.)
+
+   Notice the :tacn:`idtac` prints ``(z + 1)`` while the :tacn:`pose` substitutes
+   ``(x + 1)``.
+
+   .. coqtop:: all
+
+      match! constr:(fun x => (x + 1) * 3) with
+      | fun z => ?y * 3 => print (of_constr y); pose (fun z: nat => $y * 5)
+      end.
+
+.. _ltac2_match_term_context_ex:
+
+.. example:: Ltac2 Multiple matches for a "context" pattern.
+
+   (Equivalent to this :ref:`Ltac1 example<match_term_context_ex>`.)
+
+   Internally "x <> y" is represented as "(~ (x = y))", which produces the
+   first match.
+
+   .. coqtop:: in
+
+      Ltac2 f2 t := match! t with
+                    | context [ (~ ?t) ] => print (of_constr t); fail
+                    | _ => ()
+                    end.
+
+   .. coqtop:: all abort
+
+      f2 constr:((~ True) <> (~ False)).
+
 Match over goals
 ~~~~~~~~~~~~~~~~
 
-Similarly, there is a way to match over goals in an elegant way, which is
-just a notation desugared at parsing time.
+.. tacn:: @ltac2_match_key {? reverse } goal with @goal_match_list end
+   :name: lazy_match! goal; match! goal; multi_match! goal
 
-.. productionlist:: coq
-   ltac2_term             : match! [ reverse ] goal with `goalmatching` ... `goalmatching` end
-                    : lazy_match! [ reverse ] goal with `goalmatching` ... `goalmatching` end
-                    : multi_match! [ reverse ] goal with `goalmatching` ... `goalmatching` end
-   goalmatching     : | [ `hypmatching` ... `hypmatching` |- `constrpattern` ] => `ltac2_term`
-   hypmatching      : `lident` : `constrpattern`
-                    : _ : `constrpattern`
+   .. insertprodn goal_match_list gmatch_hyp_pattern
 
-Variables from :n:`@hypmatching` and :n:`@constrpattern` are bound in the body of the
-branch. Their types are:
+   .. prodn::
+      goal_match_list ::= {? %| } {+| @gmatch_rule }
+      gmatch_rule ::= @gmatch_pattern => @ltac2_expr
+      gmatch_pattern ::= [ {*, @gmatch_hyp_pattern } |- @ltac2_match_pattern ]
+      gmatch_hyp_pattern ::= @name : @ltac2_match_pattern
 
-- ``constr`` for pattern variables appearing in a :n:`@term`
-- ``Pattern.context`` for variables binding a context
-- ``ident`` for variables binding a hypothesis name.
+   Matches over goals, similar to Ltac1 :tacn:`match goal`.
+   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:`@ltac2_match_key @ltac2_expr` construct
+   (see :tacn:`match!`).  Each current goal is processed independently.
 
-The same identifier caveat as in the case of matching over constr applies, and
-this features has the same semantics as in Ltac1. In particular, a ``reverse``
-flag can be specified to match hypotheses from the more recently introduced to
-the least recently introduced one.
+   Matching is non-linear: if a
+   metavariable occurs more than once, each occurrence must match the same
+   expression.  Within a single term, expressions match if they are syntactically equal or
+   :term:`α-convertible <alpha-convertible>`.  When a metavariable is used across
+   multiple hypotheses or across a hypothesis and the current goal, the expressions match if
+   they are :term:`convertible`.
 
-.. _ltac2_notations:
+   .. more detail here: https://github.com/coq/coq/pull/12085#discussion_r470406466
 
-Notations
----------
+   :n:`{*, @gmatch_pattern }`
+      Patterns to match with hypotheses.  Each pattern must match a distinct hypothesis in order
+      for the branch to match.
 
-Notations are the crux of the usability of Ltac1. We should be able to recover
-a feeling similar to the old implementation by using and abusing notations.
+      Hypotheses have the form :n:`@name {? := @term__binder } : @type`.  Currently Ltac2 doesn't
+      allow matching on or capturing the value of :n:`@term__binder`.  It only supports matching on
+      the :token:`name` and the :token:`type`, for example `n : ?t`.
 
-Scopes
-~~~~~~
+      .. currently only supports the first row
+         :list-table::
+         :widths: 2 1
+         :header-rows: 1
 
-A scope is a name given to a grammar entry used to produce some Ltac2 expression
-at parsing time. Scopes are described using a form of S-expression.
+         * - Pattern syntax
+           - Example pattern
 
-.. prodn::
-   ltac2_scope ::= {| @string | @int | @lident ({+, @ltac2_scope}) }
+         * - :n:`@name : @ltac2_match_pattern`
+           - `n : ?t`
 
-A few scopes contain antiquotation features. For the sake of uniformity, all
-antiquotations are introduced by the syntax :n:`$@lident`.
+         * - :n:`@name := @match_pattern__binder`
+           - `n := ?b`
 
-The following scopes are built-in.
+         * - :n:`@name := @term__binder : @type`
+           - `n := ?b : ?t`
 
-- :n:`constr`:
+         * - :n:`@name := [ @match_pattern__binder ] : @ltac2_match_pattern`
+           - `n := [ ?b ] : ?t`
 
-  + parses :n:`c = @term` and produces :n:`constr:(c)`
+         :token:`name` can't have a `?`.  Note that the last two forms are equivalent except that:
 
-  This scope can be parameterized by a list of delimiting keys of notation
-  scopes (as described in :ref:`LocalInterpretationRulesForNotations`),
-  describing how to interpret the parsed term. For instance, :n:`constr(A, B)`
-  parses :n:`c = @term` and produces :n:`constr:(c%A%B)`.
+         - 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:`ident`:
+      If there are multiple :token:`gmatch_hyp_pattern`\s in a branch, there may be multiple ways to match them to hypotheses.
+      For :tacn:`match! goal` and :tacn:`multi_match! goal`, if the evaluation of the :token:`ltac2_expr` fails,
+      matching will continue with the next hypothesis combination.  When those are exhausted,
+      the next alternative from any `context` construct in the :token:`ltac2_match_pattern`\s is tried and then,
+      when the context alternatives are exhausted, the next branch is tried.
+      :ref:`Example<ltac2_match_goal_multiple_hyps_ex>`.
 
-  + parses :n:`id = @ident` and produces :n:`ident:(id)`
-  + parses :n:`$(x = @ident)` and produces the variable :n:`x`
+   `reverse`
+      Hypothesis matching for :token:`gmatch_hyp_pattern`\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<ltac2_match_goal_hyps_ex>` and :ref:`reverse<ltac2_match_goal_hyps_rev_ex>` examples.
 
-- :n:`list0(@ltac2_scope)`:
+   :n:`|- @ltac2_match_pattern`
+      A pattern to match with the current goal
 
-  + if :n:`@ltac2_scope` parses :n:`@quotentry`,
-    then it parses :n:`(@quotentry__0, ..., @quotentry__n)` and produces
-    :n:`[@quotentry__0; ...; @quotentry__n]`.
+   Note that unlike Ltac1, only lowercase identifiers are valid as Ltac2
+   bindings.  Ltac2 will report an error if you try to use a bound variable
+   that starts with an uppercase character.
 
-- :n:`list0(@ltac2_scope, sep = @string__sep)`:
+   Variables from :n:`@gmatch_hyp_pattern` and :n:`@ltac2_match_pattern` are
+   bound in the body of the branch. Their types are:
 
-  + if :n:`@ltac2_scope` parses :n:`@quotentry`,
-    then it parses :n:`(@quotentry__0 @string__sep ... @string__sep @quotentry__n)`
-    and produce :n:`[@quotentry__0; ...; @quotentry__n]`.
+   - ``constr`` for pattern variables appearing in a :n:`@term`
+   - ``Pattern.context`` for variables binding a context
+   - ``ident`` for variables binding a hypothesis name.
 
-- :n:`list1`: same as :n:`list0` (with or without separator) but parses :n:`{+ @quotentry}` instead
-  of :n:`{* @quotentry}`.
+   The same identifier caveat as in the case of matching over constr applies, and
+   this feature has the same semantics as in Ltac1.
 
-- :n:`opt(@ltac2_scope)`
+.. _ltac2_match_goal_hyps_ex:
 
-  + if :n:`@ltac2_scope` parses :n:`@quotentry`, parses :n:`{? @quotentry}` and produces either :n:`None` or
-    :n:`Some x` where :n:`x` is the parsed expression.
+.. example:: Ltac2 Matching hypotheses
 
-- :n:`self`:
+   (Equivalent to this :ref:`Ltac1 example<match_goal_hyps_ex>`.)
 
-  + parses a Ltac2 expression at the current level and returns it as is.
+   Hypotheses are matched from the last hypothesis (which is by default the newest
+   hypothesis) to the first until the :tacn:`apply` succeeds.
 
-- :n:`next`:
+   .. coqtop:: all abort
 
-  + parses a Ltac2 expression at the next level and returns it as is.
+      Goal forall A B : Prop, A -> B -> (A->B).
+      intros.
+      match! goal with
+      | [ h : _ |- _ ] => let h := Control.hyp h in print (of_constr h); apply $h
+      end.
 
-- :n:`tactic(n = @int)`:
+.. _ltac2_match_goal_hyps_rev_ex:
 
-  + parses a Ltac2 expression at the provided level :n:`n` and returns it as is.
+.. example:: Matching hypotheses with reverse
 
-- :n:`thunk(@ltac2_scope)`:
+   (Equivalent to this :ref:`Ltac1 example<match_goal_hyps_rev_ex>`.)
 
-  + parses the same as :n:`scope`, and if :n:`e` is the parsed expression, returns
-    :n:`fun () => e`.
+   Hypotheses are matched from the first hypothesis to the last until the :tacn:`apply` succeeds.
 
-- :n:`STRING`:
+   .. coqtop:: all abort
 
-  + parses the corresponding string as an identifier and returns :n:`()`.
+      Goal forall A B : Prop, A -> B -> (A->B).
+      intros.
+      match! reverse goal with
+      | [ h : _ |- _ ] => let h := Control.hyp h in print (of_constr h); apply $h
+      end.
 
-- :n:`keyword(s = @string)`:
+.. _ltac2_match_goal_multiple_hyps_ex:
 
-  + parses the string :n:`s` as a keyword and returns `()`.
+.. example:: Multiple ways to match a hypotheses
 
-- :n:`terminal(s = @string)`:
+   (Equivalent to this :ref:`Ltac1 example<match_goal_multiple_hyps_ex>`.)
 
-  + parses the string :n:`s` as a keyword, if it is already a
-    keyword, otherwise as an :n:`@ident`. Returns `()`.
+   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.
 
-- :n:`seq(@ltac2_scope__1, ..., @ltac2_scope__2)`:
+   .. coqtop:: all abort
 
-  + parses :n:`scope__1`, ..., :n:`scope__n` in this order, and produces a tuple made
-    out of the parsed values in the same order. As an optimization, all
-    subscopes of the form :n:`STRING` are left out of the returned tuple, instead
-    of returning a useless unit value. It is forbidden for the various
-    subscopes to refer to the global entry using :n:`self` or :n:`next`.
+      Goal forall A B : Prop, A -> B -> (A->B).
+      intros A B H.
+      match! goal with
+      | [ h1 : _, h2 : _ |- _ ] =>
+         print (concat (of_string "match ")
+               (concat (of_constr (Control.hyp h1))
+               (concat (of_string " ")
+               (of_constr (Control.hyp h2)))));
+         fail
+      | [ |- _ ] => ()
+      end.
 
-A few other specific scopes exist to handle Ltac1-like syntax, but their use is
-discouraged and they are thus not documented.
 
-For now there is no way to declare new scopes from Ltac2 side, but this is
-planned.
+Match on values
+~~~~~~~~~~~~~~~
 
-Notations
-~~~~~~~~~
+.. tacn:: match @ltac2_expr5 with {? @ltac2_branches } end
+   :name: match (Ltac2)
+
+   Matches a value, akin to the OCaml `match` construct.  By itself, it doesn't cause backtracking
+   as do the `*match*!` and `*match*! goal` constructs.
+
+   .. insertprodn ltac2_branches atomic_tac2pat
 
-The Ltac2 parser can be extended with syntactic notations.
+   .. prodn::
+      ltac2_branches ::= {? %| } {+| @tac2pat1 => @ltac2_expr }
+      tac2pat1 ::= @qualid {+ @tac2pat0 }
+      | @qualid
+      | [ ]
+      | @tac2pat0 :: @tac2pat0
+      | @tac2pat0
+      tac2pat0 ::= _
+      | ()
+      | @qualid
+      | ( {? @atomic_tac2pat } )
+      atomic_tac2pat ::= @tac2pat1 : @ltac2_type
+      | @tac2pat1 , {*, @tac2pat1 }
+      | @tac2pat1
 
-.. cmd:: Ltac2 Notation {+ {| @lident (@ltac2_scope) | @string } } {? : @int} := @ltac2_term
+.. note::
+
+   For now, deep pattern matching is not implemented.
+
+
+.. _ltac2_notations:
+
+Notations
+---------
+
+.. cmd:: Ltac2 Notation {+ @ltac2_scope } {? : @int } := @ltac2_expr
    :name: Ltac2 Notation
 
-   A Ltac2 notation adds a parsing rule to the Ltac2 grammar, which is expanded
+   .. todo seems like name maybe should use lident rather than ident, considering:
+
+      Ltac2 Notation "ex1" X(constr) := print (of_constr X).
+      ex1 1.
+
+      Unbound constructor X
+
+      This works fine with lower-case "x" in place of "X"
+
+   .. todo Ltac2 Notation := permits redefining same symbol (no warning)
+      Also allows defining a symbol beginning with uppercase, which is prohibited
+      in similar constructs.
+
+   :cmd:`Ltac2 Notation` provides a way to extend the syntax of Ltac2 tactics.  The left-hand
+   side (before the `:=`) defines the syntax to recognize and gives formal parameter
+   names for the syntactic values.  :n:`@int` is the level of the notation.
+   When the notation is used, the values are substituted
+   into the right-hand side.  The right-hand side is typechecked when the notation is used,
+   not when it is defined.  In the following example, `x` is the formal parameter name and
+   `constr` is its :ref:`syntactic class<syntactic_classes>`.  `print` and `of_constr` are
+   functions provided by |Coq| through `Message.v`.
+
+   .. todo "print" doesn't seem to pay attention to "Set Printing All"
+
+   .. example:: Printing a :n:`@term`
+
+      .. coqtop:: none
+
+         Goal True.
+
+      .. coqtop:: all
+
+         From Ltac2 Require Import Message.
+         Ltac2 Notation "ex1" x(constr) := print (of_constr x).
+         ex1 (1 + 2).
+
+      You can also print terms with a regular Ltac2 definition, but then the :n:`@term` must be in
+      the quotation `constr:( … )`:
+
+      .. coqtop:: all
+
+         Ltac2 ex2 x := print (of_constr x).
+         ex2 constr:(1+2).
+
+   There are also metasyntactic classes described :ref:`here<syntactic_classes>`
+   that combine other items.  For example, `list1(constr, ",")`
+   recognizes a comma-separated list of one or more :token:`term`\s.
+
+   .. example:: Parsing a list of :n:`@term`\s
+
+      .. coqtop:: abort all
+
+         Ltac2 rec print_list x := match x with
+         | a :: t => print (of_constr a); print_list t
+         | [] => ()
+         end.
+         Ltac2 Notation "ex2" x(list1(constr, ",")) := print_list x.
+         ex2 1, 2, 3.
+
+   An Ltac2 notation adds a parsing rule to the Ltac2 grammar, which is expanded
    to the provided body where every token from the notation is let-bound to the
    corresponding generated expression.
 
@@ -848,37 +1249,432 @@ The Ltac2 parser can be extended with syntactic notations.
 Abbreviations
 ~~~~~~~~~~~~~
 
-.. cmdv:: Ltac2 Notation @lident := @ltac2_term
+.. cmd:: Ltac2 Notation {| @string | @lident } := @ltac2_expr
+   :name: Ltac2 Notation (abbreviation)
 
-  This command introduces a special kind of notation, called an abbreviation,
-  that is designed so that it does not add any parsing rules. It is similar in
-  spirit to Coq abbreviations, insofar as its main purpose is to give an
-  absolute name to a piece of pure syntax, which can be transparently referred to
-  by this name as if it were a proper definition.
+   Introduces a special kind of notation, called an abbreviation,
+   that does not add any parsing rules. It is similar in
+   spirit to Coq abbreviations (see :cmd:`Notation (abbreviation)`,
+   insofar as its main purpose is to give an
+   absolute name to a piece of pure syntax, which can be transparently referred to
+   by this name as if it were a proper definition.
 
-  The abbreviation can then be manipulated just as a normal Ltac2 definition,
-  except that it is expanded at internalization time into the given expression.
-  Furthermore, in order to make this kind of construction useful in practice in
-  an effectful language such as Ltac2, any syntactic argument to an abbreviation
-  is thunked on-the-fly during its expansion.
+   The abbreviation can then be manipulated just like a normal Ltac2 definition,
+   except that it is expanded at internalization time into the given expression.
+   Furthermore, in order to make this kind of construction useful in practice in
+   an effectful language such as Ltac2, any syntactic argument to an abbreviation
+   is thunked on-the-fly during its expansion.
 
-For instance, suppose that we define the following.
+   For instance, suppose that we define the following.
 
-:n:`Ltac2 Notation foo := fun x => x ().`
+   :n:`Ltac2 Notation foo := fun x => x ().`
 
-Then we have the following expansion at internalization time.
+   Then we have the following expansion at internalization time.
 
-:n:`foo 0 ↦ (fun x => x ()) (fun _ => 0)`
+   :n:`foo 0 ↦ (fun x => x ()) (fun _ => 0)`
 
-Note that abbreviations are not typechecked at all, and may result in typing
-errors after expansion.
+   Note that abbreviations are not type checked at all, and may result in typing
+   errors after expansion.
+
+.. _defining_tactics:
+
+Defining tactics
+~~~~~~~~~~~~~~~~
+
+Built-in tactics (those defined in OCaml code in the |Coq| executable) and Ltac1 tactics,
+which are defined in `.v` files, must be defined through notations.  (Ltac2 tactics can be
+defined with :cmd:`Ltac2`.
+
+Notations for many but not all built-in tactics are defined in `Notations.v`, which is automatically
+loaded with Ltac2.  The Ltac2 syntax for these tactics is often identical or very similar to the
+tactic syntax described in other chapters of this documentation.  These notations rely on tactic functions
+declared in `Std.v`.  Functions corresponding to some built-in tactics may not yet be defined in the
+|Coq| executable or declared in `Std.v`.  Adding them may require code changes to |Coq| or defining
+workarounds through Ltac1 (described below).
+
+Two examples of syntax differences:
+
+- There is no notation defined that's equivalent to :n:`intros until {| @ident | @num }`.  There is,
+  however, already an ``intros_until`` tactic function defined ``Std.v``, so it may be possible for a user
+  to add the necessary notation.
+- The built-in `simpl` tactic in Ltac1 supports the use of scope keys in delta flags, e.g. :n:`simpl ["+"%nat]`
+  which is not accepted by Ltac2.  This is because Ltac2 uses a different
+  definition for :token:`delta_flag`; compare it to :token:`ltac2_delta_flag`.  This also affects
+  :tacn:`compute`.
+
+Ltac1 tactics are not automatically available in Ltac2.  (Note that some of the tactics described
+in the documentation are defined with Ltac1.)
+You can make them accessible in Ltac2 with commands similar to the following:
+
+.. coqtop:: in
+
+   From Coq Require Import Lia.
+   Local Ltac2 lia_ltac1 () := ltac1:(lia).
+   Ltac2 Notation "lia" := lia_ltac1 ().
+
+A similar approach can be used to access missing built-in tactics.  See :ref:`simple_api` for an
+example that passes two parameters to a missing build-in tactic.
+
+.. _syntactic_classes:
+
+Syntactic classes
+~~~~~~~~~~~~~~~~~
+
+The simplest syntactic classes in Ltac2 notations represent individual nonterminals
+from the |Coq| grammar.  Only a few selected nonterminals are available as syntactic classes.
+In addition, there are metasyntactic operations for describing
+more complex syntax, such as making an item optional or representing a list of items.
+When parsing, each syntactic class expression returns a value that's bound to a name in the
+notation definition.
+
+Syntactic classes are described with a form of S-expression:
+
+   .. insertprodn ltac2_scope ltac2_scope
+
+   .. prodn::
+      ltac2_scope ::= @string
+      | @int
+      | @name
+      | @name ( {+, @ltac2_scope } )
+
+.. todo no syn class for ints or strings?
+   parm names are not reserved (e.g the var can be named "list1")
+
+Metasyntactic operations that can be applied to other syntactic classes are:
+
+  :n:`opt(@ltac2_scope)`
+    Parses an optional :token:`ltac2_scope`.  The associated value is either :n:`None` or
+    enclosed in :n:`Some`
+
+  :n:`list1(@ltac2_scope {? , @string })`
+    Parses a list of one or more :token:`ltac2_scope`\s.  If :token:`string` is specified,
+    items must be separated by :token:`string`.
+
+  :n:`list0(@ltac2_scope {? , @string })`
+    Parses a list of zero or more :token:`ltac2_scope`\s.  If :token:`string` is specified,
+    items must be separated by :token:`string`.  For zero items, the associated value
+    is an empty list.
+
+  :n:`seq({+, @ltac2_scope })`
+    Parses the :token:`ltac2_scope`\s in order.  The associated value is a tuple,
+    omitting :token:`ltac2_scope`\s that are :token:`string`\s.
+    `self` and `next` are not permitted within `seq`.
+
+The following classes represent nonterminals with some special handling.  The
+table further down lists the classes that that are handled plainly.
+
+  :n:`constr {? ( {+, @scope_key } ) }`
+    Parses a :token:`term`.  If specified, the :token:`scope_key`\s are used to interpret
+    the term (as described in  :ref:`LocalInterpretationRulesForNotations`).  The last
+    :token:`scope_key` is the top of the scope stack that's applied to the :token:`term`.
+
+  :n:`open_constr`
+    Parses an open :token:`term`.
+
+  :n:`ident`
+    Parses :token:`ident` or :n:`$@ident`.  The first form returns :n:`ident:(@ident)`,
+    while the latter form returns the variable :n:`@ident`.
+
+  :n:`@string`
+    Accepts the specified string that is not a keyword, returning a value of `()`.
+
+  :n:`keyword(@string)`
+    Accepts the specified string that is a keyword, returning a value of `()`.
+
+  :n:`terminal(@string)`
+    Accepts the specified string whether it's a keyword or not, returning a value of `()`.
+
+  :n:`tactic {? (@int) }`
+    Parses an :token:`ltac2_expr`.  If :token:`int` is specified, the construct
+    parses a :n:`ltac2_expr@int`, for example `tactic(5)` parses :token:`ltac2_expr5`.
+    `tactic(6)` parses :token:`ltac2_expr`.
+    :token:`int` must be in the range `0 .. 6`.
+
+    You can also use `tactic` to accept an :token:`int` or a :token:`string`, but there's
+    no syntactic class that accepts *only* an :token:`int` or a :token:`string`.
+
+    .. todo this doesn't work as expected: "::" is in ltac2_expr1
+       Ltac2 Notation "ex4" x(tactic(0)) := x.
+       ex4 auto :: [auto].
+
+  .. not sure "self" and "next" do anything special.  I get the same error
+     message for both from constructs like
+
+     Ltac2 Notation "ex5" x(self) := auto.
+     ex5 match.
+
+     Syntax error: [tactic:tac2expr level 5] expected after 'match' (in [tactic:tac2expr]).
+
+  :n:`self`
+    parses an Ltac2 expression at the current level and returns it as is.
+
+  :n:`next`
+    parses an Ltac2 expression at the next level and returns it as is.
+
+  :n:`thunk(@ltac2_scope)`
+    Used for semantic effect only, parses the same as :token:`ltac2_scope`.
+    If :n:`e` is the parsed expression for :token:`ltac2_scope`, `thunk`
+    returns :n:`fun () => e`.
+
+  :n:`pattern`
+    parses a :token:`cpattern`
+
+A few syntactic classes contain antiquotation features. For the sake of uniformity, all
+antiquotations are introduced by the syntax :n:`$@lident`.
+
+A few other specific syntactic classes exist to handle Ltac1-like syntax, but their use is
+discouraged and they are thus not documented.
+
+For now there is no way to declare new syntactic classes from the Ltac2 side, but this is
+planned.
+
+Other nonterminals that have syntactic classes are listed here.
+
+   .. list-table::
+      :header-rows: 1
+
+      * - Syntactic class name
+        - Nonterminal
+        - Similar non-Ltac2 syntax
+
+      * - :n:`intropatterns`
+        - :token:`ltac2_intropatterns`
+        - :token:`intropattern_list`
+
+      * - :n:`intropattern`
+        - :token:`ltac2_simple_intropattern`
+        - :token:`simple_intropattern`
+
+      * - :n:`ident`
+        - :token:`ident_or_anti`
+        - :token:`ident`
+
+      * - :n:`destruction_arg`
+        - :token:`ltac2_destruction_arg`
+        - :token:`destruction_arg`
+
+      * - :n:`with_bindings`
+        - :token:`q_with_bindings`
+        - :n:`{? with @bindings }`
+
+      * - :n:`bindings`
+        - :token:`ltac2_bindings`
+        - :token:`bindings`
+
+      * - :n:`strategy`
+        - :token:`ltac2_strategy_flag`
+        - :token:`strategy_flag`
+
+      * - :n:`reference`
+        - :token:`refglobal`
+        - :token:`reference`
+
+      * - :n:`clause`
+        - :token:`ltac2_clause`
+        - :token:`clause_dft_concl`
+
+      * - :n:`occurrences`
+        - :token:`q_occurrences`
+        - :n:`{? at @occs_nums }`
+
+      * - :n:`induction_clause`
+        - :token:`ltac2_induction_clause`
+        - :token:`induction_clause`
+
+      * - :n:`conversion`
+        - :token:`ltac2_conversion`
+        - :token:`conversion`
+
+      * - :n:`rewriting`
+        - :token:`ltac2_oriented_rewriter`
+        - :token:`oriented_rewriter`
+
+      * - :n:`dispatch`
+        - :token:`ltac2_for_each_goal`
+        - :token:`for_each_goal`
+
+      * - :n:`hintdb`
+        - :token:`hintdb`
+        - :token:`hintbases`
+
+      * - :n:`move_location`
+        - :token:`move_location`
+        - :token:`where`
+
+      * - :n:`pose`
+        - :token:`pose`
+        - :token:`bindings_with_parameters`
+
+      * - :n:`assert`
+        - :token:`assertion`
+        - :n:`( @ident := @term )`
+
+      * - :n:`constr_matching`
+        - :token:`ltac2_match_list`
+        - See :tacn:`match`
+
+      * - :n:`goal_matching`
+        - :token:`goal_match_list`
+        - See :tacn:`match goal`
+
+Here is the syntax for the :n:`q_*` nonterminals:
+
+.. insertprodn ltac2_intropatterns nonsimple_intropattern
+
+.. prodn::
+   ltac2_intropatterns ::= {* @nonsimple_intropattern }
+   nonsimple_intropattern ::= *
+   | **
+   | @ltac2_simple_intropattern
+
+.. insertprodn ltac2_simple_intropattern ltac2_naming_intropattern
+
+.. prodn::
+   ltac2_simple_intropattern ::= @ltac2_naming_intropattern
+   | _
+   | @ltac2_or_and_intropattern
+   | @ltac2_equality_intropattern
+   ltac2_or_and_intropattern ::= [ {+| @ltac2_intropatterns } ]
+   | ()
+   | ( {+, @ltac2_simple_intropattern } )
+   | ( {+& @ltac2_simple_intropattern } )
+   ltac2_equality_intropattern ::= ->
+   | <-
+   | [= @ltac2_intropatterns ]
+   ltac2_naming_intropattern ::= ? @lident
+   | ?$ @lident
+   | ?
+   | @ident_or_anti
+
+.. insertprodn ident_or_anti ident_or_anti
+
+.. prodn::
+   ident_or_anti ::= @lident
+   | $ @ident
+
+.. insertprodn 	ltac2_destruction_arg ltac2_constr_with_bindings
+
+.. prodn::
+   ltac2_destruction_arg ::= @num
+   | @lident
+   | @ltac2_constr_with_bindings
+   ltac2_constr_with_bindings ::= @term {? with @ltac2_bindings }
+
+.. insertprodn q_with_bindings qhyp
+
+.. prodn::
+   q_with_bindings ::= {? with @ltac2_bindings }
+   ltac2_bindings ::= {+ @ltac2_simple_binding }
+   | {+ @term }
+   ltac2_simple_binding ::= ( @qhyp := @term )
+   qhyp ::= $ @ident
+   | @num
+   | @lident
+
+.. insertprodn ltac2_strategy_flag ltac2_delta_flag
+
+.. prodn::
+   ltac2_strategy_flag ::= {+ @ltac2_red_flag }
+   | {? @ltac2_delta_flag }
+   ltac2_red_flag ::= beta
+   | iota
+   | match
+   | fix
+   | cofix
+   | zeta
+   | delta {? @ltac2_delta_flag }
+   ltac2_delta_flag ::= {? - } [ {+ @refglobal } ]
+
+.. insertprodn refglobal refglobal
+
+.. prodn::
+   refglobal ::= & @ident
+   | @qualid
+   | $ @ident
+
+.. insertprodn ltac2_clause ltac2_in_clause
+
+.. prodn::
+   ltac2_clause ::= in @ltac2_in_clause
+   | at @ltac2_occs_nums
+   ltac2_in_clause ::= * {? @ltac2_occs }
+   | * |- {? @ltac2_concl_occ }
+   | {*, @ltac2_hypident_occ } {? |- {? @ltac2_concl_occ } }
+
+.. insertprodn q_occurrences ltac2_hypident
+
+.. prodn::
+   q_occurrences ::= {? @ltac2_occs }
+   ltac2_occs ::= at @ltac2_occs_nums
+   ltac2_occs_nums ::= {? - } {+ {| @num  | $ @ident } }
+   ltac2_concl_occ ::= * {? @ltac2_occs }
+   ltac2_hypident_occ ::= @ltac2_hypident {? @ltac2_occs }
+   ltac2_hypident ::= @ident_or_anti
+   | ( type of @ident_or_anti )
+   | ( value of @ident_or_anti )
+
+.. insertprodn ltac2_induction_clause ltac2_eqn_ipat
+
+.. prodn::
+   ltac2_induction_clause ::= @ltac2_destruction_arg {? @ltac2_as_or_and_ipat } {? @ltac2_eqn_ipat } {? @ltac2_clause }
+   ltac2_as_or_and_ipat ::= as @ltac2_or_and_intropattern
+   ltac2_eqn_ipat ::= eqn : @ltac2_naming_intropattern
+
+.. insertprodn ltac2_conversion ltac2_conversion
+
+.. prodn::
+   ltac2_conversion ::= @term
+   | @term with @term
+
+.. insertprodn ltac2_oriented_rewriter ltac2_rewriter
+
+.. prodn::
+   ltac2_oriented_rewriter ::= {| -> | <- } @ltac2_rewriter
+   ltac2_rewriter ::= {? @num } {? {| ? | ! } } @ltac2_constr_with_bindings
+
+.. insertprodn ltac2_for_each_goal ltac2_goal_tactics
+
+.. prodn::
+   ltac2_for_each_goal ::= @ltac2_goal_tactics
+   | {? @ltac2_goal_tactics %| } {? @ltac2_expr } .. {? %| @ltac2_goal_tactics }
+   ltac2_goal_tactics ::= {*| {? @ltac2_expr } }
+
+.. insertprodn hintdb hintdb
+
+.. prodn::
+   hintdb ::= *
+   | {+ @ident_or_anti }
+
+.. insertprodn move_location move_location
+
+.. prodn::
+   move_location ::= at top
+   | at bottom
+   | after @ident_or_anti
+   | before @ident_or_anti
+
+.. insertprodn pose ltac2_as_name
+
+.. prodn::
+   pose ::= ( @ident_or_anti := @term )
+   | @term {? @ltac2_as_name }
+   ltac2_as_name ::= as @ident_or_anti
+
+.. insertprodn assertion ltac2_by_tactic
+
+.. prodn::
+   assertion ::= ( @ident_or_anti := @term )
+   | ( @ident_or_anti : @term ) {? @ltac2_by_tactic }
+   | @term {? @ltac2_as_ipat } {? @ltac2_by_tactic }
+   ltac2_as_ipat ::= as @ltac2_simple_intropattern
+   ltac2_by_tactic ::= by @ltac2_expr
 
 Evaluation
 ----------
 
 Ltac2 features a toplevel loop that can be used to evaluate expressions.
 
-.. cmd:: Ltac2 Eval @ltac2_term
+.. cmd:: Ltac2 Eval @ltac2_expr
    :name: Ltac2 Eval
 
    This command evaluates the term in the current proof if there is one, or in the
@@ -899,22 +1695,26 @@ Compatibility layer with Ltac1
 Ltac1 from Ltac2
 ~~~~~~~~~~~~~~~~
 
+.. _simple_api:
+
 Simple API
 ++++++++++
 
-One can call Ltac1 code from Ltac2 by using the :n:`ltac1` quotation. It parses
+One can call Ltac1 code from Ltac2 by using the :n:`ltac1:(@ltac1_expr_in_env)` quotation.
+See :ref:`ltac2_built-in-quotations`.  It parses
 a Ltac1 expression, and semantics of this quotation is the evaluation of the
 corresponding code for its side effects. In particular, it cannot return values,
 and the quotation has type :n:`unit`.
 
-.. productionlist:: coq
-  ltac2_term : ltac1 : ( `ltac_expr` )
-
 Ltac1 **cannot** implicitly access variables from the Ltac2 scope, but this can
-be done with an explicit annotation on the :n:`ltac1` quotation.
+be done with an explicit annotation on the :n:`ltac1:({* @ident } |- @ltac_expr)`
+quotation.  See :ref:`ltac2_built-in-quotations`.  For example:
 
-.. productionlist:: coq
-  ltac2_term : ltac1 : ( `ident` ... `ident` |- `ltac_expr` )
+.. coqtop:: in
+
+   Local Ltac2 replace_with (lhs: constr) (rhs: constr) :=
+     ltac1:(lhs rhs |- replace lhs with rhs) (Ltac1.of_constr lhs) (Ltac1.of_constr rhs).
+   Ltac2 Notation "replace" lhs(constr) "with" rhs(constr) := replace_with lhs rhs.
 
 The return type of this expression is a function of the same arity as the number
 of identifiers, with arguments of type `Ltac2.Ltac1.t` (see below). This syntax
@@ -922,6 +1722,8 @@ will bind the variables in the quoted Ltac1 code as if they had been bound from
 Ltac1 itself. Similarly, the arguments applied to the quotation will be passed
 at runtime to the Ltac1 code.
 
+.. _low_level_api:
+
 Low-level API
 +++++++++++++
 
@@ -948,8 +1750,8 @@ Same as above by switching Ltac1 by Ltac2 and using the `ltac2` quotation
 instead.
 
 .. prodn::
-   ltac_expr += ltac2 : ( `ltac2_term` )
-   | ltac2 : ( `ident` ... `ident` |- `ltac2_term` )
+   ltac_expr += ltac2 : ( @ltac2_expr )
+   | ltac2 : ( {+ @ident } |- @ltac2_expr )
 
 The typing rules are dual, that is, the optional identifiers are bound
 with type `Ltac2.Ltac1.t` in the Ltac2 expression, which is expected to have
@@ -992,7 +1794,7 @@ Transition from Ltac1
 
 Owing to the use of a lot of notations, the transition should not be too
 difficult. In particular, it should be possible to do it incrementally. That
-said, we do *not* guarantee you it is going to be a blissful walk either.
+said, we do *not* guarantee it will be a blissful walk either.
 Hopefully, owing to the fact Ltac2 is typed, the interactive dialogue with Coq
 will help you.
 
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 7b3670164b..616669ffa6 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -5584,11 +5584,11 @@ context pattern see :ref:`contextual_patterns_ssr`
 
 discharge item see :ref:`discharge_ssr`
 
-.. prodn:: gen_item ::= {| {? @  } @ident | ( @ident ) | ( {? @  } @ident := @c_pattern ) }
+.. prodn:: gen_item ::= {| {? @ } @ident | ( @ident ) | ( {? @ } @ident := @c_pattern ) }
 
 generalization item see :ref:`structure_ssr`
 
-.. prodn:: i_pattern ::= {| @ident | > | _ | ? | * | + | {? @occ_switch } {| -> | <- } | [ {?|  @i_item } ] | - | [: {+ @ident } ] }
+.. prodn:: i_pattern ::= {| @ident | > | _ | ? | * | + | {? @occ_switch } {| -> | <- } | [ {?| @i_item } ] | - | [: {+ @ident } ] }
 
 intro pattern :ref:`introduction_ssr`
 
@@ -5602,7 +5602,7 @@ view :ref:`introduction_ssr`
 intro block :ref:`introduction_ssr`
 
 .. prodn::
-   i_block ::= {| [^ @ident ] | [^~ {| @ident |  @num } ] }
+   i_block ::= {| [^ @ident ] | [^~ {| @ident | @num } ] }
 
 intro item  see :ref:`introduction_ssr`
 
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 4af3ebc47b..ace0c6201a 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -2997,9 +2997,9 @@ Performing computations
    | pattern {+, @pattern_occ }
    | @ident
    delta_flag ::= {? - } [ {+ @reference } ]
-   strategy_flag ::= {+ @red_flags }
+   strategy_flag ::= {+ @red_flag }
    | @delta_flag
-   red_flags ::= beta
+   red_flag ::= beta
    | iota
    | match
    | fix
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index ad0aab19b5..36ad4af837 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1265,9 +1265,9 @@ Inlining hints for the fast reduction machines
 Registering primitive operations
 ````````````````````````````````
 
-.. cmd:: Primitive @ident {? : @term } := #@ident__prim
+.. cmd:: Primitive @ident_decl {? : @term } := #@ident
 
-   Makes the primitive type or primitive operator :n:`#@ident__prim` defined in OCaml
+   Makes the primitive type or primitive operator :n:`#@ident` defined in OCaml
    accessible in |Coq| commands and tactics.
    For internal use by implementors of |Coq|'s standard library or standard library
    replacements.  No space is allowed after the `#`.  Invalid values give a syntax
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 5cfde2cf2f..6625e07d05 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -54,6 +54,46 @@ SPLICE: [
 | G_TACTIC_in_clause
 ]
 
+RENAME: [
+| G_LTAC2_delta_flag ltac2_delta_flag
+| G_LTAC2_strategy_flag ltac2_strategy_flag
+| G_LTAC2_binder ltac2_binder
+| G_LTAC2_branches ltac2_branches
+| G_LTAC2_let_clause ltac2_let_clause
+| G_LTAC2_tactic_atom ltac2_tactic_atom
+| G_LTAC2_rewriter ltac2_rewriter
+| G_LTAC2_constr_with_bindings ltac2_constr_with_bindings
+| G_LTAC2_match_rule ltac2_match_rule
+| G_LTAC2_match_pattern ltac2_match_pattern
+| G_LTAC2_intropatterns ltac2_intropatterns
+| G_LTAC2_simple_intropattern ltac2_simple_intropattern
+| G_LTAC2_simple_intropattern_closed ltac2_simple_intropattern_closed
+| G_LTAC2_or_and_intropattern ltac2_or_and_intropattern
+| G_LTAC2_equality_intropattern ltac2_equality_intropattern
+| G_LTAC2_naming_intropattern ltac2_naming_intropattern
+| G_LTAC2_destruction_arg ltac2_destruction_arg
+| G_LTAC2_with_bindings ltac2_with_bindings
+| G_LTAC2_bindings ltac2_bindings
+| G_LTAC2_simple_binding ltac2_simple_binding
+| G_LTAC2_in_clause ltac2_in_clause
+| G_LTAC2_occs ltac2_occs
+| G_LTAC2_occs_nums ltac2_occs_nums
+| G_LTAC2_concl_occ ltac2_concl_occ
+| G_LTAC2_hypident_occ ltac2_hypident_occ
+| G_LTAC2_hypident ltac2_hypident
+| G_LTAC2_induction_clause ltac2_induction_clause
+| G_LTAC2_as_or_and_ipat ltac2_as_or_and_ipat
+| G_LTAC2_eqn_ipat ltac2_eqn_ipat
+| G_LTAC2_conversion ltac2_conversion
+| G_LTAC2_oriented_rewriter ltac2_oriented_rewriter
+| G_LTAC2_tactic_then_gen ltac2_tactic_then_gen
+| G_LTAC2_tactic_then_last ltac2_tactic_then_last
+| G_LTAC2_as_name ltac2_as_name
+| G_LTAC2_as_ipat ltac2_as_ipat
+| G_LTAC2_by_tactic ltac2_by_tactic
+| G_LTAC2_match_list ltac2_match_list
+]
+
 (* renames to eliminate qualified names
    put other renames at the end *)
 RENAME: [
@@ -64,7 +104,6 @@ RENAME: [
 | Constr.lconstr_pattern cpattern
 | G_vernac.query_command query_command
 | G_vernac.section_subset_expr section_subset_expr
-| Pltac.tactic tactic
 | Prim.ident ident
 | Prim.reference reference
 | Pvernac.Vernac_.main_entry vernac_control
@@ -109,6 +148,8 @@ DELETE: [
 | test_name_colon
 | test_pipe_closedcurly
 | ensure_fixannot
+| test_array_opening
+| test_array_closing
 
   (* SSR *)
 (* | ssr_null_entry *)
@@ -165,6 +206,26 @@ tactic_then_last: [
 | OPTINREF
 ]
 
+ltac2_tactic_then_last: [
+| REPLACE "|" LIST0 ( OPT tac2expr6 ) SEP "|"      (* Ltac2 plugin *)
+| WITH LIST0 (  "|" OPT tac2expr6 )  TAG Ltac2
+]
+
+ltac2_goal_tactics: [
+| LIST0 ( OPT tac2expr6 ) SEP "|"  TAG Ltac2
+]
+
+ltac2_tactic_then_gen: [ | DELETENT ]
+
+ltac2_tactic_then_gen: [
+| ltac2_goal_tactics  TAG Ltac2
+| OPT ( ltac2_goal_tactics "|" ) OPT tac2expr6 ".." OPT ( "|" ltac2_goal_tactics )  TAG Ltac2
+]
+
+ltac2_tactic_then_last: [
+| OPTINREF
+]
+
 reference: [ | DELETENT ]
 
 reference: [
@@ -340,6 +401,8 @@ operconstr0: [
 | MOVETO term_generalizing "`{" operconstr200 "}"
 | MOVETO term_generalizing "`(" operconstr200 ")"
 | MOVETO term_ltac "ltac" ":" "(" tactic_expr5 ")"
+| REPLACE "[" "|" array_elems "|" lconstr type_cstr "|" "]" univ_instance
+| WITH "[|" array_elems "|" lconstr type_cstr "|]" univ_instance
 ]
 
 fix_decls: [
@@ -582,9 +645,28 @@ delta_flag: [
 | OPTINREF
 ]
 
+ltac2_delta_flag: [
+| EDIT ADD_OPT "-" "[" refglobals "]"      (* Ltac2 plugin *)
+]
+
+ltac2_branches: [
+| EDIT ADD_OPT "|" LIST1 branch SEP "|"      (* Ltac2 plugin *)
+| OPTINREF
+]
+
+RENAME: [
+| red_flag ltac2_red_flag
+| red_flags red_flag
+]
+
+RENAME: [
+]
+
 strategy_flag: [
 | REPLACE OPT delta_flag
 | WITH delta_flag
+(*| REPLACE LIST1 red_flags
+| WITH LIST1 red_flag*)
 | (* empty *)
 | OPTINREF
 ]
@@ -872,7 +954,7 @@ simple_tactic: [
 | DELETE "autorewrite" "with" LIST1 preident clause "using" tactic
 | DELETE "autorewrite" "*" "with" LIST1 preident clause
 | REPLACE "autorewrite" "*" "with" LIST1 preident clause "using" tactic
-| WITH "autorewrite" OPT "*" "with" LIST1 preident clause_dft_concl OPT ( "using" tactic )
+| WITH "autorewrite" OPT "*" "with" LIST1 preident clause OPT ( "using" tactic )
 | DELETE "cofix" ident
 | REPLACE "cofix" ident "with" LIST1 cofixdecl
 | WITH "cofix" ident OPT ( "with" LIST1 cofixdecl )
@@ -931,7 +1013,7 @@ simple_tactic: [
 | DELETE "replace" "->" uconstr clause
 | DELETE "replace" "<-" uconstr clause
 | DELETE "replace" uconstr clause
-| "replace" orient uconstr clause_dft_concl   (* todo: fix 'clause' *)
+| "replace" orient uconstr clause
 | REPLACE "rewrite" "*" orient uconstr "in" hyp "at" occurrences by_arg_tac
 | WITH "rewrite" "*" orient uconstr OPT ( "in" hyp ) OPT ( "at" occurrences by_arg_tac )
 | DELETE "rewrite" "*" orient uconstr "in" hyp by_arg_tac
@@ -1194,6 +1276,7 @@ command: [
 | REPLACE "String" "Notation" reference reference reference ":" ident
 | WITH "String" "Notation" reference reference reference ":" scope_name
 
+| DELETE "Ltac2" ltac2_entry      (* was split up *)
 ]
 
 option_setting: [
@@ -1211,14 +1294,10 @@ syntax: [
 | WITH "Undelimit" "Scope" scope_name
 | REPLACE "Bind" "Scope" IDENT; "with" LIST1 class_rawexpr
 | WITH "Bind" "Scope" scope_name; "with" LIST1 class_rawexpr
-| REPLACE "Infix" ne_lstring ":=" constr [ "(" LIST1 syntax_modifier SEP "," ")" | ]   OPT [ ":" IDENT ]
-| WITH    "Infix" ne_lstring ":=" constr OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" scope_name ]
-| REPLACE "Notation" lstring ":=" constr [ "(" LIST1 syntax_modifier SEP "," ")" | ]   OPT [ ":" IDENT ]
-| WITH    "Notation" lstring ":=" constr OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" scope_name ]
-| REPLACE "Reserved" "Infix" ne_lstring [ "(" LIST1 syntax_modifier SEP "," ")" | ]
-| WITH    "Reserved" "Infix" ne_lstring OPT [ "(" LIST1 syntax_modifier SEP "," ")" ]
-| REPLACE "Reserved" "Notation" ne_lstring [ "(" LIST1 syntax_modifier SEP "," ")" | ]
-| WITH    "Reserved" "Notation" ne_lstring OPT [ "(" LIST1 syntax_modifier SEP "," ")" ]
+| REPLACE "Infix" ne_lstring ":=" constr syntax_modifiers   OPT [ ":" IDENT ]
+| WITH    "Infix" ne_lstring ":=" constr syntax_modifiers OPT [ ":" scope_name ]
+| REPLACE "Notation" lstring ":=" constr syntax_modifiers   OPT [ ":" IDENT ]
+| WITH    "Notation" lstring ":=" constr syntax_modifiers OPT [ ":" scope_name ]
 ]
 
 syntax_modifier: [
@@ -1489,8 +1568,33 @@ by_tactic: [
 ]
 
 rewriter: [
-| REPLACE [ "?" | LEFTQMARK ] constr_with_bindings_arg
-| WITH "?" constr_with_bindings_arg
+| DELETE "!" constr_with_bindings_arg
+| DELETE [ "?" | LEFTQMARK ] constr_with_bindings_arg
+| DELETE natural "!" constr_with_bindings_arg
+| DELETE natural [ "?" | LEFTQMARK ] constr_with_bindings_arg
+| DELETE natural constr_with_bindings_arg
+| DELETE constr_with_bindings_arg
+| OPT natural OPT [ "?" | "!" ] constr_with_bindings_arg
+]
+
+ltac2_rewriter: [
+| DELETE "!" ltac2_constr_with_bindings      (* Ltac2 plugin *)
+| DELETE [ "?" | LEFTQMARK ] ltac2_constr_with_bindings
+| DELETE lnatural "!" ltac2_constr_with_bindings      (* Ltac2 plugin *)
+| DELETE lnatural [ "?" | LEFTQMARK ] ltac2_constr_with_bindings
+| DELETE lnatural ltac2_constr_with_bindings      (* Ltac2 plugin *)
+| DELETE ltac2_constr_with_bindings      (* Ltac2 plugin *)
+| OPT natural OPT [ "?" | "!" ] ltac2_constr_with_bindings
+]
+
+tac2expr0: [
+| DELETE "(" ")"
+]
+
+tac2type_body: [
+| REPLACE ":=" tac2typ_knd      (* Ltac2 plugin *)
+| WITH [ ":=" | "::=" ] tac2typ_knd TAG Ltac2
+| DELETE "::=" tac2typ_knd      (* Ltac2 plugin *)
 ]
 
 intropattern_or_list_or: [
@@ -1556,6 +1660,12 @@ in_clause: [
 | DELETE LIST0 hypident_occ SEP ","
 ]
 
+ltac2_in_clause: [
+| REPLACE LIST0 ltac2_hypident_occ SEP "," "|-" ltac2_concl_occ      (* Ltac2 plugin *)
+| WITH LIST0 ltac2_hypident_occ SEP "," OPT ( "|-" ltac2_concl_occ )  TAG Ltac2
+| DELETE LIST0 ltac2_hypident_occ SEP ","      (* Ltac2 plugin *)
+]
+
 concl_occ: [
 | OPTINREF
 ]
@@ -1628,8 +1738,12 @@ by_notation: [
 ]
 
 decl_notation: [
-| REPLACE ne_lstring ":=" constr only_parsing OPT [ ":" IDENT ]
-| WITH ne_lstring ":=" constr only_parsing OPT [ ":" scope_name ]
+| REPLACE ne_lstring ":=" constr syntax_modifiers OPT [ ":" IDENT ]
+| WITH ne_lstring ":=" constr syntax_modifiers OPT [ ":" scope_name ]
+]
+
+syntax_modifiers: [
+| OPTINREF
 ]
 
 
@@ -1667,6 +1781,15 @@ tactic_mode: [
 | DELETE command
 ]
 
+sexpr: [
+| REPLACE syn_node      (* Ltac2 plugin *)
+| WITH name TAG Ltac2
+| REPLACE syn_node "(" LIST1 sexpr SEP "," ")"      (* Ltac2 plugin *)
+| WITH name "(" LIST1 sexpr SEP "," ")" TAG Ltac2
+]
+
+syn_node: [ | DELETENT ]
+
 RENAME: [
 | toplevel_selector toplevel_selector_temp
 ]
@@ -1785,9 +1908,24 @@ tactic_value: [
 | [ value_tactic | syn_value ]
 ]
 
+
+(* defined in Ltac2/Notations.v *)
+
+ltac2_match_key: [
+| "lazy_match!"
+| "match!"
+| "multi_match!"
+]
+
+ltac2_constructs: [
+| ltac2_match_key tac2expr6 "with" ltac2_match_list "end"
+| ltac2_match_key OPT "reverse" "goal" "with" gmatch_list "end"
+]
+
 simple_tactic: [
 | ltac_builtins
 | ltac_constructs
+| ltac2_constructs
 | ltac_defined_tactics
 | tactic_notation_tactics
 ]
@@ -1798,6 +1936,24 @@ tacdef_body: [
 | DELETE global ltac_def_kind tactic_expr5
 ]
 
+tac2def_typ: [
+| REPLACE "Type" rec_flag LIST1 tac2typ_def SEP "with"      (* Ltac2 plugin *)
+| WITH "Type" rec_flag tac2typ_def LIST0 ( "with" tac2typ_def ) TAG Ltac2
+]
+
+tac2def_val: [
+| REPLACE mut_flag rec_flag LIST1 tac2def_body SEP "with"      (* Ltac2 plugin *)
+| WITH mut_flag rec_flag tac2def_body LIST0 ( "with" tac2def_body ) TAG Ltac1
+]
+
+tac2alg_constructors: [
+| REPLACE "|" LIST1 tac2alg_constructor SEP "|"      (* Ltac2 plugin *)
+| WITH OPT "|" LIST1 tac2alg_constructor SEP "|" TAG Ltac2
+| DELETE LIST0 tac2alg_constructor SEP "|"      (* Ltac2 plugin *)
+| (* empty *)
+| OPTINREF
+]
+
 SPLICE: [
 | def_token
 | extended_def_token
@@ -1823,7 +1979,233 @@ logical_kind: [
 | [ "Field" | "Method" ]
 ]
 
+(* ltac2 *)
+
+DELETE: [
+| test_ltac1_env
+]
+
+mut_flag: [
+| OPTINREF
+]
+
+rec_flag: [
+| OPTINREF
+]
+
+ltac2_orient: [ | DELETENT ]
+
+ltac2_orient: [
+| orient
+]
+
 SPLICE: [
+| ltac2_orient
+]
+
+tac2typ_prm: [
+| OPTINREF
+]
+
+tac2type_body: [
+| OPTINREF
+]
+
+atomic_tac2pat: [
+| OPTINREF
+]
+
+tac2expr0: [
+(*
+| DELETE "(" ")" (* covered by "()" prodn *)
+| REPLACE "{" [  | LIST1 tac2rec_fieldexpr OPT ";" ] "}"
+| WITH "{" OPT ( LIST1 tac2rec_fieldexpr OPT ";" ) "}"
+*)
+]
+
+(* todo: should
+| tac2pat1 "," LIST0 tac2pat1 SEP ","
+use LIST1? *)
+
+SPLICE: [
+| tac2expr4
+]
+
+tac2expr3: [
+| REPLACE tac2expr2 "," LIST1 tac2expr2 SEP ","      (* Ltac2 plugin *)
+| WITH LIST1 tac2expr2 SEP "," TAG Ltac2
+| DELETE tac2expr2      (* Ltac2 plugin *)
+]
+
+tac2rec_fieldexprs: [
+| DELETE tac2rec_fieldexpr ";" tac2rec_fieldexprs
+| DELETE tac2rec_fieldexpr ";"
+| DELETE tac2rec_fieldexpr
+| LIST1 tac2rec_fieldexpr OPT ";"
+| OPTINREF
+]
+
+tac2rec_fields: [
+| DELETE tac2rec_field ";" tac2rec_fields
+| DELETE tac2rec_field ";"
+| DELETE tac2rec_field
+| LIST1 tac2rec_field SEP ";" OPT ";" TAG Ltac2
+| OPTINREF
+]
+
+(* todo: weird productions, ints only after an initial "-"??:
+  occs_nums: [
+  | LIST1 [ num | ident ]
+  | "-" [ num | ident ] LIST0 int_or_var
+*)
+ltac2_occs_nums: [
+| DELETE LIST1 nat_or_anti      (* Ltac2 plugin *)
+| REPLACE "-" nat_or_anti LIST0 nat_or_anti      (* Ltac2 plugin *)
+| WITH OPT "-" LIST1 nat_or_anti TAG Ltac2
+]
+
+syn_level: [
+| OPTINREF
+]
+
+ltac2_delta_flag: [
+| OPTINREF
+]
+
+ltac2_occs: [
+| OPTINREF
+]
+
+ltac2_concl_occ: [
+| OPTINREF
+]
+
+ltac2_with_bindings: [
+| OPTINREF
+]
+
+ltac2_as_or_and_ipat: [
+| OPTINREF
+]
+
+ltac2_eqn_ipat: [
+| OPTINREF
+]
+
+ltac2_as_name: [
+| OPTINREF
+]
+
+ltac2_as_ipat: [
+| OPTINREF
+]
+
+ltac2_by_tactic: [
+| OPTINREF
+]
+
+ltac2_entry: [
+| REPLACE tac2def_typ      (* Ltac2 plugin *)
+| WITH "Ltac2" tac2def_typ
+| REPLACE tac2def_syn      (* Ltac2 plugin *)
+| WITH "Ltac2" tac2def_syn
+| REPLACE tac2def_mut      (* Ltac2 plugin *)
+| WITH "Ltac2" tac2def_mut
+| REPLACE tac2def_val     (* Ltac2 plugin *)
+| WITH "Ltac2" tac2def_val
+| REPLACE tac2def_ext     (* Ltac2 plugin *)
+| WITH "Ltac2" tac2def_ext
+| "Ltac2" "Notation" [ string | lident ] ":=" tac2expr6 TAG Ltac2  (* variant *)
+| MOVEALLBUT command
+(* todo: MOVEALLBUT should ignore tag on "but" prodns *)
+]
+
+ltac2_match_list: [
+| EDIT ADD_OPT "|" LIST1 ltac2_match_rule SEP "|"      (* Ltac2 plugin *)
+]
+
+ltac2_or_and_intropattern: [
+| DELETE "(" ltac2_simple_intropattern ")"      (* Ltac2 plugin *)
+| REPLACE "(" ltac2_simple_intropattern "," LIST1 ltac2_simple_intropattern SEP "," ")"      (* Ltac2 plugin *)
+| WITH "(" LIST1 ltac2_simple_intropattern SEP "," ")" TAG Ltac2
+| REPLACE "(" ltac2_simple_intropattern "&" LIST1 ltac2_simple_intropattern SEP "&" ")"      (* Ltac2 plugin *)
+| WITH "(" LIST1 ltac2_simple_intropattern SEP "&" ")" TAG Ltac2
+]
+
+SPLICE: [
+| tac2def_val
+| tac2def_typ
+| tac2def_ext
+| tac2def_syn
+| tac2def_mut
+| mut_flag
+| rec_flag
+| locident
+| syn_level
+| tac2rec_fieldexprs
+| tac2type_body
+| tac2alg_constructors
+| tac2rec_fields
+| ltac2_binder
+| branch
+| anti
+]
+
+tac2expr5: [
+| REPLACE "let" OPT "rec" LIST1 ltac2_let_clause SEP "with" "in" tac2expr6      (* Ltac2 plugin *)
+| WITH "let" OPT "rec" ltac2_let_clause LIST0 ( "with" ltac2_let_clause ) "in" tac2expr6 TAG Ltac2
+| MOVETO simple_tactic "match" tac2expr5 "with" OPT ltac2_branches "end"      (* Ltac2 plugin *)
+| DELETE simple_tactic
+]
+
+RENAME: [
+| Prim.string string
+| Prim.integer int
+| Prim.qualid qualid
+| Prim.natural num
+]
+
+gmatch_list: [
+| EDIT ADD_OPT "|" LIST1 gmatch_rule SEP "|"      (* Ltac2 plugin *)
+]
+
+ltac2_quotations: [
+
+]
+
+ltac2_tactic_atom: [
+| MOVETO ltac2_quotations "constr" ":" "(" lconstr ")"      (* Ltac2 plugin *)
+| MOVETO ltac2_quotations "open_constr" ":" "(" lconstr ")"      (* Ltac2 plugin *)
+| MOVETO ltac2_quotations "ident" ":" "(" lident ")"      (* Ltac2 plugin *)
+| MOVETO ltac2_quotations "pattern" ":" "(" cpattern ")"      (* Ltac2 plugin *)
+| MOVETO ltac2_quotations "reference" ":" "(" globref ")"      (* Ltac2 plugin *)
+| MOVETO ltac2_quotations "ltac1" ":" "(" ltac1_expr_in_env ")"      (* Ltac2 plugin *)
+| MOVETO ltac2_quotations "ltac1val" ":" "(" ltac1_expr_in_env ")"      (* Ltac2 plugin *)
+]
+
+(* non-Ltac2 "clause" is really clause_dft_concl + there is an ltac2 "clause" *)
+ltac2_clause: [ ]
+
+clause: [
+| MOVEALLBUT ltac2_clause
+]
+
+clause: [
+| clause_dft_concl
+]
+
+q_clause: [
+| REPLACE clause
+| WITH ltac2_clause  TAG Ltac2
+]
+
+ltac2_induction_clause: [
+| REPLACE ltac2_destruction_arg OPT ltac2_as_or_and_ipat OPT ltac2_eqn_ipat OPT clause      (* Ltac2 plugin *)
+| WITH ltac2_destruction_arg OPT ltac2_as_or_and_ipat OPT ltac2_eqn_ipat OPT ltac2_clause  TAG Ltac2
+]
+
+SPLICE: [
+| clause
 | noedit_mode
 | bigint
 | match_list
@@ -1839,6 +2221,7 @@ SPLICE: [
 | pattern_ident
 | constr_eval  (* splices as multiple prods *)
 | tactic_then_last  (* todo: dependency on c.edit_mlg edit?? really useful? *)
+| ltac2_tactic_then_last
 | Prim.name
 | ltac_selector
 | Constr.ident
@@ -1993,7 +2376,6 @@ SPLICE: [
 | search_where
 | message_token
 | input_fun
-| tactic_then_last
 | ltac_use_default
 | toplevel_selector_temp
 | comment
@@ -2001,14 +2383,24 @@ SPLICE: [
 | match_context_rule
 | match_rule
 | by_notation
+| lnatural
+| nat_or_anti
+| globref
+| let_binder
+| refglobals (* Ltac2 *)
+| syntax_modifiers
+| array_elems
+| ltac2_expr
+| G_LTAC2_input_fun
+| ltac2_simple_intropattern_closed
+| ltac2_with_bindings
 ] (* end SPLICE *)
 
 RENAME: [
-| clause clause_dft_concl
-
 | tactic3 ltac_expr3  (* todo: can't figure out how this gets mapped by coqpp *)
 | tactic1 ltac_expr1  (* todo: can't figure out how this gets mapped by coqpp *)
 | tactic0 ltac_expr0  (* todo: can't figure out how this gets mapped by coqpp *)
+| ltac1_expr ltac_expr
 | tactic_expr5 ltac_expr
 | tactic_expr4 ltac_expr4
 | tactic_expr3 ltac_expr3
@@ -2029,6 +2421,7 @@ RENAME: [
 | ssexpr35 ssexpr (* strange in mlg, ssexpr50 is after this *)
 
 | tactic_then_gen for_each_goal
+| ltac2_tactic_then_gen ltac2_for_each_goal
 | selector_body selector
 | match_hyps match_hyp
 
@@ -2060,6 +2453,20 @@ RENAME: [
 | numnotoption numeral_modifier
 | tactic_arg_compat tactic_arg
 | lconstr_pattern cpattern
+| Pltac.tactic ltac_expr
+| sexpr ltac2_scope
+| tac2type5 ltac2_type
+| tac2type2 ltac2_type2
+| tac2type1 ltac2_type1
+| tac2type0 ltac2_type0
+| typ_param ltac2_typevar
+| tac2expr6 ltac2_expr
+| tac2expr5 ltac2_expr5
+| tac2expr3 ltac2_expr3
+| tac2expr2 ltac2_expr2
+| tac2expr1 ltac2_expr1
+| tac2expr0 ltac2_expr0
+| gmatch_list goal_match_list
 ]
 
 simple_tactic: [
@@ -2081,6 +2488,7 @@ SPLICE: [
 | command_entry
 | ltac_builtins
 | ltac_constructs
+| ltac2_constructs
 | ltac_defined_tactics
 | tactic_notation_tactics
 ]
@@ -2095,6 +2503,45 @@ NOTINRSTS: [
 | simple_tactic
 | REACHABLE
 | NOTINRSTS
+| l1_tactic
+| l2_tactic
+| l3_tactic
+| binder_tactic
+| value_tactic
+| ltac2_entry
+(* ltac2 syntactic classes *)
+| q_intropatterns
+| q_intropattern
+| q_ident
+| q_destruction_arg
+| q_with_bindings
+| q_bindings
+| q_strategy_flag
+| q_reference
+| q_clause
+| q_occurrences
+| q_induction_clause
+| q_conversion
+| q_rewriting
+| q_dispatch
+| q_hintdb
+| q_move_location
+| q_pose
+| q_assert
+| q_constr_matching
+| q_goal_matching
+
+(* todo: figure these out
+(*Warning: editedGrammar: Undefined symbol 'ltac1_expr' *)
+| dangling_pattern_extension_rule
+| vernac_aux
+| subprf
+| tactic_mode
+| tac2expr_in_env (* no refs *)
+| tac2mode (* no refs *)
+| ltac_use_default (* from tac2mode *)
+| tacticals
+*)
 ]
 
 REACHABLE: [
diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml
index 0f8144cbcf..0ac652c0db 100644
--- a/doc/tools/docgram/doc_grammar.ml
+++ b/doc/tools/docgram/doc_grammar.ml
@@ -732,6 +732,8 @@ let rec edit_prod g top edit_map prod =
   let splice_prods = match prod with
     | Snterm nt :: [] when is_splice nt ->
       get_splice_prods nt
+    | Snterm nt :: Sedit2 ("TAG", _) :: [] when is_splice nt ->
+      get_splice_prods nt
     | _ -> []
   in
   if top && splice_prods <> [] then
@@ -1901,7 +1903,8 @@ let process_rst g file args seen tac_prods cmd_prods =
     "doc/sphinx/proof-engine/ltac.rst";
     "doc/sphinx/proof-engine/ltac2.rst";
     "doc/sphinx/proof-engine/vernacular-commands.rst";
-    "doc/sphinx/user-extensions/syntax-extensions.rst"
+    "doc/sphinx/user-extensions/syntax-extensions.rst";
+    "doc/sphinx/proof-engine/vernacular-commands.rst"
   ]
   in
 
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 4c76ad9dda..7f4e92fc37 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -117,9 +117,14 @@ operconstr0: [
 | "{|" record_declaration bar_cbrace
 | "{" binder_constr "}"
 | "`{" operconstr200 "}"
+| test_array_opening "[" "|" array_elems "|" lconstr type_cstr test_array_closing "|" "]" univ_instance
 | "`(" operconstr200 ")"
 ]
 
+array_elems: [
+| LIST0 lconstr SEP ";"
+]
+
 record_declaration: [
 | fields_def
 ]
@@ -650,6 +655,17 @@ command: [
 | "Show" "Ltac" "Profile" "CutOff" int
 | "Show" "Ltac" "Profile" string
 | "Show" "Lia" "Profile"      (* micromega plugin *)
+| "Add" "Zify" "InjTyp" constr      (* micromega plugin *)
+| "Add" "Zify" "BinOp" constr      (* micromega plugin *)
+| "Add" "Zify" "UnOp" constr      (* micromega plugin *)
+| "Add" "Zify" "CstOp" constr      (* micromega plugin *)
+| "Add" "Zify" "BinRel" constr      (* micromega plugin *)
+| "Add" "Zify" "PropOp" constr      (* micromega plugin *)
+| "Add" "Zify" "PropBinOp" constr      (* micromega plugin *)
+| "Add" "Zify" "PropUOp" constr      (* micromega plugin *)
+| "Add" "Zify" "BinOpSpec" constr      (* micromega plugin *)
+| "Add" "Zify" "UnOpSpec" constr      (* micromega plugin *)
+| "Add" "Zify" "Saturate" constr      (* micromega plugin *)
 | "Add" "InjTyp" constr      (* micromega plugin *)
 | "Add" "BinOp" constr      (* micromega plugin *)
 | "Add" "UnOp" constr      (* micromega plugin *)
@@ -658,7 +674,6 @@ command: [
 | "Add" "PropOp" constr      (* micromega plugin *)
 | "Add" "PropBinOp" constr      (* micromega plugin *)
 | "Add" "PropUOp" constr      (* micromega plugin *)
-| "Add" "Spec" constr      (* micromega plugin *)
 | "Add" "BinOpSpec" constr      (* micromega plugin *)
 | "Add" "UnOpSpec" constr      (* micromega plugin *)
 | "Add" "Saturate" constr      (* micromega plugin *)
@@ -667,6 +682,8 @@ command: [
 | "Show" "Zify" "UnOp"      (* micromega plugin *)
 | "Show" "Zify" "CstOp"      (* micromega plugin *)
 | "Show" "Zify" "BinRel"      (* micromega plugin *)
+| "Show" "Zify" "UnOpSpec"      (* micromega plugin *)
+| "Show" "Zify" "BinOpSpec"      (* micromega plugin *)
 | "Show" "Zify" "Spec"      (* micromega plugin *)
 | "Add" "Ring" ident ":" constr OPT ring_mods      (* setoid_ring plugin *)
 | "Print" "Rings"      (* setoid_ring plugin *)
@@ -674,6 +691,9 @@ command: [
 | "Print" "Fields"      (* setoid_ring plugin *)
 | "Numeral" "Notation" reference reference reference ":" ident numnotoption
 | "String" "Notation" reference reference reference ":" ident
+| "Ltac2" ltac2_entry      (* Ltac2 plugin *)
+| "Ltac2" "Eval" ltac2_expr      (* Ltac2 plugin *)
+| "Print" "Ltac2" reference      (* Ltac2 plugin *)
 ]
 
 reference_or_constr: [
@@ -785,7 +805,7 @@ gallina: [
 | "Combined" "Scheme" identref "from" LIST1 identref SEP ","
 | "Register" global "as" qualid
 | "Register" "Inline" global
-| "Primitive" identref OPT [ ":" lconstr ] ":=" register_token
+| "Primitive" ident_decl OPT [ ":" lconstr ] ":=" register_token
 | "Universe" LIST1 identref
 | "Universes" LIST1 identref
 | "Constraint" LIST1 univ_constraint SEP ","
@@ -866,7 +886,7 @@ reduce: [
 ]
 
 decl_notation: [
-| ne_lstring ":=" constr only_parsing OPT [ ":" IDENT ]
+| ne_lstring ":=" constr syntax_modifiers OPT [ ":" IDENT ]
 ]
 
 decl_sep: [
@@ -1347,12 +1367,12 @@ syntax: [
 | "Delimit" "Scope" IDENT; "with" IDENT
 | "Undelimit" "Scope" IDENT
 | "Bind" "Scope" IDENT; "with" LIST1 class_rawexpr
-| "Infix" ne_lstring ":=" constr [ "(" LIST1 syntax_modifier SEP "," ")" | ] OPT [ ":" IDENT ]
+| "Infix" ne_lstring ":=" constr syntax_modifiers OPT [ ":" IDENT ]
 | "Notation" identref LIST0 ident ":=" constr only_parsing
-| "Notation" lstring ":=" constr [ "(" LIST1 syntax_modifier SEP "," ")" | ] OPT [ ":" IDENT ]
+| "Notation" lstring ":=" constr syntax_modifiers OPT [ ":" IDENT ]
 | "Format" "Notation" STRING STRING STRING
-| "Reserved" "Infix" ne_lstring [ "(" LIST1 syntax_modifier SEP "," ")" | ]
-| "Reserved" "Notation" ne_lstring [ "(" LIST1 syntax_modifier SEP "," ")" | ]
+| "Reserved" "Infix" ne_lstring syntax_modifiers
+| "Reserved" "Notation" ne_lstring syntax_modifiers
 ]
 
 only_parsing: [
@@ -1381,6 +1401,11 @@ syntax_modifier: [
 | IDENT syntax_extension_type
 ]
 
+syntax_modifiers: [
+| "(" LIST1 syntax_modifier SEP "," ")"
+|
+]
+
 syntax_extension_type: [
 | "ident"
 | "global"
@@ -1987,7 +2012,6 @@ failkw: [
 binder_tactic: [
 | "fun" LIST1 input_fun "=>" tactic_expr5
 | "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" tactic_expr5
-| "info" tactic_expr5
 ]
 
 tactic_arg_compat: [
@@ -2542,3 +2566,642 @@ numnotoption: [
 | "(" "abstract" "after" bignat ")"
 ]
 
+tac2pat1: [
+| Prim.qualid LIST1 tac2pat0      (* Ltac2 plugin *)
+| Prim.qualid      (* Ltac2 plugin *)
+| "[" "]"      (* Ltac2 plugin *)
+| tac2pat0 "::" tac2pat0      (* Ltac2 plugin *)
+| tac2pat0      (* Ltac2 plugin *)
+]
+
+tac2pat0: [
+| "_"      (* Ltac2 plugin *)
+| "()"      (* Ltac2 plugin *)
+| Prim.qualid      (* Ltac2 plugin *)
+| "(" atomic_tac2pat ")"      (* Ltac2 plugin *)
+]
+
+atomic_tac2pat: [
+|      (* Ltac2 plugin *)
+| tac2pat1 ":" tac2type5      (* Ltac2 plugin *)
+| tac2pat1 "," LIST0 tac2pat1 SEP ","      (* Ltac2 plugin *)
+| tac2pat1      (* Ltac2 plugin *)
+]
+
+tac2expr6: [
+| tac2expr5 ";" tac2expr6      (* Ltac2 plugin *)
+| tac2expr5      (* Ltac2 plugin *)
+]
+
+tac2expr5: [
+| "fun" LIST1 G_LTAC2_input_fun "=>" tac2expr6      (* Ltac2 plugin *)
+| "let" rec_flag LIST1 G_LTAC2_let_clause SEP "with" "in" tac2expr6      (* Ltac2 plugin *)
+| "match" tac2expr5 "with" G_LTAC2_branches "end"      (* Ltac2 plugin *)
+| tac2expr4      (* Ltac2 plugin *)
+]
+
+tac2expr4: [
+| tac2expr3      (* Ltac2 plugin *)
+]
+
+tac2expr3: [
+| tac2expr2 "," LIST1 tac2expr2 SEP ","      (* Ltac2 plugin *)
+| tac2expr2      (* Ltac2 plugin *)
+]
+
+tac2expr2: [
+| tac2expr1 "::" tac2expr2      (* Ltac2 plugin *)
+| tac2expr1      (* Ltac2 plugin *)
+]
+
+tac2expr1: [
+| tac2expr0 LIST1 tac2expr0      (* Ltac2 plugin *)
+| tac2expr0 ".(" Prim.qualid ")"      (* Ltac2 plugin *)
+| tac2expr0 ".(" Prim.qualid ")" ":=" tac2expr5      (* Ltac2 plugin *)
+| tac2expr0      (* Ltac2 plugin *)
+]
+
+tac2expr0: [
+| "(" tac2expr6 ")"      (* Ltac2 plugin *)
+| "(" tac2expr6 ":" tac2type5 ")"      (* Ltac2 plugin *)
+| "()"      (* Ltac2 plugin *)
+| "(" ")"      (* Ltac2 plugin *)
+| "[" LIST0 tac2expr5 SEP ";" "]"      (* Ltac2 plugin *)
+| "{" tac2rec_fieldexprs "}"      (* Ltac2 plugin *)
+| G_LTAC2_tactic_atom      (* Ltac2 plugin *)
+]
+
+G_LTAC2_branches: [
+|      (* Ltac2 plugin *)
+| "|" LIST1 branch SEP "|"      (* Ltac2 plugin *)
+| LIST1 branch SEP "|"      (* Ltac2 plugin *)
+]
+
+branch: [
+| tac2pat1 "=>" tac2expr6      (* Ltac2 plugin *)
+]
+
+rec_flag: [
+| "rec"      (* Ltac2 plugin *)
+|      (* Ltac2 plugin *)
+]
+
+mut_flag: [
+| "mutable"      (* Ltac2 plugin *)
+|      (* Ltac2 plugin *)
+]
+
+typ_param: [
+| "'" Prim.ident      (* Ltac2 plugin *)
+]
+
+G_LTAC2_tactic_atom: [
+| Prim.integer      (* Ltac2 plugin *)
+| Prim.string      (* Ltac2 plugin *)
+| Prim.qualid      (* Ltac2 plugin *)
+| "@" Prim.ident      (* Ltac2 plugin *)
+| "&" lident      (* Ltac2 plugin *)
+| "'" Constr.constr      (* Ltac2 plugin *)
+| "constr" ":" "(" Constr.lconstr ")"      (* Ltac2 plugin *)
+| "open_constr" ":" "(" Constr.lconstr ")"      (* Ltac2 plugin *)
+| "ident" ":" "(" lident ")"      (* Ltac2 plugin *)
+| "pattern" ":" "(" Constr.lconstr_pattern ")"      (* Ltac2 plugin *)
+| "reference" ":" "(" globref ")"      (* Ltac2 plugin *)
+| "ltac1" ":" "(" ltac1_expr_in_env ")"      (* Ltac2 plugin *)
+| "ltac1val" ":" "(" ltac1_expr_in_env ")"      (* Ltac2 plugin *)
+]
+
+ltac1_expr_in_env: [
+| test_ltac1_env LIST0 locident "|-" ltac1_expr      (* Ltac2 plugin *)
+| ltac1_expr      (* Ltac2 plugin *)
+]
+
+tac2expr_in_env: [
+| test_ltac1_env LIST0 locident "|-" tac2expr6      (* Ltac2 plugin *)
+| tac2expr6      (* Ltac2 plugin *)
+]
+
+G_LTAC2_let_clause: [
+| let_binder ":=" tac2expr6      (* Ltac2 plugin *)
+]
+
+let_binder: [
+| LIST1 G_LTAC2_input_fun      (* Ltac2 plugin *)
+]
+
+tac2type5: [
+| tac2type2 "->" tac2type5      (* Ltac2 plugin *)
+| tac2type2      (* Ltac2 plugin *)
+]
+
+tac2type2: [
+| tac2type1 "*" LIST1 tac2type1 SEP "*"      (* Ltac2 plugin *)
+| tac2type1      (* Ltac2 plugin *)
+]
+
+tac2type1: [
+| tac2type0 Prim.qualid      (* Ltac2 plugin *)
+| tac2type0      (* Ltac2 plugin *)
+]
+
+tac2type0: [
+| "(" LIST1 tac2type5 SEP "," ")" OPT Prim.qualid      (* Ltac2 plugin *)
+| typ_param      (* Ltac2 plugin *)
+| "_"      (* Ltac2 plugin *)
+| Prim.qualid      (* Ltac2 plugin *)
+]
+
+locident: [
+| Prim.ident      (* Ltac2 plugin *)
+]
+
+G_LTAC2_binder: [
+| "_"      (* Ltac2 plugin *)
+| Prim.ident      (* Ltac2 plugin *)
+]
+
+G_LTAC2_input_fun: [
+| tac2pat0      (* Ltac2 plugin *)
+]
+
+tac2def_body: [
+| G_LTAC2_binder LIST0 G_LTAC2_input_fun ":=" tac2expr6      (* Ltac2 plugin *)
+]
+
+tac2def_val: [
+| mut_flag rec_flag LIST1 tac2def_body SEP "with"      (* Ltac2 plugin *)
+]
+
+tac2def_mut: [
+| "Set" Prim.qualid OPT [ "as" locident ] ":=" tac2expr6      (* Ltac2 plugin *)
+]
+
+tac2typ_knd: [
+| tac2type5      (* Ltac2 plugin *)
+| "[" ".." "]"      (* Ltac2 plugin *)
+| "[" tac2alg_constructors "]"      (* Ltac2 plugin *)
+| "{" tac2rec_fields "}"      (* Ltac2 plugin *)
+]
+
+tac2alg_constructors: [
+| "|" LIST1 tac2alg_constructor SEP "|"      (* Ltac2 plugin *)
+| LIST0 tac2alg_constructor SEP "|"      (* Ltac2 plugin *)
+]
+
+tac2alg_constructor: [
+| Prim.ident      (* Ltac2 plugin *)
+| Prim.ident "(" LIST0 tac2type5 SEP "," ")"      (* Ltac2 plugin *)
+]
+
+tac2rec_fields: [
+| tac2rec_field ";" tac2rec_fields      (* Ltac2 plugin *)
+| tac2rec_field ";"      (* Ltac2 plugin *)
+| tac2rec_field      (* Ltac2 plugin *)
+|      (* Ltac2 plugin *)
+]
+
+tac2rec_field: [
+| mut_flag Prim.ident ":" tac2type5      (* Ltac2 plugin *)
+]
+
+tac2rec_fieldexprs: [
+| tac2rec_fieldexpr ";" tac2rec_fieldexprs      (* Ltac2 plugin *)
+| tac2rec_fieldexpr ";"      (* Ltac2 plugin *)
+| tac2rec_fieldexpr      (* Ltac2 plugin *)
+|      (* Ltac2 plugin *)
+]
+
+tac2rec_fieldexpr: [
+| Prim.qualid ":=" tac2expr1      (* Ltac2 plugin *)
+]
+
+tac2typ_prm: [
+|      (* Ltac2 plugin *)
+| typ_param      (* Ltac2 plugin *)
+| "(" LIST1 typ_param SEP "," ")"      (* Ltac2 plugin *)
+]
+
+tac2typ_def: [
+| tac2typ_prm Prim.qualid tac2type_body      (* Ltac2 plugin *)
+]
+
+tac2type_body: [
+|      (* Ltac2 plugin *)
+| ":=" tac2typ_knd      (* Ltac2 plugin *)
+| "::=" tac2typ_knd      (* Ltac2 plugin *)
+]
+
+tac2def_typ: [
+| "Type" rec_flag LIST1 tac2typ_def SEP "with"      (* Ltac2 plugin *)
+]
+
+tac2def_ext: [
+| "@" "external" locident ":" tac2type5 ":=" Prim.string Prim.string      (* Ltac2 plugin *)
+]
+
+syn_node: [
+| "_"      (* Ltac2 plugin *)
+| Prim.ident      (* Ltac2 plugin *)
+]
+
+sexpr: [
+| Prim.string      (* Ltac2 plugin *)
+| Prim.integer      (* Ltac2 plugin *)
+| syn_node      (* Ltac2 plugin *)
+| syn_node "(" LIST1 sexpr SEP "," ")"      (* Ltac2 plugin *)
+]
+
+syn_level: [
+|      (* Ltac2 plugin *)
+| ":" Prim.integer      (* Ltac2 plugin *)
+]
+
+tac2def_syn: [
+| "Notation" LIST1 sexpr syn_level ":=" tac2expr6      (* Ltac2 plugin *)
+]
+
+lident: [
+| Prim.ident      (* Ltac2 plugin *)
+]
+
+globref: [
+| "&" Prim.ident      (* Ltac2 plugin *)
+| Prim.qualid      (* Ltac2 plugin *)
+]
+
+anti: [
+| "$" Prim.ident      (* Ltac2 plugin *)
+]
+
+ident_or_anti: [
+| lident      (* Ltac2 plugin *)
+| "$" Prim.ident      (* Ltac2 plugin *)
+]
+
+lnatural: [
+| Prim.natural      (* Ltac2 plugin *)
+]
+
+q_ident: [
+| ident_or_anti      (* Ltac2 plugin *)
+]
+
+qhyp: [
+| anti      (* Ltac2 plugin *)
+| lnatural      (* Ltac2 plugin *)
+| lident      (* Ltac2 plugin *)
+]
+
+G_LTAC2_simple_binding: [
+| "(" qhyp ":=" Constr.lconstr ")"      (* Ltac2 plugin *)
+]
+
+G_LTAC2_bindings: [
+| test_lpar_idnum_coloneq LIST1 G_LTAC2_simple_binding      (* Ltac2 plugin *)
+| LIST1 Constr.constr      (* Ltac2 plugin *)
+]
+
+q_bindings: [
+| G_LTAC2_bindings      (* Ltac2 plugin *)
+]
+
+q_with_bindings: [
+| G_LTAC2_with_bindings      (* Ltac2 plugin *)
+]
+
+G_LTAC2_intropatterns: [
+| LIST0 nonsimple_intropattern      (* Ltac2 plugin *)
+]
+
+G_LTAC2_or_and_intropattern: [
+| "[" LIST1 G_LTAC2_intropatterns SEP "|" "]"      (* Ltac2 plugin *)
+| "()"      (* Ltac2 plugin *)
+| "(" G_LTAC2_simple_intropattern ")"      (* Ltac2 plugin *)
+| "(" G_LTAC2_simple_intropattern "," LIST1 G_LTAC2_simple_intropattern SEP "," ")"      (* Ltac2 plugin *)
+| "(" G_LTAC2_simple_intropattern "&" LIST1 G_LTAC2_simple_intropattern SEP "&" ")"      (* Ltac2 plugin *)
+]
+
+G_LTAC2_equality_intropattern: [
+| "->"      (* Ltac2 plugin *)
+| "<-"      (* Ltac2 plugin *)
+| "[=" G_LTAC2_intropatterns "]"      (* Ltac2 plugin *)
+]
+
+G_LTAC2_naming_intropattern: [
+| LEFTQMARK lident      (* Ltac2 plugin *)
+| "?$" lident      (* Ltac2 plugin *)
+| "?"      (* Ltac2 plugin *)
+| ident_or_anti      (* Ltac2 plugin *)
+]
+
+nonsimple_intropattern: [
+| G_LTAC2_simple_intropattern      (* Ltac2 plugin *)
+| "*"      (* Ltac2 plugin *)
+| "**"      (* Ltac2 plugin *)
+]
+
+G_LTAC2_simple_intropattern: [
+| G_LTAC2_simple_intropattern_closed      (* Ltac2 plugin *)
+]
+
+G_LTAC2_simple_intropattern_closed: [
+| G_LTAC2_or_and_intropattern      (* Ltac2 plugin *)
+| G_LTAC2_equality_intropattern      (* Ltac2 plugin *)
+| "_"      (* Ltac2 plugin *)
+| G_LTAC2_naming_intropattern      (* Ltac2 plugin *)
+]
+
+q_intropatterns: [
+| G_LTAC2_intropatterns      (* Ltac2 plugin *)
+]
+
+q_intropattern: [
+| G_LTAC2_simple_intropattern      (* Ltac2 plugin *)
+]
+
+nat_or_anti: [
+| lnatural      (* Ltac2 plugin *)
+| "$" Prim.ident      (* Ltac2 plugin *)
+]
+
+G_LTAC2_eqn_ipat: [
+| "eqn" ":" G_LTAC2_naming_intropattern      (* Ltac2 plugin *)
+|      (* Ltac2 plugin *)
+]
+
+G_LTAC2_with_bindings: [
+| "with" G_LTAC2_bindings      (* Ltac2 plugin *)
+|      (* Ltac2 plugin *)
+]
+
+G_LTAC2_constr_with_bindings: [
+| Constr.constr G_LTAC2_with_bindings      (* Ltac2 plugin *)
+]
+
+G_LTAC2_destruction_arg: [
+| lnatural      (* Ltac2 plugin *)
+| lident      (* Ltac2 plugin *)
+| G_LTAC2_constr_with_bindings      (* Ltac2 plugin *)
+]
+
+q_destruction_arg: [
+| G_LTAC2_destruction_arg      (* Ltac2 plugin *)
+]
+
+G_LTAC2_as_or_and_ipat: [
+| "as" G_LTAC2_or_and_intropattern      (* Ltac2 plugin *)
+|      (* Ltac2 plugin *)
+]
+
+G_LTAC2_occs_nums: [
+| LIST1 nat_or_anti      (* Ltac2 plugin *)
+| "-" nat_or_anti LIST0 nat_or_anti      (* Ltac2 plugin *)
+]
+
+G_LTAC2_occs: [
+| "at" G_LTAC2_occs_nums      (* Ltac2 plugin *)
+|      (* Ltac2 plugin *)
+]
+
+G_LTAC2_hypident: [
+| ident_or_anti      (* Ltac2 plugin *)
+| "(" "type" "of" ident_or_anti ")"      (* Ltac2 plugin *)
+| "(" "value" "of" ident_or_anti ")"      (* Ltac2 plugin *)
+]
+
+G_LTAC2_hypident_occ: [
+| G_LTAC2_hypident G_LTAC2_occs      (* Ltac2 plugin *)
+]
+
+G_LTAC2_in_clause: [
+| "*" G_LTAC2_occs      (* Ltac2 plugin *)
+| "*" "|-" G_LTAC2_concl_occ      (* Ltac2 plugin *)
+| LIST0 G_LTAC2_hypident_occ SEP "," "|-" G_LTAC2_concl_occ      (* Ltac2 plugin *)
+| LIST0 G_LTAC2_hypident_occ SEP ","      (* Ltac2 plugin *)
+]
+
+clause: [
+| "in" G_LTAC2_in_clause      (* Ltac2 plugin *)
+| "at" G_LTAC2_occs_nums      (* Ltac2 plugin *)
+]
+
+q_clause: [
+| clause      (* Ltac2 plugin *)
+]
+
+G_LTAC2_concl_occ: [
+| "*" G_LTAC2_occs      (* Ltac2 plugin *)
+|      (* Ltac2 plugin *)
+]
+
+G_LTAC2_induction_clause: [
+| G_LTAC2_destruction_arg G_LTAC2_as_or_and_ipat G_LTAC2_eqn_ipat OPT clause      (* Ltac2 plugin *)
+]
+
+q_induction_clause: [
+| G_LTAC2_induction_clause      (* Ltac2 plugin *)
+]
+
+G_LTAC2_conversion: [
+| Constr.constr      (* Ltac2 plugin *)
+| Constr.constr "with" Constr.constr      (* Ltac2 plugin *)
+]
+
+q_conversion: [
+| G_LTAC2_conversion      (* Ltac2 plugin *)
+]
+
+ltac2_orient: [
+| "->"      (* Ltac2 plugin *)
+| "<-"      (* Ltac2 plugin *)
+|      (* Ltac2 plugin *)
+]
+
+G_LTAC2_rewriter: [
+| "!" G_LTAC2_constr_with_bindings      (* Ltac2 plugin *)
+| [ "?" | LEFTQMARK ] G_LTAC2_constr_with_bindings      (* Ltac2 plugin *)
+| lnatural "!" G_LTAC2_constr_with_bindings      (* Ltac2 plugin *)
+| lnatural [ "?" | LEFTQMARK ] G_LTAC2_constr_with_bindings      (* Ltac2 plugin *)
+| lnatural G_LTAC2_constr_with_bindings      (* Ltac2 plugin *)
+| G_LTAC2_constr_with_bindings      (* Ltac2 plugin *)
+]
+
+G_LTAC2_oriented_rewriter: [
+| ltac2_orient G_LTAC2_rewriter      (* Ltac2 plugin *)
+]
+
+q_rewriting: [
+| G_LTAC2_oriented_rewriter      (* Ltac2 plugin *)
+]
+
+G_LTAC2_tactic_then_last: [
+| "|" LIST0 ( OPT tac2expr6 ) SEP "|"      (* Ltac2 plugin *)
+|      (* Ltac2 plugin *)
+]
+
+G_LTAC2_tactic_then_gen: [
+| tac2expr6 "|" G_LTAC2_tactic_then_gen      (* Ltac2 plugin *)
+| tac2expr6 ".." G_LTAC2_tactic_then_last      (* Ltac2 plugin *)
+| ".." G_LTAC2_tactic_then_last      (* Ltac2 plugin *)
+| tac2expr6      (* Ltac2 plugin *)
+| "|" G_LTAC2_tactic_then_gen      (* Ltac2 plugin *)
+|      (* Ltac2 plugin *)
+]
+
+q_dispatch: [
+| G_LTAC2_tactic_then_gen      (* Ltac2 plugin *)
+]
+
+q_occurrences: [
+| G_LTAC2_occs      (* Ltac2 plugin *)
+]
+
+red_flag: [
+| "beta"      (* Ltac2 plugin *)
+| "iota"      (* Ltac2 plugin *)
+| "match"      (* Ltac2 plugin *)
+| "fix"      (* Ltac2 plugin *)
+| "cofix"      (* Ltac2 plugin *)
+| "zeta"      (* Ltac2 plugin *)
+| "delta" G_LTAC2_delta_flag      (* Ltac2 plugin *)
+]
+
+refglobal: [
+| "&" Prim.ident      (* Ltac2 plugin *)
+| Prim.qualid      (* Ltac2 plugin *)
+| "$" Prim.ident      (* Ltac2 plugin *)
+]
+
+q_reference: [
+| refglobal      (* Ltac2 plugin *)
+]
+
+refglobals: [
+| LIST1 refglobal      (* Ltac2 plugin *)
+]
+
+G_LTAC2_delta_flag: [
+| "-" "[" refglobals "]"      (* Ltac2 plugin *)
+| "[" refglobals "]"      (* Ltac2 plugin *)
+|      (* Ltac2 plugin *)
+]
+
+G_LTAC2_strategy_flag: [
+| LIST1 red_flag      (* Ltac2 plugin *)
+| G_LTAC2_delta_flag      (* Ltac2 plugin *)
+]
+
+q_strategy_flag: [
+| G_LTAC2_strategy_flag      (* Ltac2 plugin *)
+]
+
+hintdb: [
+| "*"      (* Ltac2 plugin *)
+| LIST1 ident_or_anti      (* Ltac2 plugin *)
+]
+
+q_hintdb: [
+| hintdb      (* Ltac2 plugin *)
+]
+
+G_LTAC2_match_pattern: [
+| "context" OPT Prim.ident "[" Constr.lconstr_pattern "]"      (* Ltac2 plugin *)
+| Constr.lconstr_pattern      (* Ltac2 plugin *)
+]
+
+G_LTAC2_match_rule: [
+| G_LTAC2_match_pattern "=>" tac2expr6      (* Ltac2 plugin *)
+]
+
+G_LTAC2_match_list: [
+| LIST1 G_LTAC2_match_rule SEP "|"      (* Ltac2 plugin *)
+| "|" LIST1 G_LTAC2_match_rule SEP "|"      (* Ltac2 plugin *)
+]
+
+q_constr_matching: [
+| G_LTAC2_match_list      (* Ltac2 plugin *)
+]
+
+gmatch_hyp_pattern: [
+| Prim.name ":" G_LTAC2_match_pattern      (* Ltac2 plugin *)
+]
+
+gmatch_pattern: [
+| "[" LIST0 gmatch_hyp_pattern SEP "," "|-" G_LTAC2_match_pattern "]"      (* Ltac2 plugin *)
+]
+
+gmatch_rule: [
+| gmatch_pattern "=>" tac2expr6      (* Ltac2 plugin *)
+]
+
+gmatch_list: [
+| LIST1 gmatch_rule SEP "|"      (* Ltac2 plugin *)
+| "|" LIST1 gmatch_rule SEP "|"      (* Ltac2 plugin *)
+]
+
+q_goal_matching: [
+| gmatch_list      (* Ltac2 plugin *)
+]
+
+move_location: [
+| "at" "top"      (* Ltac2 plugin *)
+| "at" "bottom"      (* Ltac2 plugin *)
+| "after" ident_or_anti      (* Ltac2 plugin *)
+| "before" ident_or_anti      (* Ltac2 plugin *)
+]
+
+q_move_location: [
+| move_location      (* Ltac2 plugin *)
+]
+
+G_LTAC2_as_name: [
+|      (* Ltac2 plugin *)
+| "as" ident_or_anti      (* Ltac2 plugin *)
+]
+
+pose: [
+| test_lpar_id_coloneq "(" ident_or_anti ":=" Constr.lconstr ")"      (* Ltac2 plugin *)
+| Constr.constr G_LTAC2_as_name      (* Ltac2 plugin *)
+]
+
+q_pose: [
+| pose      (* Ltac2 plugin *)
+]
+
+G_LTAC2_as_ipat: [
+| "as" G_LTAC2_simple_intropattern      (* Ltac2 plugin *)
+|      (* Ltac2 plugin *)
+]
+
+G_LTAC2_by_tactic: [
+| "by" tac2expr6      (* Ltac2 plugin *)
+|      (* Ltac2 plugin *)
+]
+
+assertion: [
+| test_lpar_id_coloneq "(" ident_or_anti ":=" Constr.lconstr ")"      (* Ltac2 plugin *)
+| test_lpar_id_colon "(" ident_or_anti ":" Constr.lconstr ")" G_LTAC2_by_tactic      (* Ltac2 plugin *)
+| Constr.constr G_LTAC2_as_ipat G_LTAC2_by_tactic      (* Ltac2 plugin *)
+]
+
+q_assert: [
+| assertion      (* Ltac2 plugin *)
+]
+
+ltac2_entry: [
+| tac2def_val      (* Ltac2 plugin *)
+| tac2def_typ      (* Ltac2 plugin *)
+| tac2def_ext      (* Ltac2 plugin *)
+| tac2def_syn      (* Ltac2 plugin *)
+| tac2def_mut      (* Ltac2 plugin *)
+]
+
+ltac2_expr: [
+| tac2expr6      (* Ltac2 plugin *)
+]
+
+tac2mode: [
+| ltac2_expr ltac_use_default      (* Ltac2 plugin *)
+| G_vernac.query_command      (* Ltac2 plugin *)
+]
+
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index f4bf51b6ba..84efc1e36c 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -45,6 +45,7 @@ term0: [
 | term_match
 | term_record
 | term_generalizing
+| "[|" LIST0 term SEP ";" "|" term OPT ( ":" type ) "|]" OPT univ_annot
 | term_ltac
 | "(" term ")"
 ]
@@ -192,6 +193,32 @@ NOTINRSTS: [
 | simple_tactic
 | REACHABLE
 | NOTINRSTS
+| l1_tactic
+| l3_tactic
+| l2_tactic
+| binder_tactic
+| value_tactic
+| ltac2_entry
+| q_intropatterns
+| q_intropattern
+| q_ident
+| q_destruction_arg
+| q_with_bindings
+| q_bindings
+| q_strategy_flag
+| q_reference
+| q_clause
+| q_occurrences
+| q_induction_clause
+| q_conversion
+| q_rewriting
+| q_dispatch
+| q_hintdb
+| q_move_location
+| q_pose
+| q_assert
+| q_constr_matching
+| q_goal_matching
 ]
 
 document: [
@@ -462,11 +489,11 @@ delta_flag: [
 ]
 
 strategy_flag: [
-| LIST1 red_flags
+| LIST1 red_flag
 | delta_flag
 ]
 
-red_flags: [
+red_flag: [
 | "beta"
 | "iota"
 | "match"
@@ -751,6 +778,26 @@ command: [
 | "Declare" "Reduction" ident ":=" red_expr
 | "Declare" "Custom" "Entry" ident
 | "Derive" ident "SuchThat" one_term "As" ident      (* derive plugin *)
+| "Extraction" qualid      (* extraction plugin *)
+| "Recursive" "Extraction" LIST1 qualid      (* extraction plugin *)
+| "Extraction" string LIST1 qualid      (* extraction plugin *)
+| "Extraction" "TestCompile" LIST1 qualid      (* extraction plugin *)
+| "Separate" "Extraction" LIST1 qualid      (* extraction plugin *)
+| "Extraction" "Library" ident      (* extraction plugin *)
+| "Recursive" "Extraction" "Library" ident      (* extraction plugin *)
+| "Extraction" "Language" language      (* extraction plugin *)
+| "Extraction" "Inline" LIST1 qualid      (* extraction plugin *)
+| "Extraction" "NoInline" LIST1 qualid      (* extraction plugin *)
+| "Print" "Extraction" "Inline"      (* extraction plugin *)
+| "Reset" "Extraction" "Inline"      (* extraction plugin *)
+| "Extraction" "Implicit" qualid "[" LIST0 int_or_id "]"      (* extraction plugin *)
+| "Extraction" "Blacklist" LIST1 ident      (* extraction plugin *)
+| "Print" "Extraction" "Blacklist"      (* extraction plugin *)
+| "Reset" "Extraction" "Blacklist"      (* extraction plugin *)
+| "Extract" "Constant" qualid LIST0 string "=>" [ ident | string ]      (* extraction plugin *)
+| "Extract" "Inlined" "Constant" qualid "=>" [ ident | string ]      (* extraction plugin *)
+| "Extract" "Inductive" qualid "=>" [ ident | string ] "[" LIST0 [ ident | string ] "]" OPT string      (* extraction plugin *)
+| "Show" "Extraction"      (* extraction plugin *)
 | "Proof"
 | "Proof" "Mode" string
 | "Proof" term
@@ -807,6 +854,17 @@ command: [
 | "Reset" "Ltac" "Profile"
 | "Show" "Ltac" "Profile" OPT [ "CutOff" int | string ]
 | "Show" "Lia" "Profile"      (* micromega plugin *)
+| "Add" "Zify" "InjTyp" one_term      (* micromega plugin *)
+| "Add" "Zify" "BinOp" one_term      (* micromega plugin *)
+| "Add" "Zify" "UnOp" one_term      (* micromega plugin *)
+| "Add" "Zify" "CstOp" one_term      (* micromega plugin *)
+| "Add" "Zify" "BinRel" one_term      (* micromega plugin *)
+| "Add" "Zify" "PropOp" one_term      (* micromega plugin *)
+| "Add" "Zify" "PropBinOp" one_term      (* micromega plugin *)
+| "Add" "Zify" "PropUOp" one_term      (* micromega plugin *)
+| "Add" "Zify" "BinOpSpec" one_term      (* micromega plugin *)
+| "Add" "Zify" "UnOpSpec" one_term      (* micromega plugin *)
+| "Add" "Zify" "Saturate" one_term      (* micromega plugin *)
 | "Add" "InjTyp" one_term      (* micromega plugin *)
 | "Add" "BinOp" one_term      (* micromega plugin *)
 | "Add" "UnOp" one_term      (* micromega plugin *)
@@ -815,7 +873,6 @@ command: [
 | "Add" "PropOp" one_term      (* micromega plugin *)
 | "Add" "PropBinOp" one_term      (* micromega plugin *)
 | "Add" "PropUOp" one_term      (* micromega plugin *)
-| "Add" "Spec" one_term      (* micromega plugin *)
 | "Add" "BinOpSpec" one_term      (* micromega plugin *)
 | "Add" "UnOpSpec" one_term      (* micromega plugin *)
 | "Add" "Saturate" one_term      (* micromega plugin *)
@@ -824,8 +881,13 @@ command: [
 | "Show" "Zify" "UnOp"      (* micromega plugin *)
 | "Show" "Zify" "CstOp"      (* micromega plugin *)
 | "Show" "Zify" "BinRel"      (* micromega plugin *)
+| "Show" "Zify" "UnOpSpec"      (* micromega plugin *)
+| "Show" "Zify" "BinOpSpec"      (* micromega plugin *)
 | "Show" "Zify" "Spec"      (* micromega plugin *)
 | "Add" "Ring" ident ":" one_term OPT ( "(" LIST1 ring_mod SEP "," ")" )      (* setoid_ring plugin *)
+| "Print" "Rings"      (* setoid_ring plugin *)
+| "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" )      (* setoid_ring plugin *)
+| "Print" "Fields"      (* setoid_ring plugin *)
 | "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident )
 | "Typeclasses" "Transparent" LIST0 qualid
 | "Typeclasses" "Opaque" LIST0 qualid
@@ -841,26 +903,6 @@ command: [
 | "Print" "Firstorder" "Solver"
 | "Function" fix_definition LIST0 ( "with" fix_definition )
 | "Functional" "Scheme" fun_scheme_arg LIST0 ( "with" fun_scheme_arg )
-| "Extraction" qualid      (* extraction plugin *)
-| "Recursive" "Extraction" LIST1 qualid      (* extraction plugin *)
-| "Extraction" string LIST1 qualid      (* extraction plugin *)
-| "Extraction" "TestCompile" LIST1 qualid      (* extraction plugin *)
-| "Separate" "Extraction" LIST1 qualid      (* extraction plugin *)
-| "Extraction" "Library" ident      (* extraction plugin *)
-| "Recursive" "Extraction" "Library" ident      (* extraction plugin *)
-| "Extraction" "Language" language      (* extraction plugin *)
-| "Extraction" "Inline" LIST1 qualid      (* extraction plugin *)
-| "Extraction" "NoInline" LIST1 qualid      (* extraction plugin *)
-| "Print" "Extraction" "Inline"      (* extraction plugin *)
-| "Reset" "Extraction" "Inline"      (* extraction plugin *)
-| "Extraction" "Implicit" qualid "[" LIST0 int_or_id "]"      (* extraction plugin *)
-| "Extraction" "Blacklist" LIST1 ident      (* extraction plugin *)
-| "Print" "Extraction" "Blacklist"      (* extraction plugin *)
-| "Reset" "Extraction" "Blacklist"      (* extraction plugin *)
-| "Extract" "Constant" qualid LIST0 string "=>" [ ident | string ]      (* extraction plugin *)
-| "Extract" "Inlined" "Constant" qualid "=>" [ ident | string ]      (* extraction plugin *)
-| "Extract" "Inductive" qualid "=>" [ ident | string ] "[" LIST0 [ ident | string ] "]" OPT string      (* extraction plugin *)
-| "Show" "Extraction"      (* extraction plugin *)
 | "Functional" "Case" fun_scheme_arg      (* funind plugin *)
 | "Generate" "graph" "for" qualid      (* funind plugin *)
 | "Hint" "Rewrite" OPT [ "->" | "<-" ] LIST1 one_term OPT ( "using" ltac_expr ) OPT ( ":" LIST0 ident )
@@ -870,9 +912,6 @@ command: [
 | "Derive" "Dependent" "Inversion_clear" ident "with" one_term "Sort" sort_family
 | "Declare" "Left" "Step" one_term
 | "Declare" "Right" "Step" one_term
-| "Print" "Rings"      (* setoid_ring plugin *)
-| "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" )      (* setoid_ring plugin *)
-| "Print" "Fields"      (* setoid_ring plugin *)
 | "Numeral" "Notation" qualid qualid qualid ":" scope_name OPT numeral_modifier
 | "String" "Notation" qualid qualid qualid ":" scope_name
 | "SubClass" ident_decl def_body
@@ -889,7 +928,7 @@ command: [
 | "Combined" "Scheme" ident "from" LIST1 ident SEP ","
 | "Register" qualid "as" qualid
 | "Register" "Inline" qualid
-| "Primitive" ident OPT [ ":" term ] ":=" "#" ident
+| "Primitive" ident_decl OPT [ ":" term ] ":=" "#" ident
 | "Universe" LIST1 ident
 | "Universes" LIST1 ident
 | "Constraint" LIST1 univ_constraint SEP ","
@@ -932,12 +971,12 @@ command: [
 | "Delimit" "Scope" scope_name "with" scope_key
 | "Undelimit" "Scope" scope_name
 | "Bind" "Scope" scope_name "with" LIST1 class
-| "Infix" string ":=" one_term OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" scope_name ]
+| "Infix" string ":=" one_term OPT ( "(" LIST1 syntax_modifier SEP "," ")" ) OPT [ ":" scope_name ]
 | "Notation" ident LIST0 ident ":=" one_term OPT ( "(" "only" "parsing" ")" )
-| "Notation" string ":=" one_term OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" scope_name ]
+| "Notation" string ":=" one_term OPT ( "(" LIST1 syntax_modifier SEP "," ")" ) OPT [ ":" scope_name ]
 | "Format" "Notation" string string string
-| "Reserved" "Infix" string OPT [ "(" LIST1 syntax_modifier SEP "," ")" ]
-| "Reserved" "Notation" string OPT [ "(" LIST1 syntax_modifier SEP "," ")" ]
+| "Reserved" "Infix" string OPT ( "(" LIST1 syntax_modifier SEP "," ")" )
+| "Reserved" "Notation" string OPT ( "(" LIST1 syntax_modifier SEP "," ")" )
 | "Eval" red_expr "in" term
 | "Compute" term
 | "Check" term
@@ -946,6 +985,14 @@ command: [
 | "SearchPattern" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
 | "SearchRewrite" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
 | "Search" LIST1 ( search_query ) OPT ( [ "inside" | "outside" ] LIST1 qualid )
+| "Ltac2" OPT "mutable" OPT "rec" tac2def_body LIST0 ( "with" tac2def_body )
+| "Ltac2" "Type" OPT "rec" tac2typ_def LIST0 ( "with" tac2typ_def )
+| "Ltac2" "@" "external" ident ":" ltac2_type ":=" string string
+| "Ltac2" "Notation" LIST1 ltac2_scope OPT ( ":" int ) ":=" ltac2_expr
+| "Ltac2" "Set" qualid OPT [ "as" ident ] ":=" ltac2_expr
+| "Ltac2" "Notation" [ string | lident ] ":=" ltac2_expr      (* Ltac2 plugin *)
+| "Ltac2" "Eval" ltac2_expr      (* Ltac2 plugin *)
+| "Print" "Ltac2" qualid      (* Ltac2 plugin *)
 | "Time" sentence
 | "Redirect" string sentence
 | "Timeout" num sentence
@@ -1044,8 +1091,170 @@ ltac_production_item: [
 | ident OPT ( "(" ident OPT ( "," string ) ")" )
 ]
 
+tac2expr_in_env: [
+| LIST0 ident "|-" ltac2_expr      (* Ltac2 plugin *)
+| ltac2_expr      (* Ltac2 plugin *)
+]
+
+ltac2_type: [
+| ltac2_type2 "->" ltac2_type      (* Ltac2 plugin *)
+| ltac2_type2      (* Ltac2 plugin *)
+]
+
+ltac2_type2: [
+| ltac2_type1 "*" LIST1 ltac2_type1 SEP "*"      (* Ltac2 plugin *)
+| ltac2_type1      (* Ltac2 plugin *)
+]
+
+ltac2_type1: [
+| ltac2_type0 qualid      (* Ltac2 plugin *)
+| ltac2_type0      (* Ltac2 plugin *)
+]
+
+ltac2_type0: [
+| "(" LIST1 ltac2_type SEP "," ")" OPT qualid      (* Ltac2 plugin *)
+| ltac2_typevar      (* Ltac2 plugin *)
+| "_"      (* Ltac2 plugin *)
+| qualid      (* Ltac2 plugin *)
+]
+
+ltac2_typevar: [
+| "'" ident      (* Ltac2 plugin *)
+]
+
+lident: [
+| ident      (* Ltac2 plugin *)
+]
+
+destruction_arg: [
+| num
+| constr_with_bindings
+| constr_with_bindings_arg
+]
+
+constr_with_bindings_arg: [
+| ">" constr_with_bindings
+| constr_with_bindings
+]
+
+clause_dft_concl: [
+| "in" in_clause
+| OPT ( "at" occs_nums )
+]
+
+in_clause: [
+| "*" OPT ( "at" occs_nums )
+| "*" "|-" OPT concl_occ
+| LIST0 hypident_occ SEP "," OPT ( "|-" OPT concl_occ )
+]
+
+hypident_occ: [
+| hypident OPT ( "at" occs_nums )
+]
+
+hypident: [
+| ident
+| "(" "type" "of" ident ")"
+| "(" "value" "of" ident ")"
+]
+
+concl_occ: [
+| "*" OPT ( "at" occs_nums )
+]
+
+q_intropatterns: [
+| ltac2_intropatterns      (* Ltac2 plugin *)
+]
+
+ltac2_intropatterns: [
+| LIST0 nonsimple_intropattern      (* Ltac2 plugin *)
+]
+
+nonsimple_intropattern: [
+| "*"      (* Ltac2 plugin *)
+| "**"      (* Ltac2 plugin *)
+| ltac2_simple_intropattern      (* Ltac2 plugin *)
+]
+
+q_intropattern: [
+| ltac2_simple_intropattern      (* Ltac2 plugin *)
+]
+
+ltac2_simple_intropattern: [
+| ltac2_naming_intropattern      (* Ltac2 plugin *)
+| "_"      (* Ltac2 plugin *)
+| ltac2_or_and_intropattern      (* Ltac2 plugin *)
+| ltac2_equality_intropattern      (* Ltac2 plugin *)
+]
+
+ltac2_or_and_intropattern: [
+| "[" LIST1 ltac2_intropatterns SEP "|" "]"      (* Ltac2 plugin *)
+| "()"      (* Ltac2 plugin *)
+| "(" LIST1 ltac2_simple_intropattern SEP "," ")"      (* Ltac2 plugin *)
+| "(" LIST1 ltac2_simple_intropattern SEP "&" ")"      (* Ltac2 plugin *)
+]
+
+ltac2_equality_intropattern: [
+| "->"      (* Ltac2 plugin *)
+| "<-"      (* Ltac2 plugin *)
+| "[=" ltac2_intropatterns "]"      (* Ltac2 plugin *)
+]
+
+ltac2_naming_intropattern: [
+| "?" lident      (* Ltac2 plugin *)
+| "?$" lident      (* Ltac2 plugin *)
+| "?"      (* Ltac2 plugin *)
+| ident_or_anti      (* Ltac2 plugin *)
+]
+
+q_ident: [
+| ident_or_anti      (* Ltac2 plugin *)
+]
+
+ident_or_anti: [
+| lident      (* Ltac2 plugin *)
+| "$" ident      (* Ltac2 plugin *)
+]
+
+q_destruction_arg: [
+| ltac2_destruction_arg      (* Ltac2 plugin *)
+]
+
+ltac2_destruction_arg: [
+| num      (* Ltac2 plugin *)
+| lident      (* Ltac2 plugin *)
+| ltac2_constr_with_bindings      (* Ltac2 plugin *)
+]
+
+ltac2_constr_with_bindings: [
+| term OPT ( "with" ltac2_bindings )      (* Ltac2 plugin *)
+]
+
+q_bindings: [
+| ltac2_bindings      (* Ltac2 plugin *)
+]
+
+q_with_bindings: [
+| OPT ( "with" ltac2_bindings )      (* Ltac2 plugin *)
+]
+
+ltac2_bindings: [
+| LIST1 ltac2_simple_binding      (* Ltac2 plugin *)
+| LIST1 term      (* Ltac2 plugin *)
+]
+
+ltac2_simple_binding: [
+| "(" qhyp ":=" term ")"      (* Ltac2 plugin *)
+]
+
+qhyp: [
+| "$" ident      (* Ltac2 plugin *)
+| num      (* Ltac2 plugin *)
+| lident      (* Ltac2 plugin *)
+]
+
 int_or_id: [
-| ident      (* extraction plugin *)
+| ident
 | int      (* extraction plugin *)
 ]
 
@@ -1151,7 +1360,7 @@ decl_notations: [
 ]
 
 decl_notation: [
-| string ":=" one_term OPT ( "(" "only" "parsing" ")" ) OPT [ ":" scope_name ]
+| string ":=" one_term OPT ( "(" LIST1 syntax_modifier SEP "," ")" ) OPT [ ":" scope_name ]
 ]
 
 simple_tactic: [
@@ -1210,6 +1419,7 @@ simple_tactic: [
 | "solve" "[" LIST0 ltac_expr SEP "|" "]"
 | "idtac" LIST0 [ ident | string | int ]
 | [ "fail" | "gfail" ] OPT int_or_var LIST0 [ ident | string | int ]
+| "fun" LIST1 name "=>" ltac_expr
 | "eval" red_expr "in" term
 | "context" ident "[" term "]"
 | "type" "of" term
@@ -1219,13 +1429,14 @@ simple_tactic: [
 | "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
+| ltac2_match_key ltac2_expr "with" ltac2_match_list "end"
+| ltac2_match_key OPT "reverse" "goal" "with" goal_match_list "end"
 | "simplify_eq" OPT destruction_arg
 | "esimplify_eq" OPT destruction_arg
 | "discriminate" OPT destruction_arg
@@ -1329,10 +1540,10 @@ simple_tactic: [
 | "setoid_reflexivity"
 | "setoid_transitivity" one_term
 | "setoid_etransitivity"
-| "decide" "equality"
-| "compare" one_term one_term
 | "intros" LIST0 intropattern
 | "eintros" LIST0 intropattern
+| "decide" "equality"
+| "compare" one_term one_term
 | "apply" LIST1 constr_with_bindings_arg SEP "," OPT in_hyp_as
 | "eapply" LIST1 constr_with_bindings_arg SEP "," OPT in_hyp_as
 | "simple" "apply" LIST1 constr_with_bindings_arg SEP "," OPT in_hyp_as
@@ -1453,6 +1664,7 @@ simple_tactic: [
 | "psatz" term OPT int_or_var
 | "ring" OPT ( "[" LIST1 term "]" )
 | "ring_simplify" OPT ( "[" LIST1 term "]" ) LIST1 term OPT ( "in" ident )
+| "match" ltac2_expr5 "with" OPT ltac2_branches "end"
 | qualid LIST1 tactic_arg
 ]
 
@@ -1465,26 +1677,6 @@ hloc: [
 | "in" "(" "value" "of" ident ")"
 ]
 
-in_clause: [
-| LIST0 hypident_occ SEP "," OPT ( "|-" OPT concl_occ )
-| "*" "|-" OPT concl_occ
-| "*" OPT ( "at" occs_nums )
-]
-
-concl_occ: [
-| "*" OPT ( "at" occs_nums )
-]
-
-hypident_occ: [
-| hypident OPT ( "at" occs_nums )
-]
-
-hypident: [
-| ident
-| "(" "type" "of" ident ")"
-| "(" "value" "of" ident ")"
-]
-
 as_ipat: [
 | "as" simple_intropattern
 ]
@@ -1507,12 +1699,7 @@ as_name: [
 ]
 
 rewriter: [
-| "!" constr_with_bindings_arg
-| "?" constr_with_bindings_arg
-| num "!" constr_with_bindings_arg
-| num [ "?" | "?" ] constr_with_bindings_arg
-| num constr_with_bindings_arg
-| constr_with_bindings_arg
+| OPT num OPT [ "?" | "!" ] constr_with_bindings_arg
 ]
 
 oriented_rewriter: [
@@ -1554,9 +1741,9 @@ naming_intropattern: [
 ]
 
 intropattern: [
-| simple_intropattern
 | "*"
 | "**"
+| simple_intropattern
 ]
 
 simple_intropattern: [
@@ -1597,9 +1784,367 @@ bindings_with_parameters: [
 | "(" ident LIST0 simple_binder ":=" term ")"
 ]
 
-clause_dft_concl: [
-| "in" in_clause
-| OPT ( "at" occs_nums )
+q_clause: [
+| ltac2_clause      (* Ltac2 plugin *)
+]
+
+ltac2_clause: [
+| "in" ltac2_in_clause      (* Ltac2 plugin *)
+| "at" ltac2_occs_nums      (* Ltac2 plugin *)
+]
+
+ltac2_in_clause: [
+| "*" OPT ltac2_occs      (* Ltac2 plugin *)
+| "*" "|-" OPT ltac2_concl_occ      (* Ltac2 plugin *)
+| LIST0 ltac2_hypident_occ SEP "," OPT ( "|-" OPT ltac2_concl_occ )      (* Ltac2 plugin *)
+]
+
+q_occurrences: [
+| OPT ltac2_occs      (* Ltac2 plugin *)
+]
+
+ltac2_occs: [
+| "at" ltac2_occs_nums      (* Ltac2 plugin *)
+]
+
+ltac2_occs_nums: [
+| OPT "-" LIST1 [ num      (* Ltac2 plugin *) | "$" ident ]      (* Ltac2 plugin *)
+]
+
+ltac2_concl_occ: [
+| "*" OPT ltac2_occs      (* Ltac2 plugin *)
+]
+
+ltac2_hypident_occ: [
+| ltac2_hypident OPT ltac2_occs      (* Ltac2 plugin *)
+]
+
+ltac2_hypident: [
+| ident_or_anti      (* Ltac2 plugin *)
+| "(" "type" "of" ident_or_anti ")"      (* Ltac2 plugin *)
+| "(" "value" "of" ident_or_anti ")"      (* Ltac2 plugin *)
+]
+
+q_induction_clause: [
+| ltac2_induction_clause      (* Ltac2 plugin *)
+]
+
+ltac2_induction_clause: [
+| ltac2_destruction_arg OPT ltac2_as_or_and_ipat OPT ltac2_eqn_ipat OPT ltac2_clause      (* Ltac2 plugin *)
+]
+
+ltac2_as_or_and_ipat: [
+| "as" ltac2_or_and_intropattern      (* Ltac2 plugin *)
+]
+
+ltac2_eqn_ipat: [
+| "eqn" ":" ltac2_naming_intropattern      (* Ltac2 plugin *)
+]
+
+q_conversion: [
+| ltac2_conversion      (* Ltac2 plugin *)
+]
+
+ltac2_conversion: [
+| term      (* Ltac2 plugin *)
+| term "with" term      (* Ltac2 plugin *)
+]
+
+q_rewriting: [
+| ltac2_oriented_rewriter      (* Ltac2 plugin *)
+]
+
+ltac2_oriented_rewriter: [
+| [ "->" | "<-" ] ltac2_rewriter      (* Ltac2 plugin *)
+]
+
+ltac2_rewriter: [
+| OPT num OPT [ "?" | "!" ] ltac2_constr_with_bindings
+]
+
+q_dispatch: [
+| ltac2_for_each_goal      (* Ltac2 plugin *)
+]
+
+ltac2_for_each_goal: [
+| ltac2_goal_tactics      (* Ltac2 plugin *)
+| OPT ( ltac2_goal_tactics "|" ) OPT ltac2_expr ".." OPT ( "|" ltac2_goal_tactics )      (* Ltac2 plugin *)
+]
+
+ltac2_goal_tactics: [
+| LIST0 ( OPT ltac2_expr ) SEP "|"      (* Ltac2 plugin *)
+]
+
+q_strategy_flag: [
+| ltac2_strategy_flag      (* Ltac2 plugin *)
+]
+
+ltac2_strategy_flag: [
+| LIST1 ltac2_red_flag      (* Ltac2 plugin *)
+| OPT ltac2_delta_flag      (* Ltac2 plugin *)
+]
+
+ltac2_red_flag: [
+| "beta"      (* Ltac2 plugin *)
+| "iota"      (* Ltac2 plugin *)
+| "match"      (* Ltac2 plugin *)
+| "fix"      (* Ltac2 plugin *)
+| "cofix"      (* Ltac2 plugin *)
+| "zeta"      (* Ltac2 plugin *)
+| "delta" OPT ltac2_delta_flag      (* Ltac2 plugin *)
+]
+
+ltac2_delta_flag: [
+| OPT "-" "[" LIST1 refglobal "]"
+]
+
+q_reference: [
+| refglobal      (* Ltac2 plugin *)
+]
+
+refglobal: [
+| "&" ident      (* Ltac2 plugin *)
+| qualid      (* Ltac2 plugin *)
+| "$" ident      (* Ltac2 plugin *)
+]
+
+q_hintdb: [
+| hintdb      (* Ltac2 plugin *)
+]
+
+hintdb: [
+| "*"      (* Ltac2 plugin *)
+| LIST1 ident_or_anti      (* Ltac2 plugin *)
+]
+
+q_constr_matching: [
+| ltac2_match_list      (* Ltac2 plugin *)
+]
+
+ltac2_match_key: [
+| "lazy_match!"
+| "match!"
+| "multi_match!"
+]
+
+ltac2_match_list: [
+| OPT "|" LIST1 ltac2_match_rule SEP "|"
+]
+
+ltac2_match_rule: [
+| ltac2_match_pattern "=>" ltac2_expr      (* Ltac2 plugin *)
+]
+
+ltac2_match_pattern: [
+| cpattern      (* Ltac2 plugin *)
+| "context" OPT ident "[" cpattern "]"      (* Ltac2 plugin *)
+]
+
+q_goal_matching: [
+| goal_match_list      (* Ltac2 plugin *)
+]
+
+goal_match_list: [
+| OPT "|" LIST1 gmatch_rule SEP "|"
+]
+
+gmatch_rule: [
+| gmatch_pattern "=>" ltac2_expr      (* Ltac2 plugin *)
+]
+
+gmatch_pattern: [
+| "[" LIST0 gmatch_hyp_pattern SEP "," "|-" ltac2_match_pattern "]"      (* Ltac2 plugin *)
+]
+
+gmatch_hyp_pattern: [
+| name ":" ltac2_match_pattern      (* Ltac2 plugin *)
+]
+
+q_move_location: [
+| move_location      (* Ltac2 plugin *)
+]
+
+move_location: [
+| "at" "top"      (* Ltac2 plugin *)
+| "at" "bottom"      (* Ltac2 plugin *)
+| "after" ident_or_anti      (* Ltac2 plugin *)
+| "before" ident_or_anti      (* Ltac2 plugin *)
+]
+
+q_pose: [
+| pose      (* Ltac2 plugin *)
+]
+
+pose: [
+| "(" ident_or_anti ":=" term ")"      (* Ltac2 plugin *)
+| term OPT ltac2_as_name      (* Ltac2 plugin *)
+]
+
+ltac2_as_name: [
+| "as" ident_or_anti      (* Ltac2 plugin *)
+]
+
+q_assert: [
+| assertion      (* Ltac2 plugin *)
+]
+
+assertion: [
+| "(" ident_or_anti ":=" term ")"      (* Ltac2 plugin *)
+| "(" ident_or_anti ":" term ")" OPT ltac2_by_tactic      (* Ltac2 plugin *)
+| term OPT ltac2_as_ipat OPT ltac2_by_tactic      (* Ltac2 plugin *)
+]
+
+ltac2_as_ipat: [
+| "as" ltac2_simple_intropattern      (* Ltac2 plugin *)
+]
+
+ltac2_by_tactic: [
+| "by" ltac2_expr      (* Ltac2 plugin *)
+]
+
+ltac2_entry: [
+]
+
+tac2def_body: [
+| [ "_" | ident ] LIST0 tac2pat0 ":=" ltac2_expr      (* Ltac2 plugin *)
+]
+
+tac2typ_def: [
+| OPT tac2typ_prm qualid OPT ( [ ":=" | "::=" ] tac2typ_knd )      (* Ltac2 plugin *)
+]
+
+tac2typ_prm: [
+| ltac2_typevar      (* Ltac2 plugin *)
+| "(" LIST1 ltac2_typevar SEP "," ")"      (* Ltac2 plugin *)
+]
+
+tac2typ_knd: [
+| ltac2_type      (* Ltac2 plugin *)
+| "[" OPT ( OPT "|" LIST1 tac2alg_constructor SEP "|" ) "]"      (* Ltac2 plugin *)
+| "[" ".." "]"      (* Ltac2 plugin *)
+| "{" OPT ( LIST1 tac2rec_field SEP ";" OPT ";" ) "}"      (* Ltac2 plugin *)
+]
+
+tac2alg_constructor: [
+| ident      (* Ltac2 plugin *)
+| ident "(" LIST0 ltac2_type SEP "," ")"      (* Ltac2 plugin *)
+]
+
+tac2rec_field: [
+| OPT "mutable" ident ":" ltac2_type      (* Ltac2 plugin *)
+]
+
+ltac2_scope: [
+| string      (* Ltac2 plugin *)
+| int      (* Ltac2 plugin *)
+| name      (* Ltac2 plugin *)
+| name "(" LIST1 ltac2_scope SEP "," ")"      (* Ltac2 plugin *)
+]
+
+ltac2_expr: [
+| ltac2_expr5 ";" ltac2_expr      (* Ltac2 plugin *)
+| ltac2_expr5      (* Ltac2 plugin *)
+]
+
+ltac2_expr5: [
+| "fun" LIST1 tac2pat0 "=>" ltac2_expr      (* Ltac2 plugin *)
+| "let" OPT "rec" ltac2_let_clause LIST0 ( "with" ltac2_let_clause ) "in" ltac2_expr      (* Ltac2 plugin *)
+| ltac2_expr3      (* Ltac2 plugin *)
+]
+
+ltac2_let_clause: [
+| LIST1 tac2pat0 ":=" ltac2_expr      (* Ltac2 plugin *)
+]
+
+ltac2_expr3: [
+| LIST1 ltac2_expr2 SEP ","      (* Ltac2 plugin *)
+]
+
+ltac2_expr2: [
+| ltac2_expr1 "::" ltac2_expr2      (* Ltac2 plugin *)
+| ltac2_expr1      (* Ltac2 plugin *)
+]
+
+ltac2_expr1: [
+| ltac2_expr0 LIST1 ltac2_expr0      (* Ltac2 plugin *)
+| ltac2_expr0 ".(" qualid ")"      (* Ltac2 plugin *)
+| ltac2_expr0 ".(" qualid ")" ":=" ltac2_expr5      (* Ltac2 plugin *)
+| ltac2_expr0      (* Ltac2 plugin *)
+]
+
+tac2rec_fieldexpr: [
+| qualid ":=" ltac2_expr1      (* Ltac2 plugin *)
+]
+
+ltac2_expr0: [
+| "(" ltac2_expr ")"      (* Ltac2 plugin *)
+| "(" ltac2_expr ":" ltac2_type ")"      (* Ltac2 plugin *)
+| "()"      (* Ltac2 plugin *)
+| "[" LIST0 ltac2_expr5 SEP ";" "]"      (* Ltac2 plugin *)
+| "{" OPT ( LIST1 tac2rec_fieldexpr OPT ";" ) "}"      (* Ltac2 plugin *)
+| ltac2_tactic_atom      (* Ltac2 plugin *)
+]
+
+ltac2_tactic_atom: [
+| int      (* Ltac2 plugin *)
+| string      (* Ltac2 plugin *)
+| qualid      (* Ltac2 plugin *)
+| "@" ident      (* Ltac2 plugin *)
+| "&" lident      (* Ltac2 plugin *)
+| "'" term      (* Ltac2 plugin *)
+| ltac2_quotations
+]
+
+ltac2_quotations: [
+| "ident" ":" "(" lident ")"
+| "constr" ":" "(" term ")"
+| "open_constr" ":" "(" term ")"
+| "pattern" ":" "(" cpattern ")"
+| "reference" ":" "(" [ "&" ident | qualid ] ")"
+| "ltac1" ":" "(" ltac1_expr_in_env ")"
+| "ltac1val" ":" "(" ltac1_expr_in_env ")"
+]
+
+ltac1_expr_in_env: [
+| ltac_expr      (* Ltac2 plugin *)
+| LIST0 ident "|-" ltac_expr      (* Ltac2 plugin *)
+]
+
+ltac2_branches: [
+| OPT "|" LIST1 ( tac2pat1 "=>" ltac2_expr ) SEP "|"
+]
+
+tac2pat1: [
+| qualid LIST1 tac2pat0      (* Ltac2 plugin *)
+| qualid      (* Ltac2 plugin *)
+| "[" "]"      (* Ltac2 plugin *)
+| tac2pat0 "::" tac2pat0      (* Ltac2 plugin *)
+| tac2pat0      (* Ltac2 plugin *)
+]
+
+tac2pat0: [
+| "_"      (* Ltac2 plugin *)
+| "()"      (* Ltac2 plugin *)
+| qualid      (* Ltac2 plugin *)
+| "(" OPT atomic_tac2pat ")"      (* Ltac2 plugin *)
+]
+
+atomic_tac2pat: [
+| tac2pat1 ":" ltac2_type      (* Ltac2 plugin *)
+| tac2pat1 "," LIST0 tac2pat1 SEP ","      (* Ltac2 plugin *)
+| tac2pat1      (* Ltac2 plugin *)
+]
+
+tac2mode: [
+| ltac2_expr [ "." | "..." ]      (* Ltac2 plugin *)
+| "Eval" red_expr "in" term
+| "Compute" term
+| "Check" term
+| "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 )
+| "Search" LIST1 ( search_query ) OPT ( [ "inside" | "outside" ] LIST1 qualid )
 ]
 
 clause_dft_all: [
@@ -1636,17 +2181,6 @@ constr_with_bindings: [
 | one_term OPT ( "with" bindings )
 ]
 
-destruction_arg: [
-| num
-| constr_with_bindings
-| constr_with_bindings_arg
-]
-
-constr_with_bindings_arg: [
-| ">" constr_with_bindings
-| constr_with_bindings
-]
-
 conversion: [
 | one_term
 | one_term "with" one_term