Convert Gallina Vernac to use prodn

24 files changed, 1263 insertions, 986 deletions

diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index a34b2d5195..89b4bda71a 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -34,14 +34,14 @@ Names (link targets) are auto-generated for most simple objects, though they can
 
 Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms).  Undocumented objects should have the ``:undocumented:`` flag instead, as shown above.  When multiple objects have a single description, they can be grouped into a single object, like this (semicolons can be used to separate the names of the objects; names starting with ``_`` will be omitted from the indexes)::
 
-   .. cmdv:: Lemma @ident {? @binders} : @type
-             Remark @ident {? @binders} : @type
-             Fact @ident {? @binders} : @type
-             Corollary @ident {? @binders} : @type
-             Proposition @ident {? @binders} : @type
+   .. cmdv:: Lemma @ident {* @binder } : @type
+             Remark @ident {* @binder } : @type
+             Fact @ident {* @binder } : @type
+             Corollary @ident {* @binder } : @type
+             Proposition @ident {* @binder } : @type
       :name: Lemma; Remark; Fact; Corollary; Proposition
 
-      These commands are all synonyms of :n:`Theorem @ident {? @binders } : type`.
+      These commands are all synonyms of :n:`Theorem @ident {* @binder } : type`.
 
 Notations
 ---------
@@ -89,10 +89,15 @@ Objects
 
 Here is the list of all objects of the Coq domain (The symbol :black_nib: indicates an object whose signature can be written using the notations DSL):
 
+``.. attr::`` :black_nib: An attribute.
+    Example::
+
+       .. attr:: local
+
 ``.. cmd::`` :black_nib: A Coq command.
     Example::
 
-       .. cmd:: Infix "@symbol" := @term ({+, @modifier}).
+       .. cmd:: Infix @string := @term1_extended {? ( {+, @syntax_modifier } ) } {? : @ident }
 
           This command is equivalent to :n:`…`.
 
diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst
index 51d5174567..c5e0007e78 100644
--- a/doc/sphinx/README.template.rst
+++ b/doc/sphinx/README.template.rst
@@ -34,14 +34,14 @@ Names (link targets) are auto-generated for most simple objects, though they can
 
 Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms).  Undocumented objects should have the ``:undocumented:`` flag instead, as shown above.  When multiple objects have a single description, they can be grouped into a single object, like this (semicolons can be used to separate the names of the objects; names starting with ``_`` will be omitted from the indexes)::
 
-   .. cmdv:: Lemma @ident {? @binders} : @type
-             Remark @ident {? @binders} : @type
-             Fact @ident {? @binders} : @type
-             Corollary @ident {? @binders} : @type
-             Proposition @ident {? @binders} : @type
+   .. cmdv:: Lemma @ident {* @binder } : @type
+             Remark @ident {* @binder } : @type
+             Fact @ident {* @binder } : @type
+             Corollary @ident {* @binder } : @type
+             Proposition @ident {* @binder } : @type
       :name: Lemma; Remark; Fact; Corollary; Proposition
 
-      These commands are all synonyms of :n:`Theorem @ident {? @binders } : type`.
+      These commands are all synonyms of :n:`Theorem @ident {* @binder } : type`.
 
 Notations
 ---------
diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index 9f5741f72a..94ab6e789c 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -170,7 +170,7 @@ compatibility constraints.
 Adding new relations and morphisms
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmd::  Add Parametric Relation @binders : (A t1 ... tn) (Aeq t′1 ... t′m) {? reflexivity proved by @term} {? symmetry proved by @term} {? transitivity proved by @term} as @ident
+.. cmd::  Add Parametric Relation {* @binder } : (A t1 ... tn) (Aeq t′1 ... t′m) {? reflexivity proved by @term} {? symmetry proved by @term} {? transitivity proved by @term} as @ident
 
    This command declares a parametric relation :g:`Aeq: forall (y1 : β1 ... ym : βm)`,
    :g:`relation (A t1 ... tn)` over :g:`(A : αi -> ... αn -> Type)`.
@@ -219,7 +219,7 @@ replace terms with related ones only in contexts that are syntactic
 compositions of parametric morphism instances declared with the
 following command.
 
-.. cmd:: Add Parametric Morphism @binders : (@ident {+ @term__1}) with signature @term__2 as @ident
+.. cmd:: Add Parametric Morphism {* @binder } : (@ident {+ @term__1}) with signature @term__2 as @ident
 
    This command declares a parametric morphism :n:`@ident {+ @term__1}` of
    signature :n:`@term__2`.  The final identifier :token:`ident` gives a unique
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index 19b33f0d90..b007509b2e 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -198,7 +198,7 @@ Figure :ref:`vernacular` as follows:
    \comindex{Hypothesis \mbox{\rm (and coercions)}}
 
 .. productionlist::
-   assumption : `assumption_keyword` `assums` .
+   assumption : `assumption_token` `assums` .
    assums : `simple_assums`
           : (`simple_assums`) ... (`simple_assums`)
    simple_assums : `ident` ... `ident` :[>] `term`
@@ -215,12 +215,6 @@ grammar of inductive types from Figure :ref:`vernacular` as follows:
    \comindex{Inductive \mbox{\rm (and coercions)}}
    \comindex{CoInductive \mbox{\rm (and coercions)}}
 
-.. productionlist::
-   inductive : Inductive `ind_body` with ... with `ind_body`
-             : CoInductive `ind_body` with ... with `ind_body`
-   ind_body : `ident` [ `binders` ] : `term` := [[|] `constructor` | ... | `constructor` ]
-   constructor : `ident` [ `binders` ] [:[>] `term` ]
-
 Especially, if the extra ``>`` is present in a constructor
 declaration, this constructor is declared as a coercion.
 
@@ -240,7 +234,7 @@ declaration, this constructor is declared as a coercion.
 
       Same as :cmd:`Identity Coercion` but locally to the current section.
 
-   .. cmdv:: SubClass @ident := @type
+   .. cmd:: SubClass @ident_decl @def_body
       :name: SubClass
 
       If :n:`@type` is a class :n:`@ident'` applied to some arguments then
@@ -251,7 +245,7 @@ declaration, this constructor is declared as a coercion.
       :n:`Definition @ident := @type.`
       :n:`Identity Coercion Id_@ident_@ident' : @ident >-> @ident'`.
 
-   .. cmdv:: Local SubClass @ident := @type
+   .. cmdv:: Local SubClass @ident_decl @def_body
 
       Same as before but locally to the current section.
 
@@ -299,7 +293,7 @@ Classes as Records
 We allow the definition of *Structures with Inheritance* (or classes as records)
 by extending the existing :cmd:`Record` macro. Its new syntax is:
 
-.. cmdv:: Record {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } }
+.. cmdv:: {| Record | Structure } {? >} @ident {* @binder } : @sort := {? @ident} { {+; @ident :{? >} @term } }
 
    The first identifier :token:`ident` is the name of the defined record and
    :token:`sort` is its type. The optional identifier after ``:=`` is the name
@@ -315,12 +309,6 @@ by extending the existing :cmd:`Record` macro. Its new syntax is:
    (this may fail if the uniform inheritance condition is not
    satisfied).
 
-.. cmdv:: Structure {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } }
-   :name: Structure
-
-   This is a synonym of :cmd:`Record`.
-
-
 Coercions and Sections
 ----------------------
 
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index a17dca1693..549249d25c 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -174,7 +174,7 @@ Program Definition
       .. exn:: In environment … the term: @term does not have type @type. Actually, it has type ...
          :undocumented:
 
-   .. cmdv:: Program Definition @ident @binders : @type := @term
+   .. cmdv:: Program Definition @ident {* @binder } : @type := @term
 
       This is equivalent to:
 
@@ -189,7 +189,7 @@ Program Definition
 Program Fixpoint
 ~~~~~~~~~~~~~~~~
 
-.. cmd:: Program Fixpoint @ident @binders {? {@order}} : @type := @term
+.. cmd:: Program Fixpoint @ident {* @binder } {? {@order}} : @type := @term
 
    The optional order annotation follows the grammar:
 
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 57a2254100..af4e9051bb 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -295,14 +295,18 @@ the Existing Instance command to achieve the same effect.
 Summary of the commands
 -----------------------
 
-.. cmd:: Class @ident {? @binders} : {? @sort} := {? @ident} { {+; @ident :{? >} @term } }
+.. cmd:: Class @inductive_definition {* with @inductive_definition }
 
    The :cmd:`Class` command is used to declare a typeclass with parameters
    :token:`binders` and fields the declared record fields.
 
+   This command supports the :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`,
+   :attr:`universes(template)`, :attr:`universes(notemplate)`,
+   :attr:`Cumulative`, :attr:`NonCumulative` and :attr:`Private` attributes.
+
    .. _singleton-class:
 
-   .. cmdv:: Class @ident {? @binders} : {? @sort} := @ident : @term
+   .. cmdv:: Class @ident {* @binder } : {? @sort} := @ident : @term
 
       This variant declares a *singleton* class with a single method.  This
       singleton class is a so-called definitional class, represented simply
@@ -324,7 +328,7 @@ Summary of the commands
 
          This command has no effect when used on a typeclass.
 
-.. cmd:: Instance @ident {? @binders} : @term__0 {+ @term} {? | @num} := { {*; @field_def} }
+.. cmd:: Instance @ident {* @binder } : @term__0 {+ @term} {? | @num} := { {*; @field_def} }
 
    This command is used to declare a typeclass instance named
    :token:`ident` of the class :n:`@term__0` with parameters :token:`term` and
@@ -337,10 +341,10 @@ Summary of the commands
    :tacn:`auto` hints. If the priority :token:`num` is not specified, it defaults to the number
    of non-dependent binders of the instance.
 
-   .. cmdv:: Instance @ident {? @binders} : forall {? @binders}, @term__0 {+ @term} {? | @num } := @term
+   .. cmdv:: Instance @ident {* @binder } : forall {* @binder }, @term__0 {+ @term} {? | @num } := @term
 
       This syntax is used for declaration of singleton class instances or
-      for directly giving an explicit term of type :n:`forall @binders, @term__0
+      for directly giving an explicit term of type :n:`forall {* @binder }, @term__0
       {+ @term}`.  One need not even mention the unique field name for
       singleton classes.
 
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index f9cc25959c..c069782add 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -152,6 +152,8 @@ Many other commands support the ``Polymorphic`` flag, including:
 - :cmd:`Hint Resolve` and :cmd:`Hint Rewrite` will use the auto/rewrite hint
   polymorphically, not at a single instance.
 
+.. _cumulative:
+
 Cumulative, NonCumulative
 -------------------------
 
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index 77cb3ecc21..22102aa3ab 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -183,16 +183,21 @@ todo_include_todos = False
 nitpicky = True
 
 nitpick_ignore = [ ('token', token) for token in [
+    'binders',
     'collection',
     'command',
+    'definition',
     'dirpath',
+    'inductive',
+    'ind_body',
     'modpath',
     'module',
-    'red_expr',
+    'simple_tactic',
     'symbol',
     'tactic',
     'term_pattern',
     'term_pattern_string',
+    'toplevel_selector',
 ]]
 
 # -- Options for HTML output ----------------------------------------------
diff --git a/doc/sphinx/coq-cmdindex.rst b/doc/sphinx/coq-cmdindex.rst
index fd0b342ae4..18d2e379ac 100644
--- a/doc/sphinx/coq-cmdindex.rst
+++ b/doc/sphinx/coq-cmdindex.rst
@@ -2,6 +2,8 @@
 
 .. hack to get index in TOC
 
+.. _command_index:
+
 -----------------
 Command index
 -----------------
diff --git a/doc/sphinx/coq-tacindex.rst b/doc/sphinx/coq-tacindex.rst
index 31b2f7f8cb..cddcdf83e8 100644
--- a/doc/sphinx/coq-tacindex.rst
+++ b/doc/sphinx/coq-tacindex.rst
@@ -2,6 +2,8 @@
 
 .. hack to get index in TOC
 
+.. _tactic_index:
+
 -------------
 Tactic index
 -------------
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 9686500a35..6c1d83b3b8 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -27,19 +27,26 @@ expressions. In this sense, the :cmd:`Record` construction allows defining
      field          : `ident` [ `binders` ] : `type` [ where `notation` ]
                     : `ident` [ `binders` ] [: `type` ] := `term`
 
-.. cmd:: Record @ident @binders {? : @sort} := {? @ident} { {*; @ident @binders : @type } }
+.. cmd:: {| Record | Structure } @inductive_definition {* with @inductive_definition }
+   :name: Record; Structure
 
    The first identifier :token:`ident` is the name of the defined record and :token:`sort` is its
    type. The optional identifier following ``:=`` is the name of its constructor. If it is omitted,
    the default name :n:`Build_@ident`, where :token:`ident` is the record name, is used. If :token:`sort` is
    omitted, the default sort is :math:`\Type`. The identifiers inside the brackets are the names of
-   fields. For a given field :token:`ident`, its type is :n:`forall @binders, @type`.
+   fields. For a given field :token:`ident`, its type is :n:`forall {* @binder }, @type`.
    Remark that the type of a particular identifier may depend on a previously-given identifier. Thus the
    order of the fields is important. Finally, :token:`binders` are parameters of the record.
 
+   :cmd:`Record` and :cmd:`Structure` are synonyms.
+
+   This command supports the :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`,
+   :attr:`universes(template)`, :attr:`universes(notemplate)`,
+   :attr:`Cumulative`, :attr:`NonCumulative` and :attr:`Private` attributes.
+
 More generally, a record may have explicitly defined (a.k.a. manifest)
 fields. For instance, we might have:
-:n:`Record @ident @binders : @sort := { @ident__1 : @type__1 ; @ident__2 := @term__2 ; @ident__3 : @type__3 }`.
+:n:`Record @ident {* @binder } : @sort := { @ident__1 : @type__1 ; @ident__2 := @term__2 ; @ident__3 : @type__3 }`.
 in which case the correctness of :n:`@type__3` may rely on the instance :n:`@term__2` of :n:`@ident__2` and :n:`@term__2` may in turn depend on :n:`@ident__1`.
 
 .. example::
@@ -62,7 +69,7 @@ in which case the correctness of :n:`@type__3` may rely on the instance :n:`@ter
 
 Let us now see the work done by the ``Record`` macro. First the macro
 generates a variant type definition with just one constructor:
-:n:`Variant @ident {? @binders } : @sort := @ident__0 {? @binders }`.
+:n:`Variant @ident {* @binder } : @sort := @ident__0 {* @binder }`.
 
 To build an object of type :token:`ident`, one should provide the constructor
 :n:`@ident__0` with the appropriate number of terms filling the fields of the record.
@@ -183,8 +190,6 @@ other arguments are the parameters of the inductive type.
    defined with the ``Record`` keyword can be activated with the
    :flag:`Nonrecursive Elimination Schemes` flag (see :ref:`proofschemes-induction-principles`).
 
-.. note:: ``Structure`` is a synonym of the keyword ``Record``.
-
 .. warn:: @ident cannot be defined.
 
   It can happen that the definition of a projection is impossible.
@@ -696,7 +701,7 @@ used by ``Function``. A more precise description is given below.
 
 .. cmdv:: Function @ident {* @binder } : @type := @term
 
-   Defines the not recursive function :token:`ident` as if declared with
+   Defines the nonrecursive function :token:`ident` as if it was declared with
    :cmd:`Definition`. Moreover the following are defined:
 
     + :token:`ident`\ ``_rect``, :token:`ident`\ ``_rec`` and :token:`ident`\ ``_ind``,
@@ -817,32 +822,6 @@ Sections create local contexts which can be shared across multiple definitions.
    Most commands, like :cmd:`Hint`, :cmd:`Notation`, option management, … which
    appear inside a section are canceled when the section is closed.
 
-.. cmd:: Variable @ident : @type
-
-   This command links :token:`type` to the name :token:`ident` in the context of
-   the current section. When the current section is closed, name :token:`ident`
-   will be unknown and every object using this variable will be explicitly
-   parameterized (the variable is *discharged*).
-
-   .. exn:: @ident already exists.
-      :name: @ident already exists. (Variable)
-      :undocumented:
-
-   .. cmdv:: Variable {+ @ident } : @type
-
-      Links :token:`type` to each :token:`ident`.
-
-   .. cmdv:: Variable {+ ( {+ @ident } : @type ) }
-
-      Declare one or more variables with various types.
-
-   .. cmdv:: Variables {+ ( {+ @ident } : @type) }
-             Hypothesis {+ ( {+ @ident } : @type) }
-             Hypotheses {+ ( {+ @ident } : @type) }
-      :name: Variables; Hypothesis; Hypotheses
-
-      These variants are synonyms of :n:`Variable {+ ( {+ @ident } : @type) }`.
-
 .. cmd:: Let @ident := @term
 
    This command binds the value :token:`term` to the name :token:`ident` in the
@@ -855,7 +834,7 @@ Sections create local contexts which can be shared across multiple definitions.
       :name: @ident already exists. (Let)
       :undocumented:
 
-   .. cmdv:: Let @ident {? @binders } {? : @type } := @term
+   .. cmdv:: Let @ident {* @binder } {? : @type } := @term
       :undocumented:
 
    .. cmdv:: Let Fixpoint @ident @fix_body {* with @fix_body}
@@ -866,7 +845,7 @@ Sections create local contexts which can be shared across multiple definitions.
       :name: Let CoFixpoint
       :undocumented:
 
-.. cmd:: Context @binders
+.. cmd:: Context {* @binder }
 
    Declare variables in the context of the current section, like :cmd:`Variable`,
    but also allowing implicit variables, :ref:`implicit-generalization`, and
@@ -1011,7 +990,7 @@ Reserved commands inside an interactive module type:
 
    This is a shortcut for the command :n:`Include @module` for each :token:`module`.
 
-.. cmd:: @assumption_keyword Inline @assums
+.. cmd:: @assumption_token Inline @assums
    :name: Inline
 
    The instance of this assumption will be automatically expanded at functor application, except when
@@ -1673,11 +1652,11 @@ The syntax is also supported in internal binders. For instance, in the
 following kinds of expressions, the type of each declaration present
 in :token:`binders` can be bracketed to mark the declaration as
 implicit:
-:n:`fun (@ident:forall @binders, @type) => @term`,
-:n:`forall (@ident:forall @binders, @type), @type`,
-:n:`let @ident @binders := @term in @term`,
-:n:`fix @ident @binders := @term in @term` and
-:n:`cofix @ident @binders := @term in @term`.
+:n:`fun (@ident:forall {* @binder }, @type) => @term`,
+:n:`forall (@ident:forall {* @binder }, @type), @type`,
+:n:`let @ident {* @binder } := @term in @term`,
+:n:`fix @ident {* @binder } := @term in @term` and
+:n:`cofix @ident {* @binder } := @term in @term`.
 Here is an example:
 
 .. coqtop:: all
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 7ce4538a4d..e12ff1ba98 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -49,11 +49,11 @@ Blanks
 
 Comments
   Comments are enclosed between ``(*`` and ``*)``.  They can be nested.
-  They can contain any character. However, embedded :token:`string` literals must be
+  They can contain any character. However, embedded :n:`@string` literals must be
   correctly closed. Comments are treated as blanks.
 
 Identifiers
-  Identifiers, written :token:`ident`, are sequences of letters, digits, ``_`` and
+  Identifiers, written :n:`@ident`, are sequences of letters, digits, ``_`` and
   ``'``, that do not start with a digit or ``'``.  That is, they are
   recognized by the following grammar (except that the string ``_`` is reserved;
   it is not a valid identifier):
@@ -74,8 +74,8 @@ Identifiers
 
 Numerals
   Numerals are sequences of digits with an optional fractional part
-  and exponent, optionally preceded by a minus sign. :token:`int` is an integer;
-  a numeral without fractional or exponent parts. :token:`num` is a non-negative
+  and exponent, optionally preceded by a minus sign. :n:`@int` is an integer;
+  a numeral without fractional or exponent parts. :n:`@num` is a non-negative
   integer.  Underscores embedded in the digits are ignored, for example
   ``1_000_000`` is the same as ``1000000``.
 
@@ -175,12 +175,19 @@ is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`.
    | ltac : ( @ltac_expr )
    field_def ::= @qualid {* @binder } := @term
 
+.. _types:
+
 Types
 -----
 
-Coq terms are typed. Coq types are recognized by the same syntactic
-class as :token:`term`. We denote by :production:`type` the semantic subclass
-of types inside the syntactic class :token:`term`.
+.. prodn::
+   type ::= @term
+
+:n:`@type`\s are a subset of :n:`@term`\s; not every :n:`@term` is a :n:`@type`.
+Every term has an associated type, which
+can be determined by applying the :ref:`typing-rules`.  Distinct terms
+may share the same type, for example 0 and 1 are both of type `nat`, the
+natural numbers.
 
 .. _gallina-identifiers:
 
@@ -193,14 +200,14 @@ Qualified identifiers and simple identifiers
    qualid ::= @ident {* @field_ident }
    field_ident ::= .@ident
 
-*Qualified identifiers* (:token:`qualid`) denote *global constants*
+*Qualified identifiers* (:n:`@qualid`) denote *global constants*
 (definitions, lemmas, theorems, remarks or facts), *global variables*
 (parameters or axioms), *inductive types* or *constructors of inductive
-types*. *Simple identifiers* (or shortly :token:`ident`) are a syntactic subset
+types*. *Simple identifiers* (or shortly :n:`@ident`) are a syntactic subset
 of qualified identifiers. Identifiers may also denote *local variables*,
 while qualified identifiers do not.
 
-Field identifiers, written :token:`field_ident`, are identifiers prefixed by
+Field identifiers, written :n:`@field_ident`, are identifiers prefixed by
 `.` (dot) with no blank between the dot and the identifier.
 
 
@@ -215,7 +222,7 @@ numbers (see :ref:`datatypes`).
 
 .. note::
 
-   Negative integers are not at the same level as :token:`num`, for this
+   Negative integers are not at the same level as :n:`@num`, for this
    would make precedence unnatural.
 
 .. index::
@@ -227,7 +234,7 @@ numbers (see :ref:`datatypes`).
 Sorts
 -----
 
-.. insertprodn sort univ_annot
+.. insertprodn sort univ_constraint
 
 .. prodn::
    sort ::= Set
@@ -242,12 +249,14 @@ Sorts
    universe_name ::= @qualid
    | Set
    | Prop
+   univ_annot ::= @%{ {* @universe_level } %}
    universe_level ::= Set
    | Prop
    | Type
    | _
    | @qualid
-   univ_annot ::= @%{ {* @universe_level } %}
+   univ_decl ::= @%{ {* @ident } {? + } {? %| {*, @univ_constraint } {? + } } %}
+   univ_constraint ::= @universe_name {| < | = | <= } @universe_name
 
 There are four sorts :g:`SProp`, :g:`Prop`, :g:`Set`  and :g:`Type`.
 
@@ -255,13 +264,13 @@ There are four sorts :g:`SProp`, :g:`Prop`, :g:`Set`  and :g:`Type`.
    propositions* (also called *strict propositions*).
 
 -  :g:`Prop` is the universe of *logical propositions*. The logical propositions
-   themselves are typing the proofs. We denote propositions by :token:`form`.
-   This constitutes a semantic subclass of the syntactic class :token:`term`.
+   themselves are typing the proofs. We denote propositions by :n:`@form`.
+   This constitutes a semantic subclass of the syntactic class :n:`@term`.
 
 -  :g:`Set` is the universe of *program types* or *specifications*. The
    specifications themselves are typing the programs. We denote
-   specifications by :token:`specif`. This constitutes a semantic subclass of
-   the syntactic class :token:`term`.
+   specifications by :n:`@specif`. This constitutes a semantic subclass of
+   the syntactic class :n:`@term`.
 
 -  :g:`Type` is the type of sorts.
 
@@ -280,15 +289,15 @@ Binders
    name ::= _
    | @ident
    binder ::= @name
-   | ( {+ @name } : @term )
-   | ( @name {? : @term } := @term )
-   | %{ {+ @name } {? : @term } %}
-   | [ {+ @name } {? : @term } ]
+   | ( {+ @name } : @type )
+   | ( @name {? : @type } := @term )
+   | ( @name : @type %| @term )
+   | %{ {+ @name } {? : @type } %}
+   | [ {+ @name } {? : @type } ]
    | `( {+, @typeclass_constraint } )
    | `%{ {+, @typeclass_constraint } %}
    | `[ {+, @typeclass_constraint } ]
    | ' @pattern0
-   | ( @name : @term %| @term )
    typeclass_constraint ::= {? ! } @term
    | %{ @name %} : {? ! } @term
    | @name : {? ! } @term
@@ -303,14 +312,14 @@ a notation for a sequence of binding variables sharing the same type:
 binder can also be any pattern prefixed by a quote, e.g. :g:`'(x,y)`.
 
 Some constructions allow the binding of a variable to value. This is
-called a “let-binder”. The entry :token:`binder` of the grammar accepts
+called a “let-binder”. The entry :n:`@binder` of the grammar accepts
 either an assumption binder as defined above or a let-binder. The notation in
 the latter case is :n:`(@ident := @term)`. In a let-binder, only one
 variable can be introduced at the same time. It is also possible to give
 the type of the variable as follows:
 :n:`(@ident : @type := @term)`.
 
-Lists of :token:`binder`\s are allowed. In the case of :g:`fun` and :g:`forall`,
+Lists of :n:`@binder`\s are allowed. In the case of :g:`fun` and :g:`forall`,
 it is intended that at least one binder of the list is an assumption otherwise
 fun and forall gets identical. Moreover, parentheses can be omitted in
 the case of a single sequence of bindings sharing the same type (e.g.:
@@ -322,9 +331,9 @@ Abstractions: fun
 -----------------
 
 The expression :n:`fun @ident : @type => @term` defines the
-*abstraction* of the variable :token:`ident`, of type :token:`type`, over the term
-:token:`term`. It denotes a function of the variable :token:`ident` that evaluates to
-the expression :token:`term` (e.g. :g:`fun x : A => x` denotes the identity
+*abstraction* of the variable :n:`@ident`, of type :n:`@type`, over the term
+:n:`@term`. It denotes a function of the variable :n:`@ident` that evaluates to
+the expression :n:`@term` (e.g. :g:`fun x : A => x` denotes the identity
 function on type :g:`A`). The keyword :g:`fun` can be followed by several
 binders as given in Section :ref:`binders`. Functions over
 several variables are equivalent to an iteration of one-variable
@@ -341,12 +350,12 @@ Products: forall
 ----------------
 
 The expression :n:`forall @ident : @type, @term` denotes the
-*product* of the variable :token:`ident` of type :token:`type`, over the term :token:`term`.
+*product* of the variable :n:`@ident` of type :n:`@type`, over the term :n:`@term`.
 As for abstractions, :g:`forall` is followed by a binder list, and products
 over several variables are equivalent to an iteration of one-variable
-products. Note that :token:`term` is intended to be a type.
+products. Note that :n:`@term` is intended to be a type.
 
-If the variable :token:`ident` occurs in :token:`term`, the product is called
+If the variable :n:`@ident` occurs in :n:`@term`, the product is called
 *dependent product*. The intention behind a dependent product
 :g:`forall x : A, B` is twofold. It denotes either
 the universal quantification of the variable :g:`x` of type :g:`A`
@@ -391,13 +400,13 @@ Type cast
    | @term10 :>
 
 The expression :n:`@term : @type` is a type cast expression. It enforces
-the type of :token:`term` to be :token:`type`.
+the type of :n:`@term` to be :n:`@type`.
 
 :n:`@term <: @type` locally sets up the virtual machine for checking that
-:token:`term` has type :token:`type`.
+:n:`@term` has type :n:`@type`.
 
-:n:`@term <<: @type` uses native compilation for checking that :token:`term`
-has type :token:`type`.
+:n:`@term <<: @type` uses native compilation for checking that :n:`@term`
+has type :n:`@type`.
 
 .. index:: _
 
@@ -418,15 +427,15 @@ Let-in definitions
 .. insertprodn term_let term_let
 
 .. prodn::
-   term_let ::= let @name {? : @term } := @term in @term
-   | let @name {+ @binder } {? : @term } := @term in @term
+   term_let ::= let @name {? : @type } := @term in @term
+   | let @name {+ @binder } {? : @type } := @term in @term
    | let ( {*, @name } ) {? {? as @name } return @term100 } := @term in @term
    | let ' @pattern := @term {? return @term100 } in @term
    | let ' @pattern in @pattern := @term return @term100 in @term
 
 :n:`let @ident := @term in @term’`
-denotes the local binding of :token:`term` to the variable
-:token:`ident` in :token:`term`’. There is a syntactic sugar for let-in
+denotes the local binding of :n:`@term` to the variable
+:n:`@ident` in :n:`@term`’. There is a syntactic sugar for let-in
 definition of functions: :n:`let @ident {+ @binder} := @term in @term’`
 stands for :n:`let @ident := fun {+ @binder} => @term in @term’`.
 
@@ -463,8 +472,8 @@ to apply specific treatments accordingly.
 This paragraph describes the basic form of pattern matching. See
 Section :ref:`Mult-match` and Chapter :ref:`extendedpatternmatching` for the description
 of the general form. The basic form of pattern matching is characterized
-by a single :token:`case_item` expression, an :token:`eqn` restricted to a
-single :token:`pattern` and :token:`pattern` restricted to the form
+by a single :n:`@case_item` expression, an :n:`@eqn` restricted to a
+single :n:`@pattern` and :n:`@pattern` restricted to the form
 :n:`@qualid {* @ident}`.
 
 The expression
@@ -486,7 +495,7 @@ In the *dependent* case, there are three subcases. In the first subcase,
 the type in each branch may depend on the exact value being matched in
 the branch. In this case, the whole pattern matching itself depends on
 the term being matched. This dependency of the term being matched in the
-return type is expressed with an :n:`@ident` clause where :token:`ident`
+return type is expressed with an :n:`@ident` clause where :n:`@ident`
 is dependent in the return type. For instance, in the following example:
 
 .. coqtop:: in
@@ -538,7 +547,7 @@ dependency of the return type in the annotations of the inductive type
 is expressed with a clause in the form
 :n:`in @qualid {+ _ } {+ @pattern }`, where
 
--  :token:`qualid` is the inductive type of the term being matched;
+-  :n:`@qualid` is the inductive type of the term being matched;
 
 -  the holes :n:`_` match the parameters of the inductive type: the
    return type is not dependent on them.
@@ -587,7 +596,7 @@ Recursive and co-recursive functions: fix and cofix
 .. prodn::
    term_fix ::= let fix @fix_body in @term
    | fix @fix_body {? {+ with @fix_body } for @ident }
-   fix_body ::= @ident {* @binder } {? @fixannot } {? : @term } := @term
+   fix_body ::= @ident {* @binder } {? @fixannot } {? : @type } := @term
    fixannot ::= %{ struct @ident %}
    | %{ wf @term1_extended @ident %}
    | %{ measure @term1_extended {? @ident } {? @term1_extended } %}
@@ -595,92 +604,55 @@ Recursive and co-recursive functions: fix and cofix
    | @ @qualid {? @univ_annot }
 
 
-The expression “``fix`` :token:`ident`:math:`_1` :token:`binder`:math:`_1` ``:``
-:token:`type`:math:`_1` ``:=`` :token:`term`:math:`_1` ``with … with``
-:token:`ident`:math:`_n` :token:`binder`:math:`_n` : :token:`type`:math:`_n`
-``:=`` :token:`term`:math:`_n` ``for`` :token:`ident`:math:`_i`” denotes the
+The expression ":n:`fix @ident__1 @binder__1 : @type__1 := @term__1 with … with @ident__n @binder__n : @type__n := @term__n for @ident__i`" denotes the
 :math:`i`-th component of a block of functions defined by mutual structural
 recursion. It is the local counterpart of the :cmd:`Fixpoint` command. When
-:math:`n=1`, the “``for`` :token:`ident`:math:`_i`” clause is omitted.
+:math:`n=1`, the ":n:`for @ident__i`" clause is omitted.
 
 The association of a single fixpoint and a local definition have a special
-syntax: :n:`let fix @ident @binders := @term in` stands for
-:n:`let @ident := fix @ident @binders := @term in`. The same applies for co-fixpoints.
+syntax: :n:`let fix @ident {* @binder } := @term in` stands for
+:n:`let @ident := fix @ident {* @binder } := @term in`. The same applies for co-fixpoints.
 
 .. insertprodn term_cofix cofix_body
 
 .. prodn::
    term_cofix ::= let cofix @cofix_body in @term
    | cofix @cofix_body {? {+ with @cofix_body } for @ident }
-   cofix_body ::= @ident {* @binder } {? : @term } := @term
+   cofix_body ::= @ident {* @binder } {? : @type } := @term
 
-The expression “``cofix`` :token:`ident`:math:`_1` :token:`binder`:math:`_1` ``:``
-:token:`type`:math:`_1` ``with … with`` :token:`ident`:math:`_n` :token:`binder`:math:`_n`
-: :token:`type`:math:`_n` ``for`` :token:`ident`:math:`_i`” denotes the
-:math:`i`-th component of a block of terms defined by a mutual guarded
+The expression
+":n:`cofix @ident__1 @binder__1 : @type__1 with … with @ident__n @binder__n : @type__n for @ident__i`"
+denotes the :math:`i`-th component of a block of terms defined by a mutual guarded
 co-recursion. It is the local counterpart of the :cmd:`CoFixpoint` command. When
-:math:`n=1`, the “``for`` :token:`ident`:math:`_i`” clause is omitted.
+:math:`n=1`, the ":n:`for @ident__i`" clause is omitted.
 
 .. _vernacular:
 
 The Vernacular
 ==============
 
-.. insertgramXX vernac ident_opt2
-
-.. productionlist:: coq
-   decorated-sentence : [ `decoration` … `decoration` ] `sentence`
-   sentence           : `assumption`
-                      : `definition`
-                      : `inductive`
-                      : `fixpoint`
-                      : `assertion` `proof`
-   assumption         : `assumption_keyword` `assums`.
-   assumption_keyword : Axiom | Conjecture
-                      : Parameter | Parameters
-                      : Variable | Variables
-                      : Hypothesis | Hypotheses
-   assums             : `ident` … `ident` : `term`
-                      : ( `ident` … `ident` : `term` ) … ( `ident` … `ident` : `term` )
-   definition         : [Local] Definition `ident` [`binders`] [: `term`] := `term` .
-                      : Let `ident` [`binders`] [: `term`] := `term` .
-   binders            : binders binder
-                      : binder
-   inductive          : Inductive `ind_body` with … with `ind_body` .
-                      : CoInductive `ind_body` with … with `ind_body` .
-   ind_body           : `ident` [`binders`] : `term` :=
-                      : [[|] `ident` [`binders`] [:`term`] | … | `ident` [`binders`] [:`term`]]
-   fixpoint           : Fixpoint `fix_body` with … with `fix_body` .
-                      : CoFixpoint `fix_body` with … with `fix_body` .
-   assertion          : `assertion_keyword` `ident` [`binders`] : `term` .
-   assertion_keyword  : Theorem | Lemma
-                      : Remark | Fact
-                      : Corollary | Property | Proposition
-                      : Definition | Example
-   proof              : Proof . … Qed .
-                      : Proof . … Defined .
-                      : Proof . … Admitted .
-   decoration : #[ `attributes` ]
-   attributes : [`attribute`, … , `attribute`]
-   attribute :  `ident`
-             : `ident` = `string`
-             : `ident` ( `attributes` )
-
-.. todo:: This use of … in this grammar is inconsistent
-          What about removing the proof part of this grammar from this chapter
-          and putting it somewhere where top-level tactics can be described as well?
-          See also #7583.
-
-This grammar describes *The Vernacular* which is the language of
-commands of Gallina. A sentence of the vernacular language, like in
-many natural languages, begins with a capital letter and ends with a
-dot.
-
-Sentences may be *decorated* with so-called *attributes*,
-which are described in the corresponding section (:ref:`gallina-attributes`).
-
-The different kinds of command are described hereafter. They all suppose
-that the terms occurring in the sentences are well-typed.
+.. insertprodn vernacular vernacular
+
+.. prodn::
+   vernacular ::= {* {? @all_attrs } {| @command | @ltac_expr } . }
+
+The top-level input to |Coq| is a series of :production:`command`\s and :production:`tactic`\s,
+each terminated with a period
+and optionally decorated with :ref:`gallina-attributes`.  :n:`@ltac_expr` syntax supports both simple
+and compound tactics.  For example: ``split.`` is a simple tactic while ``split; auto.`` combines two
+simple tactics.
+
+Tactics specify how to transform the current proof state as a step in creating a proof.  They
+are syntactically valid only when |Coq| is in proof mode, such as after a :cmd:`Theorem` command
+and before any subsequent proof-terminating command such as :cmd:`Qed`.  See :ref:`proofhandling` for more
+on proof mode.
+
+By convention, command names begin with uppercase letters, while
+tactic names begin with lowercase letters.  Commands appear in the
+HTML documentation in blue boxes after the label "Command".  In the pdf, they appear
+after the boldface label "Command:".  Commands are listed in the :ref:`command_index`.
+
+Similarly, tactics appear after the label "Tactic".  Tactics are listed in the :ref:`tactic_index`.
 
 .. _gallina-assumptions:
 
@@ -688,73 +660,68 @@ Assumptions
 -----------
 
 Assumptions extend the environment with axioms, parameters, hypotheses
-or variables. An assumption binds an :token:`ident` to a :token:`type`. It is accepted
-by Coq if and only if this :token:`type` is a correct type in the environment
-preexisting the declaration and if :token:`ident` was not previously defined in
-the same module. This :token:`type` is considered to be the type (or
-specification, or statement) assumed by :token:`ident` and we say that :token:`ident`
-has type :token:`type`.
+or variables. An assumption binds an :n:`@ident` to a :n:`@type`. It is accepted
+by Coq if and only if this :n:`@type` is a correct type in the environment
+preexisting the declaration and if :n:`@ident` was not previously defined in
+the same module. This :n:`@type` is considered to be the type (or
+specification, or statement) assumed by :n:`@ident` and we say that :n:`@ident`
+has type :n:`@type`.
 
 .. _Axiom:
 
-.. cmd:: Parameter @ident : @type
-
-   This command links :token:`type` to the name :token:`ident` as its specification in
-   the global context. The fact asserted by :token:`type` is thus assumed as a
-   postulate.
-
-   .. exn:: @ident already exists.
-      :name: @ident already exists. (Axiom)
-      :undocumented:
-
-   .. cmdv:: Parameter {+ @ident } : @type
+.. cmd:: @assumption_token {? Inline {? ( @num ) } } {| {+ ( @assumpt ) } | @assumpt }
+   :name: Axiom; Axioms; Conjecture; Conjectures; Hypothesis; Hypotheses; Parameter; Parameters; Variable; Variables
 
-      Adds several parameters with specification :token:`type`.
+   .. insertprodn assumption_token of_type
 
-   .. cmdv:: Parameter {+ ( {+ @ident } : @type ) }
+   .. prodn::
+      assumption_token ::= {| Axiom | Axioms }
+      | {| Conjecture | Conjectures }
+      | {| Parameter | Parameters }
+      | {| Hypothesis | Hypotheses }
+      | {| Variable | Variables }
+      assumpt ::= {+ @ident_decl } @of_type
+      ident_decl ::= @ident {? @univ_decl }
+      of_type ::= {| : | :> | :>> } @type
 
-      Adds blocks of parameters with different specifications.
+   These commands bind one or more :n:`@ident`\(s) to specified :n:`@type`\(s) as their specifications in
+   the global context. The fact asserted by the :n:`@type` (or, equivalently, the existence
+   of an object of this type) is accepted as a postulate.
 
-   .. cmdv:: Local Parameter {+ ( {+ @ident } : @type ) }
-      :name: Local Parameter
+   :cmd:`Axiom`, :cmd:`Conjecture`, :cmd:`Parameter` and their plural forms
+   are equivalent.  They can take the :attr:`local` attribute (see :ref:`gallina-attributes`),
+   which makes the defined :n:`@ident`\s accessible by :cmd:`Import` and its variants
+   only through their fully qualified names.
 
-      Such parameters are never made accessible through their unqualified name by
-      :cmd:`Import` and its variants. You have to explicitly give their fully
-      qualified name to refer to them.
+   Similarly, :cmd:`Hypothesis`, :cmd:`Variable` and their plural forms are equivalent.  Outside
+   of a section, these are equivalent to :n:`Local Parameter`.  Inside a section, the
+   :n:`@ident`\s defined are only accessible within the section.  When the current section
+   is closed, the :n:`@ident`\(s) become undefined and every object depending on them will be explicitly
+   parameterized (i.e., the variables are *discharged*).  See Section :ref:`section-mechanism`.
 
-   .. cmdv:: {? Local } Parameters {+ ( {+ @ident } : @type ) }
-             {? Local } Axiom {+ ( {+ @ident } : @type ) }
-             {? Local } Axioms {+ ( {+ @ident } : @type ) }
-             {? Local } Conjecture {+ ( {+ @ident } : @type ) }
-             {? Local } Conjectures {+ ( {+ @ident } : @type ) }
-      :name: Parameters; Axiom; Axioms; Conjecture; Conjectures
+.. example:: Simple assumptions
 
-      These variants are synonyms of :n:`{? Local } Parameter {+ ( {+ @ident } : @type ) }`.
+    .. coqtop:: reset in
 
-   .. cmdv:: Variable  {+ ( {+ @ident } : @type ) }
-             Variables {+ ( {+ @ident } : @type ) }
-             Hypothesis {+ ( {+ @ident } : @type ) }
-             Hypotheses {+ ( {+ @ident } : @type ) }
-      :name: Variable (outside a section); Variables (outside a section); Hypothesis (outside a section); Hypotheses (outside a section)
+       Parameter X Y : Set.
+       Parameter (R : X -> Y -> Prop) (S : Y -> X -> Prop).
+       Axiom R_S_inv : forall x y, R x y <-> S y x.
 
-      Outside of any section, these variants are synonyms of
-      :n:`Local Parameter {+ ( {+ @ident } : @type ) }`.
-      For their meaning inside a section, see :cmd:`Variable` in
-      :ref:`section-mechanism`.
+.. exn:: @ident already exists.
+   :name: @ident already exists. (Axiom)
+   :undocumented:
 
-      .. warn:: @ident is declared as a local axiom [local-declaration,scope]
+.. warn:: @ident is declared as a local axiom [local-declaration,scope]
 
-         Warning generated when using :cmd:`Variable` instead of
-         :cmd:`Local Parameter`.
+   Warning generated when using :cmd:`Variable` or its equivalent
+   instead of :n:`Local Parameter` or its equivalent.
 
 .. note::
-   It is advised to use the commands :cmd:`Axiom`, :cmd:`Conjecture` and
+   We advise using the commands :cmd:`Axiom`, :cmd:`Conjecture` and
    :cmd:`Hypothesis` (and their plural forms) for logical postulates (i.e. when
-   the assertion :token:`type` is of sort :g:`Prop`), and to use the commands
+   the assertion :n:`@type` is of sort :g:`Prop`), and to use the commands
    :cmd:`Parameter` and :cmd:`Variable` (and their plural forms) in other cases
-   (corresponding to the declaration of an abstract mathematical entity).
-
-.. seealso:: Section :ref:`section-mechanism`.
+   (corresponding to the declaration of an abstract object of the given type).
 
 .. _gallina-definitions:
 
@@ -777,85 +744,92 @@ type which is the type of its body.
 A formal presentation of constants and environments is given in
 Section :ref:`typing-rules`.
 
-.. cmd:: Definition @ident := @term
-
-   This command binds :token:`term` to the name :token:`ident` in the environment,
-   provided that :token:`term` is well-typed.
-
-   .. exn:: @ident already exists.
-      :name: @ident already exists. (Definition)
-      :undocumented:
-
-   .. cmdv:: Definition @ident : @type := @term
-
-      This variant checks that the type of :token:`term` is definitionally equal to
-      :token:`type`, and registers :token:`ident` as being of type
-      :token:`type`, and bound to value :token:`term`.
-
-      .. exn:: The term @term has type @type while it is expected to have type @type'.
-         :undocumented:
-
-   .. cmdv:: Definition @ident @binders {? : @type } := @term
+.. cmd:: {| Definition | Example } @ident_decl @def_body
+   :name: Definition; Example
 
-      This is equivalent to
-      :n:`Definition @ident : forall @binders, @type := fun @binders => @term`.
+   .. insertprodn def_body def_body
 
-   .. cmdv:: Local Definition @ident {? @binders } {? : @type } := @term
-      :name: Local Definition
+   .. prodn::
+      def_body ::= {* @binder } {? : @type } := {? @reduce } @term
+      | {* @binder } : @type
 
-      Such definitions are never made accessible through their
-      unqualified name by :cmd:`Import` and its variants.
-      You have to explicitly give their fully qualified name to refer to them.
+   These commands bind :n:`@term` to the name :n:`@ident` in the environment,
+   provided that :n:`@term` is well-typed.  They can take the :attr:`local` attribute (see :ref:`gallina-attributes`),
+   which makes the defined :n:`@ident` accessible by :cmd:`Import` and its variants
+   only through their fully qualified names.
+   If :n:`@reduce` is present then :n:`@ident` is bound to the result of the specified
+   computation on :n:`@term`.
 
-   .. cmdv:: {? Local } Example @ident {? @binders } {? : @type } := @term
-      :name: Example
+   If :n:`@term` is omitted, Coq enters the proof editing mode.  This can be
+   used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic.
+   In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant
+   for which the computational behavior is relevant.  See :ref:`proof-editing-mode`.
 
-      This is equivalent to :cmd:`Definition`.
+   The form :n:`Definition @ident : @type := @term` checks that the type of :n:`@term`
+   is definitionally equal to :n:`@type`, and registers :n:`@ident` as being of type
+   :n:`@type`, and bound to value :n:`@term`.
 
-   .. cmdv:: Let @ident := @term
-      :name: Let (outside a section)
+   The form :n:`Definition @ident {* @binder } : @type := @term` is equivalent to
+   :n:`Definition @ident : forall {* @binder }, @type := fun {* @binder } => @term`.
 
-      Outside of any section, this variant is a synonym of
-      :n:`Local Definition @ident := @term`.
-      For its meaning inside a section, see :cmd:`Let` in
-      :ref:`section-mechanism`.
-
-      .. warn:: @ident is declared as a local definition [local-declaration,scope]
+   .. seealso:: :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`.
 
-         Warning generated when using :cmd:`Let` instead of
-         :cmd:`Local Definition`.
+   .. exn:: @ident already exists.
+      :name: @ident already exists. (Definition)
+      :undocumented:
 
-.. seealso:: Section :ref:`section-mechanism`, commands :cmd:`Opaque`,
-             :cmd:`Transparent`, and tactic :tacn:`unfold`.
+   .. exn:: The term @term has type @type while it is expected to have type @type'.
+      :undocumented:
 
 .. _gallina-inductive-definitions:
 
-Inductive definitions
----------------------
-
-We gradually explain simple inductive types, simple annotated inductive
-types, simple parametric inductive types, mutually inductive types. We
-explain also co-inductive types.
-
-Simple inductive types
-~~~~~~~~~~~~~~~~~~~~~~
+Inductive types
+---------------
 
-.. cmd:: Inductive @ident : {? @sort } := {? | } @ident : @type {* | @ident : @type }
-
-   This command defines a simple inductive type and its constructors.
-   The first :token:`ident` is the name of the inductively defined type
-   and :token:`sort` is the universe where it lives. The next :token:`ident`\s
-   are the names of its constructors and :token:`type` their respective types.
-   Depending on the universe where the inductive type :token:`ident` lives
-   (e.g. its type :token:`sort`), Coq provides a number of destructors.
-   Destructors are named :token:`ident`\ ``_sind``,:token:`ident`\ ``_ind``,
-   :token:`ident`\ ``_rec`` or :token:`ident`\ ``_rect`` which respectively
-   correspond to elimination principles on :g:`SProp`, :g:`Prop`, :g:`Set` and :g:`Type`.
-   The type of the destructors expresses structural induction/recursion
-   principles over objects of type :token:`ident`.
-   The constant :token:`ident`\ ``_ind`` is always provided,
-   whereas :token:`ident`\ ``_rec`` and :token:`ident`\ ``_rect`` can be
-   impossible to derive (for example, when :token:`ident` is a proposition).
+.. cmd:: Inductive @inductive_definition {* with @inductive_definition }
+
+   .. insertprodn inductive_definition field_body
+
+   .. prodn::
+      inductive_definition ::= {? > } @ident_decl {* @binder } {? %| {* @binder } } {? : @type } {? := {? @constructors_or_record } } {? @decl_notations }
+      constructors_or_record ::= {? %| } {+| @constructor }
+      | {? @ident } %{ {+; @record_field } %}
+      constructor ::= @ident {* @binder } {? @of_type }
+      record_field ::= {* #[ {*, @attr } ] } @name {? @field_body } {? %| @num } {? @decl_notations }
+      field_body ::= {* @binder } @of_type
+      | {* @binder } @of_type := @term
+      | {* @binder } := @term
+
+   This command defines one or more
+   inductive types and its constructors.  Coq generates destructors
+   depending on the universe that the inductive type belongs to.
+
+   The destructors are named :n:`@ident`\ ``_rect``, :n:`@ident`\ ``_ind``,
+   :n:`@ident`\ ``_rec`` and :n:`@ident`\ ``_sind``, which
+   respectively correspond to elimination principles on :g:`Type`, :g:`Prop`,
+   :g:`Set` and :g:`SProp`.  The type of the destructors
+   expresses structural induction/recursion principles over objects of
+   type :n:`@ident`.  The constant :n:`@ident`\ ``_ind`` is always
+   generated, whereas :n:`@ident`\ ``_rec`` and :n:`@ident`\ ``_rect``
+   may be impossible to derive (for example, when :n:`@ident` is a
+   proposition).
+
+   This command supports the :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`,
+   :attr:`universes(template)`, :attr:`universes(notemplate)`,
+   :attr:`Cumulative`, :attr:`NonCumulative` and :attr:`Private` attributes.
+
+   Mutually inductive types can be defined by including multiple :n:`@inductive_definition`\s.
+   The :n:`@ident`\s are simultaneously added to the environment before the types of constructors are checked.
+   Each :n:`@ident` can be used independently thereafter.
+   See :ref:`mutually_inductive_types`.
+
+   If the entire inductive definition is parameterized with :n:`@binder`\s, the parameters correspond
+   to a local context in which the entire set of inductive declarations is interpreted.
+   For this reason, the parameters must be strictly the same for each inductive type.
+   See :ref:`parametrized-inductive-types`.
+
+   Constructor :n:`@ident`\s can come with :n:`@binder`\s, in which case
+   the actual type of the constructor is :n:`forall {* @binder }, @type`.
 
    .. exn:: Non strictly positive occurrence of @ident in @type.
 
@@ -867,66 +841,71 @@ Simple inductive types
    .. exn:: The conclusion of @type is not valid; it must be built from @ident.
 
       The conclusion of the type of the constructors must be the inductive type
-      :token:`ident` being defined (or :token:`ident` applied to arguments in
+      :n:`@ident` being defined (or :n:`@ident` applied to arguments in
       the case of annotated inductive types — cf. next section).
 
-   .. example::
+The following subsections show examples of simple inductive types, simple annotated
+inductive types, simple parametric inductive types and mutually inductive
+types.
 
-      The set of natural numbers is defined as:
+.. _simple-inductive-types:
 
-      .. coqtop:: all
+Simple inductive types
+~~~~~~~~~~~~~~~~~~~~~~
 
-         Inductive nat : Set :=
-         | O : nat
-         | S : nat -> nat.
+A simple inductive type belongs to a universe that is a simple :n:`sort`.
 
-      The type nat is defined as the least :g:`Set` containing :g:`O` and closed by
-      the :g:`S` constructor. The names :g:`nat`, :g:`O` and :g:`S` are added to the
-      environment.
+.. example::
 
-      Now let us have a look at the elimination principles. They are three of them:
-      :g:`nat_ind`, :g:`nat_rec` and :g:`nat_rect`. The type of :g:`nat_ind` is:
+   The set of natural numbers is defined as:
 
-      .. coqtop:: all
+   .. coqtop:: reset all
 
-         Check nat_ind.
+      Inductive nat : Set :=
+      | O : nat
+      | S : nat -> nat.
 
-      This is the well known structural induction principle over natural
-      numbers, i.e. the second-order form of Peano’s induction principle. It
-      allows proving some universal property of natural numbers (:g:`forall
-      n:nat, P n`) by induction on :g:`n`.
+   The type nat is defined as the least :g:`Set` containing :g:`O` and closed by
+   the :g:`S` constructor. The names :g:`nat`, :g:`O` and :g:`S` are added to the
+   environment.
 
-      The types of :g:`nat_rec` and :g:`nat_rect` are similar, except that they pertain
-      to :g:`(P:nat->Set)` and :g:`(P:nat->Type)` respectively. They correspond to
-      primitive induction principles (allowing dependent types) respectively
-      over sorts ``Set`` and ``Type``.
+   This definition generates four elimination principles:
+   :g:`nat_rect`, :g:`nat_ind`, :g:`nat_rec` and :g:`nat_sind`. The type of :g:`nat_ind` is:
 
-   .. cmdv:: Inductive @ident {? : @sort } := {? | } {*| @ident {? @binders } {? : @type } }
+   .. coqtop:: all
 
-      Constructors :token:`ident`\s can come with :token:`binders` in which case,
-      the actual type of the constructor is :n:`forall @binders, @type`.
+      Check nat_ind.
 
-      In the case where inductive types have no annotations (next section
-      gives an example of such annotations), a constructor can be defined
-      by only giving the type of its arguments.
+   This is the well known structural induction principle over natural
+   numbers, i.e. the second-order form of Peano’s induction principle. It
+   allows proving universal properties of natural numbers (:g:`forall
+   n:nat, P n`) by induction on :g:`n`.
 
-      .. example::
+   The types of :g:`nat_rect`, :g:`nat_rec` and :g:`nat_sind` are similar, except that they
+   apply to, respectively, :g:`(P:nat->Type)`, :g:`(P:nat->Set)` and :g:`(P:nat->SProp)`. They correspond to
+   primitive induction principles (allowing dependent types) respectively
+   over sorts ```Type``, ``Set`` and ``SProp``.
 
-         .. coqtop:: none
+In the case where inductive types don't have annotations (the next section
+gives an example of annotations), a constructor can be defined
+by giving the type of its arguments alone.
 
-            Reset nat.
+.. example::
 
-         .. coqtop:: in
+   .. coqtop:: reset none
 
-            Inductive nat : Set := O | S (_:nat).
+      Reset nat.
 
+   .. coqtop:: in
+
+      Inductive nat : Set := O | S (_:nat).
 
 Simple annotated inductive types
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-In an annotated inductive types, the universe where the inductive type
-is defined is no longer a simple sort, but what is called an arity,
-which is a type whose conclusion is a sort.
+In annotated inductive types, the universe where the inductive type
+is defined is no longer a simple :n:`@sort`, but what is called an arity,
+which is a type whose conclusion is a :n:`@sort`.
 
 .. example::
 
@@ -939,72 +918,74 @@ which is a type whose conclusion is a sort.
       | even_0 : even O
       | even_SS : forall n:nat, even n -> even (S (S n)).
 
-   The type :g:`nat->Prop` means that even is a unary predicate (inductively
+   The type :g:`nat->Prop` means that :g:`even` is a unary predicate (inductively
    defined) over natural numbers. The type of its two constructors are the
-   defining clauses of the predicate even. The type of :g:`even_ind` is:
+   defining clauses of the predicate :g:`even`. The type of :g:`even_ind` is:
 
    .. coqtop:: all
 
       Check even_ind.
 
-   From a mathematical point of view it asserts that the natural numbers satisfying
-   the predicate even are exactly in the smallest set of naturals satisfying the
+   From a mathematical point of view, this asserts that the natural numbers satisfying
+   the predicate :g:`even` are exactly in the smallest set of naturals satisfying the
    clauses :g:`even_0` or :g:`even_SS`. This is why, when we want to prove any
    predicate :g:`P` over elements of :g:`even`, it is enough to prove it for :g:`O`
    and to prove that if any natural number :g:`n` satisfies :g:`P` its double
-   successor :g:`(S (S n))` satisfies also :g:`P`. This is indeed analogous to the
+   successor :g:`(S (S n))` satisfies also :g:`P`. This is analogous to the
    structural induction principle we got for :g:`nat`.
 
+.. _parametrized-inductive-types:
+
 Parameterized inductive types
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmdv:: Inductive @ident @binders {? : @type } := {? | } @ident : @type {* | @ident : @type}
+In the previous example, each constructor introduces a different
+instance of the predicate :g:`even`. In some cases, all the constructors
+introduce the same generic instance of the inductive definition, in
+which case, instead of an annotation, we use a context of parameters
+which are :n:`@binder`\s shared by all the constructors of the definition.
 
-   In the previous example, each constructor introduces a different
-   instance of the predicate :g:`even`. In some cases, all the constructors
-   introduce the same generic instance of the inductive definition, in
-   which case, instead of an annotation, we use a context of parameters
-   which are :token:`binders` shared by all the constructors of the definition.
+Parameters differ from inductive type annotations in that the
+conclusion of each type of constructor invokes the inductive type with
+the same parameter values of its specification.
 
-   Parameters differ from inductive type annotations in the fact that the
-   conclusion of each type of constructor invoke the inductive type with
-   the same values of parameters as its specification.
+.. example::
 
-   .. example::
+   A typical example is the definition of polymorphic lists:
 
-      A typical example is the definition of polymorphic lists:
+   .. coqtop:: all
 
-      .. coqtop:: in
+      Inductive list (A:Set) : Set :=
+      | nil : list A
+      | cons : A -> list A -> list A.
 
-         Inductive list (A:Set) : Set :=
-         | nil : list A
-         | cons : A -> list A -> list A.
+   In the type of :g:`nil` and :g:`cons`, we write ":g:`list A`" and not
+   just ":g:`list`". The constructors :g:`nil` and :g:`cons` have these types:
 
-      In the type of :g:`nil` and :g:`cons`, we write :g:`(list A)` and not
-      just :g:`list`. The constructors :g:`nil` and :g:`cons` will have respectively
-      types:
+   .. coqtop:: all
 
-      .. coqtop:: all
+      Check nil.
+      Check cons.
 
-         Check nil.
-         Check cons.
+   Observe that the destructors are also quantified with :g:`(A:Set)`, for example:
 
-      Types of destructors are also quantified with :g:`(A:Set)`.
+   .. coqtop:: all
 
-      Once again, it is possible to specify only the type of the arguments
-      of the constructors, and to omit the type of the conclusion:
+      Check list_ind.
 
-      .. coqtop:: none
+   Once again, the types of the constructor arguments and of the conclusion can be omitted:
+
+   .. coqtop:: none
 
-         Reset list.
+      Reset list.
 
-      .. coqtop:: in
+   .. coqtop:: in
 
-         Inductive list (A:Set) : Set := nil | cons (_:A) (_:list A).
+      Inductive list (A:Set) : Set := nil | cons (_:A) (_:list A).
 
 .. note::
-   + It is possible in the type of a constructor, to
-     invoke recursively the inductive definition on an argument which is not
+   + The constructor type can
+     recursively invoke the inductive definition on an argument which is not
      the parameter itself.
 
      One can define :
@@ -1019,7 +1000,9 @@ Parameterized inductive types
 
      .. coqtop:: all reset
 
-        Inductive list2 (A:Set) : Set := nil2 | cons2 (_:A) (_:list2 (A*A)).
+        Inductive list2 (A:Set) : Set :=
+        | nil2
+        | cons2 (_:A) (_:list2 (A*A)).
 
      But the following definition will give an error:
 
@@ -1078,42 +1061,16 @@ Parameterized inductive types
 .. seealso::
    Section :ref:`inductive-definitions` and the :tacn:`induction` tactic.
 
-Variants
-~~~~~~~~
-
-.. cmd:: Variant @ident @binders {? : @type } := {? | } @ident : @type {* | @ident : @type}
-
-   The :cmd:`Variant` command is identical to the :cmd:`Inductive` command, except
-   that it disallows recursive definition of types (for instance, lists cannot
-   be defined using :cmd:`Variant`). No induction scheme is generated for
-   this variant, unless the :flag:`Nonrecursive Elimination Schemes` flag is on.
-
-   .. exn:: The @num th argument of @ident must be @ident in @type.
-      :undocumented:
+.. _mutually_inductive_types:
 
 Mutually defined inductive types
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmdv:: Inductive @ident {? : @type } := {? | } {*| @ident : @type } {* with {? | } {*| @ident {? : @type } } }
-
-   This variant allows defining a block of mutually inductive types.
-   It has the same semantics as the above :cmd:`Inductive` definition for each
-   :token:`ident`. All :token:`ident` are simultaneously added to the environment.
-   Then well-typing of constructors can be checked. Each one of the :token:`ident`
-   can be used on its own.
+.. example:: Mutually defined inductive types
 
-   .. cmdv:: Inductive @ident @binders {? : @type } := {? | } {*| @ident : @type } {* with {? | } {*| @ident @binders {? : @type } } }
-
-      In this variant, the inductive definitions are parameterized
-      with :token:`binders`. However, parameters correspond to a local context
-      in which the whole set of inductive declarations is done. For this
-      reason, the parameters must be strictly the same for each inductive types.
-
-.. example::
-
-   The typical example of a mutual inductive data type is the one for trees and
-   forests. We assume given two types :g:`A` and :g:`B` as variables. It can
-   be declared the following way.
+   A typical example of mutually inductive data types is trees and
+   forests. We assume two types :g:`A` and :g:`B` that are given as variables. The types can
+   be declared like this:
 
    .. coqtop:: in
 
@@ -1125,13 +1082,10 @@ Mutually defined inductive types
       | leaf : B -> forest
       | cons : tree -> forest -> forest.
 
-   This declaration generates automatically six induction principles. They are
-   respectively called :g:`tree_rec`, :g:`tree_ind`, :g:`tree_rect`,
-   :g:`forest_rec`, :g:`forest_ind`, :g:`forest_rect`. These ones are not the most
-   general ones but are just the induction principles corresponding to each
-   inductive part seen as a single inductive definition.
+   This declaration automatically generates eight induction principles. They are not the most
+   general principles, but they correspond to each inductive part seen as a single inductive definition.
 
-   To illustrate this point on our example, we give the types of :g:`tree_rec`
+   To illustrate this point on our example, here are the types of :g:`tree_rec`
    and :g:`forest_rec`.
 
    .. coqtop:: all
@@ -1142,7 +1096,7 @@ Mutually defined inductive types
 
    Assume we want to parameterize our mutual inductive definitions with the
    two type variables :g:`A` and :g:`B`, the declaration should be
-   done the following way:
+   done as follows:
 
    .. coqdoc::
 
@@ -1161,10 +1115,27 @@ Mutually defined inductive types
    A generic command :cmd:`Scheme` is useful to build automatically various
    mutual induction principles.
 
+Variants
+~~~~~~~~
+
+.. cmd:: Variant @inductive_definition {* with @inductive_definition }
+
+   The :cmd:`Variant` command is identical to the :cmd:`Inductive` command, except
+   that it disallows recursive definition of types (for instance, lists cannot
+   be defined using :cmd:`Variant`). No induction scheme is generated for
+   this variant, unless the :flag:`Nonrecursive Elimination Schemes` flag is on.
+
+   This command supports the :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`,
+   :attr:`universes(template)`, :attr:`universes(notemplate)`,
+   :attr:`Cumulative`, :attr:`NonCumulative` and :attr:`Private` attributes.
+
+   .. exn:: The @num th argument of @ident must be @ident in @type.
+      :undocumented:
+
 .. _coinductive-types:
 
 Co-inductive types
-~~~~~~~~~~~~~~~~~~
+------------------
 
 The objects of an inductive type are well-founded with respect to the
 constructors of the type. In other words, such objects contain only a
@@ -1174,7 +1145,7 @@ constructors. Infinite objects are introduced by a non-ending (but
 effective) process of construction, defined in terms of the constructors
 of the type.
 
-.. cmd:: CoInductive @ident @binders {? : @type } := {? | } @ident : @type {* | @ident : @type}
+.. cmd:: CoInductive @inductive_definition {* with @inductive_definition }
 
    This command introduces a co-inductive type.
    The syntax of the command is the same as the command :cmd:`Inductive`.
@@ -1182,10 +1153,14 @@ of the type.
    type, since such principles only make sense for inductive types.
    For co-inductive types, the only elimination principle is case analysis.
 
+   This command supports the :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`,
+   :attr:`universes(template)`, :attr:`universes(notemplate)`,
+   :attr:`Cumulative`, :attr:`NonCumulative` and :attr:`Private` attributes.
+
 .. example::
 
-   An example of a co-inductive type is the type of infinite sequences of
-   natural numbers, usually called streams.
+   The type of infinite sequences of natural numbers, usually called streams,
+   is an example of a co-inductive type.
 
    .. coqtop:: in
 
@@ -1199,13 +1174,12 @@ of the type.
       Definition hd (x:Stream) := let (a,s) := x in a.
       Definition tl (x:Stream) := let (a,s) := x in s.
 
-Definition of co-inductive predicates and blocks of mutually
+Definitions of co-inductive predicates and blocks of mutually
 co-inductive definitions are also allowed.
 
 .. example::
 
-   An example of a co-inductive predicate is the extensional equality on
-   streams:
+   The extensional equality on streams is an example of a co-inductive type:
 
    .. coqtop:: in
 
@@ -1219,7 +1193,7 @@ co-inductive definitions are also allowed.
    objects in Section :ref:`cofixpoint`.
 
 Caveat
-++++++
+~~~~~~
 
 The ability to define co-inductive types by constructors, hereafter called
 *positive co-inductive types*, is known to break subject reduction. The story is
@@ -1287,27 +1261,41 @@ constructions.
 
 .. _Fixpoint:
 
-.. cmd:: Fixpoint @ident @binders {? {struct @ident} } {? : @type } := @term
+.. cmd:: Fixpoint @fix_definition {* with @fix_definition }
+
+   .. insertprodn fix_definition fix_definition
+
+   .. prodn::
+      fix_definition ::= @ident_decl {* @binder } {? @fixannot } {? : @type } {? := @term } {? @decl_notations }
 
    This command allows defining functions by pattern matching over inductive
    objects using a fixed point construction. The meaning of this declaration is
-   to define :token:`ident` a recursive function with arguments specified by
-   the :token:`binders` such that :token:`ident` applied to arguments
-   corresponding to these :token:`binders` has type :token:`type`, and is
-   equivalent to the expression :token:`term`. The type of :token:`ident` is
-   consequently :n:`forall @binders, @type` and its value is equivalent
-   to :n:`fun @binders => @term`.
+   to define :n:`@ident` as a recursive function with arguments specified by
+   the :n:`@binder`\s such that :n:`@ident` applied to arguments
+   corresponding to these :n:`@binder`\s has type :n:`@type`, and is
+   equivalent to the expression :n:`@term`. The type of :n:`@ident` is
+   consequently :n:`forall {* @binder }, @type` and its value is equivalent
+   to :n:`fun {* @binder } => @term`.
 
    To be accepted, a :cmd:`Fixpoint` definition has to satisfy some syntactical
    constraints on a special argument called the decreasing argument. They
    are needed to ensure that the :cmd:`Fixpoint` definition always terminates.
-   The point of the :n:`{struct @ident}` annotation is to let the user tell the
-   system which argument decreases along the recursive calls.
+   The point of the :n:`{struct @ident}` annotation (see :n:`@fixannot`) is to
+   let the user tell the system which argument decreases along the recursive calls.
 
-   The :n:`{struct @ident}` annotation may be left implicit, in this case the
-   system tries successively arguments from left to right until it finds one
+   The :n:`{struct @ident}` annotation may be left implicit, in which case the
+   system successively tries arguments from left to right until it finds one
    that satisfies the decreasing condition.
 
+   The :n:`with` clause allows simultaneously defining several mutual fixpoints.
+   It is especially useful when defining functions over mutually defined
+   inductive types.  Example: :ref:`Mutual Fixpoints<example_mutual_fixpoints>`.
+
+   If :n:`@term` is omitted, :n:`@type` is required and Coq enters the proof editing mode.
+   This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic.
+   In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant
+   for which the computational behavior is relevant.  See :ref:`proof-editing-mode`.
+
    .. note::
 
       + Some fixpoints may have several arguments that fit as decreasing
@@ -1388,35 +1376,35 @@ constructions.
                   end
          end.
 
+.. _example_mutual_fixpoints:
 
-   .. cmdv:: Fixpoint @ident @binders {? {struct @ident} } {? : @type } := @term {* with @ident @binders {? : @type } := @term }
+   .. example:: Mutual fixpoints
 
-      This variant allows defining simultaneously several mutual fixpoints.
-      It is especially useful when defining functions over mutually defined
-      inductive types.
+      The size of trees and forests can be defined the following way:
 
-      .. example::
-
-         The size of trees and forests can be defined the following way:
-
-         .. coqtop:: all
+      .. coqtop:: all
 
-            Fixpoint tree_size (t:tree) : nat :=
-            match t with
-            | node a f => S (forest_size f)
-            end
-            with forest_size (f:forest) : nat :=
-            match f with
-            | leaf b => 1
-            | cons t f' => (tree_size t + forest_size f')
-            end.
+         Fixpoint tree_size (t:tree) : nat :=
+         match t with
+         | node a f => S (forest_size f)
+         end
+         with forest_size (f:forest) : nat :=
+         match f with
+         | leaf b => 1
+         | cons t f' => (tree_size t + forest_size f')
+         end.
 
 .. _cofixpoint:
 
 Definitions of recursive objects in co-inductive types
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmd:: CoFixpoint @ident {? @binders } {? : @type } := @term
+.. cmd:: CoFixpoint @cofix_definition {* with @cofix_definition }
+
+   .. insertprodn cofix_definition cofix_definition
+
+   .. prodn::
+      cofix_definition ::= @ident_decl {* @binder } {? : @type } {? := @term } {? @decl_notations }
 
    This command introduces a method for constructing an infinite object of a
    coinductive type. For example, the stream containing all natural numbers can
@@ -1428,7 +1416,7 @@ Definitions of recursive objects in co-inductive types
 
       CoFixpoint from (n:nat) : Stream := Seq n (from (S n)).
 
-   Oppositely to recursive ones, there is no decreasing argument in a
+   Unlike recursive definitions, there is no decreasing argument in a
    co-recursive definition. To be admissible, a method of construction must
    provide at least one extra constructor of the infinite object for each
    iteration. A syntactical guard condition is imposed on co-recursive
@@ -1457,10 +1445,63 @@ Definitions of recursive objects in co-inductive types
       Eval compute in (hd (from 0)).
       Eval compute in (tl (from 0)).
 
-   .. cmdv:: CoFixpoint @ident {? @binders } {? : @type } := @term {* with @ident {? @binders } : {? @type } := @term }
+   As in the :cmd:`Fixpoint` command, the :n:`with` clause allows simultaneously
+   defining several mutual cofixpoints.
+
+   If :n:`@term` is omitted, :n:`@type` is required and Coq enters the proof editing mode.
+   This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic.
+   In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant
+   for which the computational behavior is relevant.  See :ref:`proof-editing-mode`.
+
+.. _Computations:
+
+Computations
+------------
+
+.. insertprodn reduce pattern_occ
+
+.. prodn::
+   reduce ::= Eval @red_expr in
+   red_expr ::= red
+   | hnf
+   | simpl {? @delta_flag } {? @ref_or_pattern_occ }
+   | cbv {? @strategy_flag }
+   | cbn {? @strategy_flag }
+   | lazy {? @strategy_flag }
+   | compute {? @delta_flag }
+   | vm_compute {? @ref_or_pattern_occ }
+   | native_compute {? @ref_or_pattern_occ }
+   | unfold {+, @unfold_occ }
+   | fold {+ @term1_extended }
+   | pattern {+, @pattern_occ }
+   | @ident
+   delta_flag ::= {? - } [ {+ @smart_global } ]
+   smart_global ::= @qualid
+   | @by_notation
+   by_notation ::= @string {? % @ident }
+   strategy_flag ::= {+ @red_flags }
+   | @delta_flag
+   red_flags ::= beta
+   | iota
+   | match
+   | fix
+   | cofix
+   | zeta
+   | delta {? @delta_flag }
+   ref_or_pattern_occ ::= @smart_global {? at @occs_nums }
+   | @term1_extended {? at @occs_nums }
+   occs_nums ::= {+ @num_or_var }
+   | - @num_or_var {* @int_or_var }
+   num_or_var ::= @num
+   | @ident
+   int_or_var ::= @int
+   | @ident
+   unfold_occ ::= @smart_global {? at @occs_nums }
+   pattern_occ ::= @term1_extended {? at @occs_nums }
 
-      As in the :cmd:`Fixpoint` command, it is possible to introduce a block of
-      mutually dependent methods.
+See :ref:`Conversion-rules`.
+
+.. todo:: Add text here
 
 .. _Assertions:
 
@@ -1472,40 +1513,26 @@ inhabitant of the type) is interactively built using tactics. The interactive
 proof mode is described in Chapter :ref:`proofhandling` and the tactics in
 Chapter :ref:`Tactics`. The basic assertion command is:
 
-.. cmd:: Theorem @ident {? @binders } : @type
+.. cmd:: @thm_token @ident_decl {* @binder } : @type {* with @ident_decl {* @binder } : @type }
+   :name: Theorem; Lemma; Fact; Remark; Corollary; Proposition; Property
 
-   After the statement is asserted, Coq needs a proof. Once a proof of
-   :token:`type` under the assumptions represented by :token:`binders` is given and
-   validated, the proof is generalized into a proof of :n:`forall @binders, @type` and
-   the theorem is bound to the name :token:`ident` in the environment.
+   .. insertprodn thm_token thm_token
 
-   .. exn:: The term @term has type @type which should be Set, Prop or Type.
-      :undocumented:
+   .. prodn::
+      thm_token ::= Theorem
+      | Lemma
+      | Fact
+      | Remark
+      | Corollary
+      | Proposition
+      | Property
 
-   .. exn:: @ident already exists.
-      :name: @ident already exists. (Theorem)
-
-      The name you provided is already defined. You have then to choose
-      another name.
-
-   .. exn:: Nested proofs are not allowed unless you turn the Nested Proofs Allowed flag on.
-
-      You are asserting a new statement while already being in proof editing mode.
-      This feature, called nested proofs, is disabled by default.
-      To activate it, turn the :flag:`Nested Proofs Allowed` flag on.
-
-   .. cmdv:: Lemma @ident {? @binders } : @type
-             Remark @ident {? @binders } : @type
-             Fact @ident {? @binders } : @type
-             Corollary @ident {? @binders } : @type
-             Proposition @ident {? @binders } : @type
-      :name: Lemma; Remark; Fact; Corollary; Proposition
-
-      These commands are all synonyms of :n:`Theorem @ident {? @binders } : type`.
-
-.. cmdv:: Theorem @ident {? @binders } : @type {* with @ident {? @binders } : @type}
+   After the statement is asserted, Coq needs a proof. Once a proof of
+   :n:`@type` under the assumptions represented by :n:`@binder`\s is given and
+   validated, the proof is generalized into a proof of :n:`forall {* @binder }, @type` and
+   the theorem is bound to the name :n:`@ident` in the environment.
 
-   This command is useful for theorems that are proved by simultaneous induction
+   Forms using the :n:`with` clause are useful for theorems that are proved by simultaneous induction
    over a mutually inductive assumption, or that assert mutually dependent
    statements in some mutual co-inductive type. It is equivalent to
    :cmd:`Fixpoint` or :cmd:`CoFixpoint` but using tactics to build the proof of
@@ -1522,46 +1549,29 @@ Chapter :ref:`Tactics`. The basic assertion command is:
    correct at some time of the interactive development of a proof, use the
    command :cmd:`Guarded`.
 
-   The command can be used also with :cmd:`Lemma`, :cmd:`Remark`, etc. instead of
-   :cmd:`Theorem`.
-
-.. cmdv:: Definition @ident {? @binders } : @type
-
-   This allows defining a term of type :token:`type` using the proof editing
-   mode. It behaves as :cmd:`Theorem` but is intended to be used in conjunction with
-   :cmd:`Defined` in order to define a constant of which the computational
-   behavior is relevant.
-
-   The command can be used also with :cmd:`Example` instead of :cmd:`Definition`.
-
-   .. seealso:: :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`.
-
-.. cmdv:: Let @ident {? @binders } : @type
-
-   Like :n:`Definition @ident {? @binders } : @type` except that the definition is
-   turned into a let-in definition generalized over the declarations depending
-   on it after closing the current section.
+   .. exn:: The term @term has type @type which should be Set, Prop or Type.
+      :undocumented:
 
-.. cmdv:: Fixpoint @ident @binders : @type {* with @ident @binders : @type}
+   .. exn:: @ident already exists.
+      :name: @ident already exists. (Theorem)
 
-   This generalizes the syntax of :cmd:`Fixpoint` so that one or more bodies
-   can be defined interactively using the proof editing mode (when a
-   body is omitted, its type is mandatory in the syntax). When the block
-   of proofs is completed, it is intended to be ended by :cmd:`Defined`.
+      The name you provided is already defined. You have then to choose
+      another name.
 
-.. cmdv:: CoFixpoint @ident {? @binders } : @type {* with @ident {? @binders } : @type}
+   .. exn:: Nested proofs are not allowed unless you turn the Nested Proofs Allowed flag on.
 
-   This generalizes the syntax of :cmd:`CoFixpoint` so that one or more bodies
-   can be defined interactively using the proof editing mode.
+      You are asserting a new statement while already being in proof editing mode.
+      This feature, called nested proofs, is disabled by default.
+      To activate it, turn the :flag:`Nested Proofs Allowed` flag on.
 
-A proof starts by the keyword :cmd:`Proof`. Then Coq enters the proof editing mode
-until the proof is completed. The proof editing mode essentially contains
-tactics that are described in chapter :ref:`Tactics`. Besides tactics, there
-are commands to manage the proof editing mode. They are described in Chapter
+Proofs start with the keyword :cmd:`Proof`. Then Coq enters the proof editing mode
+until the proof is completed. In proof editing mode, the user primarily enters
+tactics, which are described in chapter :ref:`Tactics`. The user may also enter
+commands to manage the proof editing mode. They are described in Chapter
 :ref:`proofhandling`.
 
-When the proof is completed it should be validated and put in the environment
-using the keyword :cmd:`Qed`.
+When the proof is complete, use the :cmd:`Qed` command so the kernel verifies
+the proof and adds it to the environment.
 
 .. note::
 
@@ -1590,33 +1600,96 @@ using the keyword :cmd:`Qed`.
 Attributes
 -----------
 
-Any vernacular command can be decorated with a list of attributes, enclosed
-between ``#[`` (hash and opening square bracket) and ``]`` (closing square bracket)
-and separated by commas ``,``. Multiple space-separated blocks may be provided.
+.. insertprodn all_attrs legacy_attrs
 
-Each attribute has a name (an identifier) and may have a value.
-A value is either a :token:`string` (in which case it is specified with an equal ``=`` sign),
-or a list of attributes, enclosed within brackets.
+.. prodn::
+   all_attrs ::= {* #[ {*, @attr } ] } {? @legacy_attrs }
+   attr ::= @ident {? @attr_value }
+   attr_value ::= = @string
+   | ( {*, @attr } )
+   legacy_attrs ::= {? {| Local | Global } } {? {| Polymorphic | Monomorphic } } {? Program } {? {| Cumulative | NonCumulative } } {? Private }
+
+Attributes modify the behavior of a command or tactic.
+Syntactically, most commands and tactics can be decorated with attributes, but
+attributes not supported by the command or tactic will be flagged as errors.
+
+The order of top-level attributes doesn't affect their meaning.  ``#[foo,bar]``, ``#[bar,foo]``,
+``#[foo]#[bar]`` and ``#[bar]#[foo]`` are equivalent.
+
+The legacy attributes (:n:`@legacy_attrs`) provide an older, alternate syntax
+for certain attributes.  They are equivalent to new attributes as follows:
+
+================  ================================
+Legacy attribute  New attribute
+================  ================================
+`Local`           :attr:`local`
+`Global`          :attr:`global`
+`Polymorphic`     :attr:`universes(polymorphic)`
+`Monomorphic`     :attr:`universes(monomorphic)`
+`Cumulative`      none
+`NonCumulative`   none
+`Private`         none
+`Program`         :attr:`program`
+================  ================================
 
 Some attributes are specific to a command, and so are described with
-that command. Currently, the following attributes are recognized by a
-variety of commands:
+that command. Currently, the following attributes are recognized:
+
+.. attr:: universes(monomorphic)
+   :name: universes(monomorphic)
+
+   See :ref:`polymorphicuniverses`.
+
+.. attr:: universes(polymorphic)
+   :name: universes(polymorphic)
+
+   See :ref:`polymorphicuniverses`.
+
+.. attr:: universes(template)
+   :name: universes(template)
+
+   See :ref:`Template-polymorphism`
+
+.. attr:: universes(notemplate)
+   :name: universes(notemplate)
+
+   See :ref:`Template-polymorphism`
+
+.. attr:: program
 
-``universes(monomorphic)``, ``universes(polymorphic)``
-    Equivalent to the ``Monomorphic`` and
-    ``Polymorphic`` flags (see :ref:`polymorphicuniverses`).
+   See :ref:`programs`.
 
-``program``
-    Takes no value, equivalent to the ``Program`` flag
-    (see :ref:`programs`).
+.. attr:: global
 
-``global``, ``local``
-    Take no value, equivalent to the ``Global`` and ``Local`` flags
-    (see :ref:`controlling-locality-of-commands`).
+   See :ref:`controlling-locality-of-commands`.
 
-``deprecated``
-    Takes as value the optional attributes ``since`` and ``note``;
-    both have a string value.
+.. attr:: local
+
+   See :ref:`controlling-locality-of-commands`.
+
+.. attr:: Cumulative
+
+   Legacy attribute, only allowed in a polymorphic context.
+   Specifies that two instances of the same inductive type (family) are convertible
+   based on the universe variances; they do not need to be equal.
+   See :ref:`cumulative`.
+
+.. attr:: NonCumulative
+
+   Legacy attribute, only allowed in a polymorphic context.
+   Specifies that two instances of the same inductive type (family) are convertible
+   only if all the universes are equal.
+   See :ref:`cumulative`.
+
+.. attr:: Private
+
+   Legacy attribute.  Documentation to be added.
+
+.. attr:: deprecated ( {? since = @string , } {? note = @string } )
+   :name: deprecated
+
+    At least one of :n:`since` or :n:`note` must be present.  If both are present,
+    either one may appear first and they must be separated by a comma.
 
     This attribute is supported by the following commands: :cmd:`Ltac`,
     :cmd:`Tactic Notation`, :cmd:`Notation`, :cmd:`Infix`.
@@ -1634,12 +1707,13 @@ variety of commands:
        :n:`@string__1` is the actual notation, :n:`@string__2` is the version number,
        :n:`@string__3` is the note.
 
-``canonical``
+.. attr:: canonical
+
     This attribute can decorate a :cmd:`Definition` or :cmd:`Let` command.
     It is equivalent to having a :cmd:`Canonical Structure` declaration just
     after the command.
 
-    This attirbute can take the value ``false`` when decorating a record field
+    This attribute can take the value ``false`` when decorating a record field
     declaration with the effect of preventing the field from being involved in
     the inference of canonical instances.
 
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index b722b1af74..56e33b9ea5 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -907,9 +907,9 @@ Ltac2 from Ltac1
 Same as above by switching Ltac1 by Ltac2 and using the `ltac2` quotation
 instead.
 
-.. productionlist:: coq
-  ltac_expr : ltac2 : ( `ltac2_term` )
-            : ltac2 : ( `ident` ... `ident` |- `ltac2_term` )
+.. prodn::
+   ltac_expr += ltac2 : ( `ltac2_term` )
+   | ltac2 : ( `ident` ... `ident` |- `ltac2_term` )
 
 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
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index b1734b3f19..03eebc32f9 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -80,20 +80,19 @@ list of assertion commands is given in :ref:`Assertions`. The command
       a while when the proof is large. In some exceptional cases one may
       even incur a memory overflow.
 
-   .. cmdv:: Defined
-      :name: Defined
+.. cmd:: Defined
 
-      Same as :cmd:`Qed` but the proof is then declared transparent, which means
-      that its content can be explicitly used for type checking and that it can be
-      unfolded in conversion tactics (see :ref:`performingcomputations`,
-      :cmd:`Opaque`, :cmd:`Transparent`).
+   Same as :cmd:`Qed`, except the proof is made *transparent*, which means
+   that its content can be explicitly used for type checking and that it can be
+   unfolded in conversion tactics (see :ref:`performingcomputations`,
+   :cmd:`Opaque`, :cmd:`Transparent`).
 
-   .. cmdv:: Save @ident
-      :name: Save
+.. cmd:: Save @ident
+   :name: Save
 
-      Forces the name of the original goal to be :token:`ident`. This
-      command (and the following ones) can only be used if the original goal
-      has been opened using the :cmd:`Goal` command.
+   Forces the name of the original goal to be :token:`ident`. This
+   command can only be used if the original goal
+   was opened using the :cmd:`Goal` command.
 
 .. cmd:: Admitted
 
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 46215f16a6..90a991794f 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -1702,7 +1702,7 @@ Intro patterns
   when it is the
   very *first* :token:`i_pattern` after tactic ``=>`` tactical *and* tactic
   is not a move, is a *branching*:token:`i_pattern`. It executes the sequence
-  :token:`i_item`:math:`_i` on the i-th   subgoal produced by tactic. The
+  :n:`@i_item__i` on the i-th subgoal produced by tactic. The
   execution of tactic should thus generate exactly m subgoals, unless the
   ``[…]`` :token:`i_pattern` comes after an initial ``//`` or ``//=``
   :token:`s_item` that closes some of the goals produced by ``tactic``, in
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 2fa4f1fa42..6a0ce20c79 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -1281,16 +1281,16 @@ Managing the local context
       is an occurrence clause whose syntax and behavior are described in
       :ref:`goal occurrences <occurrencessets>`.
 
-   .. tacv:: set (@ident @binders := @term) {? in @goal_occurrences }
+   .. tacv:: set (@ident {* @binder } := @term) {? in @goal_occurrences }
 
-      This is equivalent to :n:`set (@ident := fun @binders => @term) {? in @goal_occurrences }`.
+      This is equivalent to :n:`set (@ident := fun {* @binder } => @term) {? in @goal_occurrences }`.
 
    .. tacv:: set @term {? in @goal_occurrences }
 
       This behaves as :n:`set (@ident := @term) {? in @goal_occurrences }`
       but :token:`ident` is generated by Coq.
 
-   .. tacv:: eset (@ident {? @binders } := @term) {? in @goal_occurrences }
+   .. tacv:: eset (@ident {* @binder } := @term) {? in @goal_occurrences }
              eset @term {? in @goal_occurrences }
       :name: eset; _
 
@@ -1326,16 +1326,16 @@ Managing the local context
    without performing any replacement in the goal or in the hypotheses. It is
    equivalent to :n:`set (@ident := @term) in |-`.
 
-   .. tacv:: pose (@ident @binders := @term)
+   .. tacv:: pose (@ident {* @binder } := @term)
 
-      This is equivalent to :n:`pose (@ident := fun @binders => @term)`.
+      This is equivalent to :n:`pose (@ident := fun {* @binder } => @term)`.
 
    .. tacv:: pose @term
 
       This behaves as :n:`pose (@ident := @term)` but :token:`ident` is
       generated by Coq.
 
-   .. tacv:: epose (@ident {? @binders} := @term)
+   .. tacv:: epose (@ident {* @binder } := @term)
              epose @term
       :name: epose; _
 
diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst
index 5b0b3c51b0..34197c4fcf 100644
--- a/doc/sphinx/user-extensions/proof-schemes.rst
+++ b/doc/sphinx/user-extensions/proof-schemes.rst
@@ -337,31 +337,31 @@ Generation of inversion principles with ``Derive`` ``Inversion``
 -----------------------------------------------------------------
 
 .. cmd:: Derive Inversion @ident with @ident Sort @sort
-         Derive Inversion @ident with (forall @binders, @ident @term) Sort @sort
+         Derive Inversion @ident with (forall {* @binder }, @ident @term) Sort @sort
 
    This command generates an inversion principle for the
    :tacn:`inversion ... using ...` tactic.  The first :token:`ident` is the name
    of the generated principle.  The second :token:`ident` should be an inductive
    predicate, and :token:`binders` the variables occurring in the term
    :token:`term`. This command generates the inversion lemma for the sort
-   :token:`sort` corresponding to the instance :n:`forall @binders, @ident @term`.
+   :token:`sort` corresponding to the instance :n:`forall {* @binder }, @ident @term`.
    When applied, it is equivalent to having inverted the instance with the
    tactic :g:`inversion`.
 
 .. cmdv:: Derive Inversion_clear @ident with @ident Sort @sort
-          Derive Inversion_clear @ident with (forall @binders, @ident @term) Sort @sort
+          Derive Inversion_clear @ident with (forall {* @binder }, @ident @term) Sort @sort
 
    When applied, it is equivalent to having inverted the instance with the
    tactic inversion replaced by the tactic `inversion_clear`.
 
 .. cmdv:: Derive Dependent Inversion @ident with @ident Sort @sort
-          Derive Dependent Inversion @ident with (forall @binders, @ident @term) Sort @sort
+          Derive Dependent Inversion @ident with (forall {* @binder }, @ident @term) Sort @sort
 
    When applied, it is equivalent to having inverted the instance with
    the tactic `dependent inversion`.
 
 .. cmdv:: Derive Dependent Inversion_clear @ident with @ident Sort @sort
-          Derive Dependent Inversion_clear @ident with (forall @binders, @ident @term) Sort @sort
+          Derive Dependent Inversion_clear @ident with (forall {* @binder }, @ident @term) Sort @sort
 
    When applied, it is equivalent to having inverted the instance
    with the tactic `dependent inversion_clear`.
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 8bfcab0f4e..e1545bdc2b 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -310,10 +310,10 @@ at the time of use of the notation.
 The Infix command
 ~~~~~~~~~~~~~~~~~~
 
-The :cmd:`Infix` command is a shortening for declaring notations of infix
+The :cmd:`Infix` command is a shortcut for declaring notations for infix
 symbols.
 
-.. cmd:: Infix "@symbol" := @term {? (@modifiers) }.
+.. cmd:: Infix @string := @term {? (@modifiers) }
 
    This command is equivalent to
 
@@ -366,7 +366,7 @@ Thanks to reserved notations, the inductive, co-inductive, record, recursive and
 corecursive definitions can benefit from customized notations. To do this, insert
 a ``where`` notation clause after the definition of the (co)inductive type or
 (co)recursive term (or after the definition of each of them in case of mutual
-definitions). The exact syntax is given by :token:`decl_notation` for inductive,
+definitions). The exact syntax is given by :n:`@decl_notation` for inductive,
 co-inductive, recursive and corecursive definitions and in :ref:`record-types`
 for records. Here are examples:
 
@@ -909,7 +909,6 @@ notations are given below. The optional :production:`scope` is described in
                  : Fixpoint `fix_body` [`decl_notation`] with … with `fix_body` [`decl_notation`].
                  : CoFixpoint `fix_body` [`decl_notation`] with … with `fix_body` [`decl_notation`].
                  : [Local] Declare Custom Entry `ident`.
-   decl_notation : [where `string` := `term` [: `scope`] and … and `string` := `term` [: `scope`]].
    modifiers     : `modifier`, … , `modifier`
    modifier      : at level `num`
                  : in custom `ident`
@@ -939,6 +938,12 @@ notations are given below. The optional :production:`scope` is described in
                  : as pattern
                  : as strict pattern
 
+.. insertprodn decl_notations decl_notation
+
+.. prodn::
+   decl_notations ::= where @decl_notation {* and @decl_notation }
+   decl_notation ::= @string := @term1_extended {? : @ident }
+
 .. note:: No typing of the denoted expression is performed at definition
           time. Type checking is done only at the time of use of the notation.
 
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 8d74e3c1e5..d6ecf311f1 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -294,7 +294,7 @@ class VernacObject(NotationObject):
 
     Example::
 
-       .. cmd:: Infix "@symbol" := @term ({+, @modifier}).
+       .. cmd:: Infix @string := @term1_extended {? ( {+, @syntax_modifier } ) } {? : @ident }
 
           This command is equivalent to :n:`…`.
     """
@@ -346,7 +346,7 @@ class AttributeNotationObject(NotationObject):
 
     Example::
 
-       .. attr:: #[ local ]
+       .. attr:: local
     """
     subdomain = "attr"
     index_suffix = "(attribute)"
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 9c1827f5b7..3524d77380 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -39,7 +39,7 @@ RENAME: [
 | Prim.natural natural
 *)
 | Vernac.rec_definition rec_definition
-
+(* todo: hmm, rename adds 1 prodn to closed_binder?? *)
 | Constr.closed_binder closed_binder
 ]
 
@@ -162,11 +162,6 @@ lconstr: [
 | DELETE l_constr
 ]
 
-type_cstr: [
-| REPLACE ":" lconstr
-| WITH OPT ( ":" lconstr )
-| DELETE (* empty *)
-]
 
 let_type_cstr: [
 | DELETE OPT [ ":" lconstr ]
@@ -210,8 +205,6 @@ term_let: [
 atomic_constr: [
 (* @Zimmi48: "string" used only for notations, but keep to be consistent with patterns *)
 (* | DELETE string *)
-| REPLACE global univ_instance
-| WITH global OPT univ_instance
 | REPLACE "?" "[" ident "]"
 | WITH "?[" ident "]"
 | MOVETO term_evar "?[" ident "]"
@@ -237,8 +230,6 @@ operconstr10: [
 (* fixme: add in as a prodn somewhere *)
 | MOVETO dangling_pattern_extension_rule "@" pattern_identref LIST1 identref
 | DELETE dangling_pattern_extension_rule
-| REPLACE "@" global univ_instance LIST0 operconstr9
-| WITH "@" global OPT univ_instance LIST0 operconstr9
 ]
 
 operconstr9: [
@@ -285,13 +276,6 @@ binders_fixannot: [
 | LIST0 binder OPT fixannot
 ]
 
-
-of_type_with_opt_coercion: [
-| DELETE ":>" ">"
-| DELETE ":" ">" ">"
-| DELETE ":" ">"
-]
-
 binder: [
 | DELETE name
 ]
@@ -306,11 +290,15 @@ open_binders: [
 | DELETE closed_binder binders
 ]
 
+type: [
+| operconstr200
+]
+
 closed_binder: [
 | name
 
 | REPLACE "(" name LIST1 name ":" lconstr ")"
-| WITH "(" LIST1 name ":" lconstr ")"
+| WITH "(" LIST1 name ":" type ")"
 | DELETE "(" name ":" lconstr ")"
 
 | DELETE "(" name ":=" lconstr ")"
@@ -324,6 +312,16 @@ closed_binder: [
 | REPLACE "{" name LIST1 name ":" lconstr "}"
 | WITH "{" LIST1 name type_cstr "}"
 | DELETE "{" name ":" lconstr  "}"
+
+| DELETE "[" name "]"
+| DELETE "[" name LIST1 name "]"
+
+| REPLACE "[" name LIST1 name ":" lconstr "]"
+| WITH "[" LIST1 name type_cstr "]"
+| DELETE "[" name ":" lconstr  "]"
+
+| REPLACE "(" Prim.name ":" lconstr "|" lconstr ")"
+| WITH "(" Prim.name ":" type "|" lconstr ")"
 ]
 
 name_colon: [
@@ -377,28 +375,151 @@ eqn: [
 ]
 
 universe_increment: [
-| REPLACE "+" natural
-| WITH OPT ( "+" natural )
-| DELETE (* empty *)
+| OPTINREF
 ]
 
 evar_instance: [
-| REPLACE "@{" LIST1 inst SEP ";" "}"
-| WITH OPT ( "@{" LIST1 inst SEP ";" "}" )
+| OPTINREF
+]
+
+gallina: [
+| REPLACE thm_token ident_decl binders ":" lconstr LIST0 [ "with" ident_decl binders ":" lconstr ]
+| WITH thm_token ident_decl binders ":" type LIST0 [ "with" ident_decl binders ":" type ]
+| DELETE assumptions_token inline assum_list
+| REPLACE OPT cumulativity_token private_token finite_token LIST1 inductive_definition SEP "with"
+| WITH "Inductive" inductive_definition LIST0 ( "with" inductive_definition )
+|   "CoInductive" inductive_definition LIST0 ( "with" inductive_definition )
+|   "Variant" inductive_definition LIST0 ( "with" inductive_definition )
+|   [ "Record" | "Structure" ] inductive_definition LIST0 ( "with" inductive_definition )
+|   "Class" inductive_definition LIST0 ( "with" inductive_definition )
+| REPLACE "Fixpoint" LIST1 rec_definition SEP "with"
+| WITH "Fixpoint" rec_definition LIST0 ( "with" rec_definition )
+| REPLACE "Let" "Fixpoint" LIST1 rec_definition SEP "with"
+| WITH "Let" "Fixpoint" rec_definition LIST0 ( "with" rec_definition )
+| REPLACE "CoFixpoint" LIST1 corec_definition SEP "with"
+| WITH "CoFixpoint" corec_definition LIST0 ( "with" corec_definition )
+| REPLACE "Let" "CoFixpoint" LIST1 corec_definition SEP "with"
+| WITH "Let" "CoFixpoint" corec_definition LIST0 ( "with" corec_definition )
+| REPLACE "Scheme" LIST1 scheme SEP "with"
+| WITH "Scheme" scheme LIST0 ( "with" scheme )
+]
+
+DELETE: [
+| private_token
+| cumulativity_token
+]
+
+opt_coercion: [
+| OPTINREF
+]
+
+opt_constructors_or_fields: [
+| OPTINREF
+]
+
+SPLICE: [
+| opt_coercion
+| opt_constructors_or_fields
+]
+
+constructor_list_or_record_decl: [
+| OPTINREF
+]
+
+record_fields: [
+| REPLACE record_field ";" record_fields
+| WITH LIST1 record_field SEP ";"
+| DELETE record_field
 | DELETE (* empty *)
 ]
 
+decl_notation: [
+| REPLACE "where" LIST1 one_decl_notation SEP decl_sep
+| WITH "where" one_decl_notation LIST0 ( decl_sep one_decl_notation )
+]
+
+assumptions_token: [
+| DELETENT
+]
+
+inline: [
+| REPLACE "Inline" "(" natural ")"
+| WITH "Inline" OPT ( "(" natural ")" )
+| DELETE "Inline"
+| OPTINREF
+]
+
 univ_instance: [
-| DELETE (* empty *)
+| OPTINREF
+]
+
+univ_decl: [
+| REPLACE "@{" LIST0 identref [ "+" | ]     [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | bar_cbrace ] ]
+| WITH    "@{" LIST0 identref  OPT "+"  OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}"
+]
+
+of_type_with_opt_coercion: [
+| DELETENT
+]
+
+of_type_with_opt_coercion: [
+| [ ":" | ":>" | ":>>" ] type
+]
+
+attribute_value: [
+| OPTINREF
+]
+
+def_body: [
+| DELETE binders ":=" reduce lconstr
+| REPLACE binders ":" lconstr ":=" reduce lconstr
+| WITH LIST0 binder OPT (":" type) ":=" reduce lconstr
+| REPLACE binders ":" lconstr
+| WITH LIST0 binder ":" type
+]
+
+reduce: [
+| OPTINREF
+]
+
+occs: [
+| OPTINREF
+]
+
+delta_flag: [
+| REPLACE "-" "[" LIST1 smart_global "]"
+| WITH OPT "-" "[" LIST1 smart_global "]"
+| DELETE "[" LIST1 smart_global "]"
+| OPTINREF
+]
+
+strategy_flag: [
+| REPLACE OPT delta_flag
+| WITH delta_flag
+| (* empty *)
+| OPTINREF
 ]
 
-constr: [
-| REPLACE "@" global univ_instance
-| WITH "@" global OPT univ_instance
+export_token: [
+| OPTINREF
 ]
 
-(* todo: binders should be binders_opt *)
+functor_app_annot: [
+| OPTINREF
+]
+
+is_module_expr: [
+| OPTINREF
+]
 
+is_module_type: [
+| OPTINREF
+]
+
+gallina_ext: [
+| REPLACE "Arguments" smart_global LIST0 argument_spec_block OPT [ "," LIST1 [ LIST0 more_implicits_block ] SEP "," ] OPT [ ":" LIST1 arguments_modifier SEP "," ]
+| WITH "Arguments" smart_global LIST0 argument_spec_block    LIST0 [  "," LIST0 more_implicits_block ]                OPT [ ":" LIST1 arguments_modifier SEP "," ]
+]
 
 (* lexer stuff *)
 IDENT: [
@@ -478,6 +599,8 @@ tactic_expr1: [
 | EDIT match_key ADD_OPT "reverse" "goal" "with" match_context_list "end"
 | MOVETO ltac_match_goal match_key OPT "reverse" "goal" "with" match_context_list "end"
 | MOVETO ltac_match_term match_key tactic_expr5 "with" match_list "end"
+| REPLACE failkw [ int_or_var | ] LIST0 message_token
+| WITH failkw OPT int_or_var LIST0 message_token
 ]
 
 DELETE: [
@@ -544,12 +667,146 @@ bar_cbrace: [
 | WITH "|}"
 ]
 
+printable: [
+| REPLACE [ "Sorted" | ] "Universes" OPT printunivs_subgraph OPT ne_string
+| WITH OPT "Sorted" "Universes" OPT printunivs_subgraph OPT ne_string
+| INSERTALL "Print"
+]
+
+command: [
+| REPLACE "Print" printable
+| WITH printable
+| "SubClass" ident_decl def_body
+| REPLACE "Ltac" LIST1 ltac_tacdef_body SEP "with"
+| WITH "Ltac" ltac_tacdef_body LIST0 ( "with" ltac_tacdef_body )
+| REPLACE "Function" LIST1 function_rec_definition_loc SEP "with"      (* funind plugin *)
+| WITH "Function" function_rec_definition_loc LIST0 ( "with" function_rec_definition_loc )      (* funind plugin *)
+| REPLACE "Functional" "Scheme" LIST1 fun_scheme_arg SEP "with"      (* funind plugin *)
+| WITH "Functional" "Scheme" fun_scheme_arg LIST0 ( "with" fun_scheme_arg )      (* funind plugin *)
+
+]
+
+only_parsing: [
+| OPTINREF
+]
+
+syntax: [
+| REPLACE "Infix" ne_lstring ":=" constr [ "(" LIST1 syntax_modifier SEP "," ")" | ]   OPT [ ":" IDENT ]
+| WITH    "Infix" ne_lstring ":=" constr OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" IDENT ]
+| REPLACE "Notation" lstring ":=" constr [ "(" LIST1 syntax_modifier SEP "," ")" | ]   OPT [ ":" IDENT ]
+| WITH    "Notation" lstring ":=" constr OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" IDENT ]
+| 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 "," ")" ]
+]
+
+numnotoption: [
+| OPTINREF
+]
+
+binder_tactic: [
+| REPLACE "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" tactic_expr5
+| WITH "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" tactic_expr5
+]
+
+tactic_then_gen: [
+| OPTINREF
+]
+
+record_binder_body: [
+| REPLACE binders of_type_with_opt_coercion lconstr
+| WITH binders of_type_with_opt_coercion
+| REPLACE binders of_type_with_opt_coercion lconstr ":=" lconstr
+| WITH binders of_type_with_opt_coercion ":=" lconstr
+]
+
+simple_assum_coe: [
+| REPLACE LIST1 ident_decl of_type_with_opt_coercion lconstr
+| WITH LIST1 ident_decl of_type_with_opt_coercion
+]
+
+constructor_type: [
+| REPLACE binders [ of_type_with_opt_coercion lconstr | ]
+| WITH binders OPT of_type_with_opt_coercion
+]
+
 (* todo: is this really correct? Search for "Pvernac.register_proof_mode" *)
 (* consider tactic_command vs tac2mode *)
 vernac_aux: [
 | tactic_mode "."
 ]
 
+def_token: [
+| DELETE "SubClass" (* document separately from Definition and Example *)
+]
+
+assumption_token: [
+| REPLACE "Axiom"
+| WITH [ "Axiom" | "Axioms" ]
+| REPLACE "Conjecture"
+| WITH [ "Conjecture" | "Conjectures" ]
+| REPLACE "Hypothesis"
+| WITH [ "Hypothesis" | "Hypotheses" ]
+| REPLACE "Parameter"
+| WITH [ "Parameter" | "Parameters" ]
+| REPLACE "Variable"
+| WITH [ "Variable" | "Variables" ]
+]
+
+legacy_attrs: [
+| OPT [ "Local" | "Global" ] OPT [ "Polymorphic" | "Monomorphic" ] OPT "Program" OPT [ "Cumulative" | "NonCumulative" ] OPT "Private"
+]
+
+all_attrs: [
+| LIST0 ( "#[" LIST0 attribute SEP "," "]" ) OPT legacy_attrs
+]
+
+vernacular: [
+| LIST0 ( OPT all_attrs [ command | tactic ] "." )
+]
+
+rec_definition: [
+| REPLACE ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notation
+| WITH ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notation
+]
+
+corec_definition: [
+| REPLACE ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notation
+| WITH ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notation
+]
+
+type_cstr: [
+| REPLACE ":" lconstr
+| WITH ":" type
+| OPTINREF
+]
+
+decl_notation: [
+| OPTINREF
+]
+
+inductive_definition: [
+| REPLACE OPT ">" ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] OPT ( ":=" OPT constructor_list_or_record_decl ) OPT decl_notation
+| WITH OPT ">" ident_decl binders OPT [ "|" binders ] OPT [ ":" type ] OPT ( ":=" OPT constructor_list_or_record_decl ) OPT decl_notation
+]
+
+constructor_list_or_record_decl: [
+| DELETE "|" LIST1 constructor SEP "|"
+| REPLACE identref constructor_type "|" LIST1 constructor SEP "|"
+| WITH OPT "|" LIST1 constructor SEP "|"
+| DELETE identref constructor_type
+| REPLACE identref "{" record_fields "}"
+| WITH OPT identref "{" record_fields "}"
+| DELETE "{" record_fields "}"
+]
+
+record_binder: [
+| REPLACE name record_binder_body
+| WITH name OPT record_binder_body
+| DELETE name
+]
+
 SPLICE: [
 | noedit_mode
 | command_entry
@@ -642,8 +899,6 @@ SPLICE: [
 | tactic
 | uconstr
 | impl_ident_head
-| argument_spec
-| at_level
 | branches
 | check_module_type
 | decorated_vernac
@@ -666,7 +921,27 @@ SPLICE: [
 | evar_instance
 | fix_decls
 | cofix_decls
-]
+| assum_list
+| assum_coe
+| inline
+| occs
+| univ_name_list
+| ltac_info
+| field_mods
+| ltac_production_sep
+| ltac_tactic_level
+| printunivs_subgraph
+| ring_mods
+| scope_delimiter
+| eliminator  (* todo: splice or not? *)
+| quoted_attributes  (* todo: splice or not? *)
+| printable
+| only_parsing
+| def_token
+| record_fields
+| constructor_type
+| record_binder
+] (* end SPLICE *)
 
 RENAME: [
 | clause clause_dft_concl
@@ -711,6 +986,14 @@ RENAME: [
 | corec_definition cofix_definition
 | inst evar_binding
 | univ_instance univ_annot
+| simple_assum_coe assumpt
+| of_type_with_opt_coercion of_type
+| decl_notation decl_notations
+| one_decl_notation decl_notation
+| attribute attr
+| attribute_value attr_value
+| constructor_list_or_record_decl constructors_or_record
+| record_binder_body field_body
 ]
 
 
diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml
index 7d18630a02..5fcb56f5f2 100644
--- a/doc/tools/docgram/doc_grammar.ml
+++ b/doc/tools/docgram/doc_grammar.ml
@@ -1700,9 +1700,9 @@ let process_rst g file args seen tac_prods cmd_prods =
       let start_index = index_of start !g.order in
       let end_index = index_of end_ !g.order in
       if start_index = None then
-        error "%s line %d: '%s' is undefined\n" file !linenum start;
+        error "%s line %d: '%s' is undefined in insertprodn\n" file !linenum start;
       if end_index = None then
-        error "%s line %d: '%s' is undefined\n" file !linenum end_;
+        error "%s line %d: '%s' is undefined in insertprodn\n" file !linenum end_;
       if start_index <> None && end_index <> None then
         check_range_consistency g start end_;
       match start_index, end_index with
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index e12589bb89..529d81e424 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -322,8 +322,13 @@ closed_binder: [
 | "{" name LIST1 name ":" lconstr "}"
 | "{" name ":" lconstr "}"
 | "{" name LIST1 name "}"
+| "[" name "]"
+| "[" name LIST1 name ":" lconstr "]"
+| "[" name ":" lconstr "]"
+| "[" name LIST1 name "]"
 | "`(" LIST1 typeclass_constraint SEP "," ")"
 | "`{" LIST1 typeclass_constraint SEP "," "}"
+| "`[" LIST1 typeclass_constraint SEP "," "]"
 | "'" pattern0
 ]
 
@@ -643,6 +648,7 @@ command: [
 | "Show" "Ltac" "Profile"
 | "Show" "Ltac" "Profile" "CutOff" int
 | "Show" "Ltac" "Profile" string
+| "Show" "Lia" "Profile"      (* micromega plugin *)
 | "Add" "InjTyp" constr      (* micromega plugin *)
 | "Add" "BinOp" constr      (* micromega plugin *)
 | "Add" "UnOp" constr      (* micromega plugin *)
@@ -937,12 +943,12 @@ opt_constructors_or_fields: [
 ]
 
 inductive_definition: [
-| opt_coercion ident_decl binders OPT [ ":" lconstr ] opt_constructors_or_fields decl_notation
+| opt_coercion ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] opt_constructors_or_fields decl_notation
 ]
 
 constructor_list_or_record_decl: [
 | "|" LIST1 constructor SEP "|"
-| identref constructor_type "|" LIST0 constructor SEP "|"
+| identref constructor_type "|" LIST1 constructor SEP "|"
 | identref constructor_type
 | identref "{" record_fields "}"
 | "{" record_fields "}"
@@ -1270,7 +1276,7 @@ printable: [
 | "Instances" smart_global
 | "Coercions"
 | "Coercion" "Paths" class_rawexpr class_rawexpr
-| "Canonical" "Projections"
+| "Canonical" "Projections" LIST0 smart_global
 | "Typing" "Flags"
 | "Tables"
 | "Options"
@@ -1400,8 +1406,7 @@ syntax_modifier: [
 | "only" "parsing"
 | "format" STRING OPT STRING
 | IDENT; "," LIST1 IDENT SEP "," "at" level
-| IDENT; "at" level
-| IDENT; "at" level constr_as_binder_kind
+| IDENT; "at" level OPT constr_as_binder_kind
 | IDENT constr_as_binder_kind
 | IDENT syntax_extension_type
 ]
@@ -1412,17 +1417,18 @@ syntax_extension_type: [
 | "bigint"
 | "binder"
 | "constr"
-| "constr" OPT at_level OPT constr_as_binder_kind
+| "constr" at_level_opt OPT constr_as_binder_kind
 | "pattern"
 | "pattern" "at" "level" natural
 | "strict" "pattern"
 | "strict" "pattern" "at" "level" natural
 | "closed" "binder"
-| "custom" IDENT OPT at_level OPT constr_as_binder_kind
+| "custom" IDENT at_level_opt OPT constr_as_binder_kind
 ]
 
-at_level: [
+at_level_opt: [
 | "at" level
+|
 ]
 
 constr_as_binder_kind: [
@@ -1719,7 +1725,6 @@ simple_tactic: [
 | "restart_timer" OPT string
 | "finish_timing" OPT string
 | "finish_timing" "(" string ")" OPT string
-| "myred"      (* micromega plugin *)
 | "psatz_Z" int_or_var tactic      (* micromega plugin *)
 | "psatz_Z" tactic      (* micromega plugin *)
 | "xlia" tactic      (* micromega plugin *)
@@ -1735,13 +1740,12 @@ simple_tactic: [
 | "psatz_R" tactic      (* micromega plugin *)
 | "psatz_Q" int_or_var tactic      (* micromega plugin *)
 | "psatz_Q" tactic      (* micromega plugin *)
-| "iter_specs" tactic      (* micromega plugin *)
+| "zify_iter_specs" tactic      (* micromega plugin *)
 | "zify_op"      (* micromega plugin *)
-| "saturate"      (* micromega plugin *)
+| "zify_saturate"      (* micromega plugin *)
+| "zify_iter_let" tactic      (* micromega plugin *)
 | "nsatz_compute" constr      (* nsatz plugin *)
 | "omega"      (* omega plugin *)
-| "omega" "with" LIST1 ident      (* omega plugin *)
-| "omega" "with" "*"      (* omega plugin *)
 | "rtauto"
 | "protect_fv" string "in" ident      (* setoid_ring plugin *)
 | "protect_fv" string      (* setoid_ring plugin *)
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 63e0ca129c..908e3ccd51 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -29,7 +29,7 @@ vernac_control: [
 | "Redirect" string vernac_control
 | "Timeout" num vernac_control
 | "Fail" vernac_control
-| LIST0 ( "#[" LIST0 attribute SEP "," "]" ) vernac
+| LIST0 ( "#[" LIST0 attr SEP "," "]" ) vernac
 ]
 
 term: [
@@ -102,50 +102,24 @@ dangling_pattern_extension_rule: [
 | "@" "?" ident LIST1 ident
 ]
 
-record_fields: [
-| record_field ";" record_fields
-| record_field
-|
-]
-
-record_field: [
-| LIST0 ( "#[" LIST0 attribute SEP "," "]" ) record_binder OPT [ "|" num ] decl_notation
-]
-
-decl_notation: [
-| "where" LIST1 one_decl_notation SEP "and"
-|
-]
-
-one_decl_notation: [
-| string ":=" term1_extended OPT [ ":" ident ]
+assumption_token: [
+| [ "Axiom" | "Axioms" ]
+| [ "Conjecture" | "Conjectures" ]
+| [ "Parameter" | "Parameters" ]
+| [ "Hypothesis" | "Hypotheses" ]
+| [ "Variable" | "Variables" ]
 ]
 
-record_binder: [
-| name
-| name record_binder_body
+assumpt: [
+| LIST1 ident_decl of_type
 ]
 
-record_binder_body: [
-| LIST0 binder of_type_with_opt_coercion term
-| LIST0 binder of_type_with_opt_coercion term ":=" term
-| LIST0 binder ":=" term
-]
-
-of_type_with_opt_coercion: [
-| ":>>"
-| ":>"
-| ":"
+ident_decl: [
+| ident OPT univ_decl
 ]
 
-attribute: [
-| ident attribute_value
-]
-
-attribute_value: [
-| "=" string
-| "(" LIST0 attribute SEP "," ")"
-|
+of_type: [
+| [ ":" | ":>" | ":>>" ] type
 ]
 
 qualid: [
@@ -156,6 +130,10 @@ field_ident: [
 | "." ident
 ]
 
+type: [
+| term
+]
+
 numeral: [
 | LIST1 digit OPT ( "." LIST1 digit ) OPT [ [ "e" | "E" ] OPT [ "+" | "-" ] LIST1 digit ]
 ]
@@ -184,6 +162,27 @@ subsequent_letter: [
 | [ first_letter | digit | "'" | unicode_id_part ]
 ]
 
+vernacular: [
+| LIST0 ( OPT all_attrs [ command | ltac_expr ] "." )
+]
+
+all_attrs: [
+| LIST0 ( "#[" LIST0 attr SEP "," "]" ) OPT legacy_attrs
+]
+
+attr: [
+| ident OPT attr_value
+]
+
+attr_value: [
+| "=" string
+| "(" LIST0 attr SEP "," ")"
+]
+
+legacy_attrs: [
+| OPT [ "Local" | "Global" ] OPT [ "Polymorphic" | "Monomorphic" ] OPT "Program" OPT [ "Cumulative" | "NonCumulative" ] OPT "Private"
+]
+
 sort: [
 | "Set"
 | "Prop"
@@ -208,6 +207,10 @@ universe_name: [
 | "Prop"
 ]
 
+univ_annot: [
+| "@{" LIST0 universe_level "}"
+]
+
 universe_level: [
 | "Set"
 | "Prop"
@@ -216,8 +219,12 @@ universe_level: [
 | qualid
 ]
 
-univ_annot: [
-| "@{" LIST0 universe_level "}"
+univ_decl: [
+| "@{" LIST0 ident OPT "+" OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}"
+]
+
+univ_constraint: [
+| universe_name [ "<" | "=" | "<=" ] universe_name
 ]
 
 term_fix: [
@@ -226,7 +233,7 @@ term_fix: [
 ]
 
 fix_body: [
-| ident LIST0 binder OPT fixannot OPT ( ":" term ) ":=" term
+| ident LIST0 binder OPT fixannot OPT ( ":" type ) ":=" term
 ]
 
 fixannot: [
@@ -246,12 +253,12 @@ term_cofix: [
 ]
 
 cofix_body: [
-| ident LIST0 binder OPT ( ":" term ) ":=" term
+| ident LIST0 binder OPT ( ":" type ) ":=" term
 ]
 
 term_let: [
-| "let" name OPT ( ":" term ) ":=" term "in" term
-| "let" name LIST1 binder OPT ( ":" term ) ":=" term "in" term
+| "let" name OPT ( ":" type ) ":=" term "in" term
+| "let" name LIST1 binder OPT ( ":" type ) ":=" term "in" term
 | "let" "(" LIST0 name SEP "," ")" OPT [ OPT [ "as" name ] "return" term100 ] ":=" term "in" term
 | "let" "'" pattern ":=" term OPT ( "return" term100 ) "in" term
 | "let" "'" pattern "in" pattern ":=" term "return" term100 "in" term
@@ -269,13 +276,15 @@ name: [
 
 binder: [
 | name
-| "(" LIST1 name ":" term ")"
-| "(" name OPT ( ":" term ) ":=" term ")"
-| "{" LIST1 name OPT ( ":" term ) "}"
+| "(" LIST1 name ":" type ")"
+| "(" name OPT ( ":" type ) ":=" term ")"
+| "(" name ":" type "|" term ")"
+| "{" LIST1 name OPT ( ":" type ) "}"
+| "[" LIST1 name OPT ( ":" type ) "]"
 | "`(" LIST1 typeclass_constraint SEP "," ")"
 | "`{" LIST1 typeclass_constraint SEP "," "}"
+| "`[" LIST1 typeclass_constraint SEP "," "]"
 | "'" pattern0
-| "(" name ":" term "|" term ")"
 ]
 
 typeclass_constraint: [
@@ -359,17 +368,20 @@ subprf: [
 ]
 
 gallina: [
-| thm_token ident_decl LIST0 binder ":" term LIST0 [ "with" ident_decl LIST0 binder ":" term ]
-| assumption_token inline assum_list
-| assumptions_token inline assum_list
-| def_token ident_decl def_body
+| thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ]
+| assumption_token OPT ( "Inline" OPT ( "(" num ")" ) ) [ LIST1 ( "(" assumpt ")" ) | assumpt ]
+| [ "Definition" | "Example" ] ident_decl def_body
 | "Let" ident def_body
-| OPT cumulativity_token private_token finite_token LIST1 inductive_definition SEP "with"
-| "Fixpoint" LIST1 fix_definition SEP "with"
-| "Let" "Fixpoint" LIST1 fix_definition SEP "with"
-| "CoFixpoint" LIST1 cofix_definition SEP "with"
-| "Let" "CoFixpoint" LIST1 cofix_definition SEP "with"
-| "Scheme" LIST1 scheme SEP "with"
+| "Inductive" inductive_definition LIST0 ( "with" inductive_definition )
+| "CoInductive" inductive_definition LIST0 ( "with" inductive_definition )
+| "Variant" inductive_definition LIST0 ( "with" inductive_definition )
+| [ "Record" | "Structure" ] inductive_definition LIST0 ( "with" inductive_definition )
+| "Class" inductive_definition LIST0 ( "with" inductive_definition )
+| "Fixpoint" fix_definition LIST0 ( "with" fix_definition )
+| "Let" "Fixpoint" fix_definition LIST0 ( "with" fix_definition )
+| "CoFixpoint" cofix_definition LIST0 ( "with" cofix_definition )
+| "Let" "CoFixpoint" cofix_definition LIST0 ( "with" cofix_definition )
+| "Scheme" scheme LIST0 ( "with" scheme )
 | "Combined" "Scheme" ident "from" LIST1 ident SEP ","
 | "Register" qualid "as" qualid
 | "Register" "Inline" qualid
@@ -380,7 +392,15 @@ gallina: [
 ]
 
 fix_definition: [
-| ident_decl LIST0 binder OPT fixannot OPT ( ":" term ) OPT [ ":=" term ] decl_notation
+| ident_decl LIST0 binder OPT fixannot OPT ( ":" type ) OPT [ ":=" term ] OPT decl_notations
+]
+
+decl_notations: [
+| "where" decl_notation LIST0 ( "and" decl_notation )
+]
+
+decl_notation: [
+| string ":=" term1_extended OPT [ ":" ident ]
 ]
 
 register_token: [
@@ -444,80 +464,23 @@ thm_token: [
 | "Property"
 ]
 
-def_token: [
-| "Definition"
-| "Example"
-| "SubClass"
-]
-
-assumption_token: [
-| "Hypothesis"
-| "Variable"
-| "Axiom"
-| "Parameter"
-| "Conjecture"
-]
-
-assumptions_token: [
-| "Hypotheses"
-| "Variables"
-| "Axioms"
-| "Parameters"
-| "Conjectures"
-]
-
-inline: [
-| "Inline" "(" num ")"
-| "Inline"
-|
-]
-
-univ_constraint: [
-| universe_name [ "<" | "=" | "<=" ] universe_name
-]
-
-ident_decl: [
-| ident OPT ( "@{" LIST0 ident [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | "|}" ] ] )
-]
-
-finite_token: [
-| "Inductive"
-| "CoInductive"
-| "Variant"
-| "Record"
-| "Structure"
-| "Class"
-]
-
-cumulativity_token: [
-| "Cumulative"
-| "NonCumulative"
-]
-
-private_token: [
-| "Private"
-|
-]
-
 def_body: [
-| LIST0 binder ":=" reduce term
-| LIST0 binder ":" term ":=" reduce term
-| LIST0 binder ":" term
+| LIST0 binder OPT ( ":" type ) ":=" OPT reduce term
+| LIST0 binder ":" type
 ]
 
 reduce: [
 | "Eval" red_expr "in"
-|
 ]
 
 red_expr: [
 | "red"
 | "hnf"
-| "simpl" delta_flag OPT ref_or_pattern_occ
-| "cbv" strategy_flag
-| "cbn" strategy_flag
-| "lazy" strategy_flag
-| "compute" delta_flag
+| "simpl" OPT delta_flag OPT ref_or_pattern_occ
+| "cbv" OPT strategy_flag
+| "cbn" OPT strategy_flag
+| "lazy" OPT strategy_flag
+| "compute" OPT delta_flag
 | "vm_compute" OPT ref_or_pattern_occ
 | "native_compute" OPT ref_or_pattern_occ
 | "unfold" LIST1 unfold_occ SEP ","
@@ -526,6 +489,19 @@ red_expr: [
 | ident
 ]
 
+delta_flag: [
+| OPT "-" "[" LIST1 smart_global "]"
+]
+
+smart_global: [
+| qualid
+| by_notation
+]
+
+by_notation: [
+| string OPT [ "%" ident ]
+]
+
 strategy_flag: [
 | LIST1 red_flags
 | delta_flag
@@ -538,70 +514,71 @@ red_flags: [
 | "fix"
 | "cofix"
 | "zeta"
-| "delta" delta_flag
+| "delta" OPT delta_flag
 ]
 
-delta_flag: [
-| "-" "[" LIST1 smart_global "]"
-| "[" LIST1 smart_global "]"
-|
+ref_or_pattern_occ: [
+| smart_global OPT ( "at" occs_nums )
+| term1_extended OPT ( "at" occs_nums )
 ]
 
-ref_or_pattern_occ: [
-| smart_global occs
-| term1_extended occs
+occs_nums: [
+| LIST1 num_or_var
+| "-" num_or_var LIST0 int_or_var
 ]
 
-unfold_occ: [
-| smart_global occs
+num_or_var: [
+| num
+| ident
 ]
 
-opt_constructors_or_fields: [
-| ":=" constructor_list_or_record_decl
-|
+int_or_var: [
+| int
+| ident
 ]
 
-inductive_definition: [
-| opt_coercion ident_decl LIST0 binder OPT [ ":" term ] opt_constructors_or_fields decl_notation
+unfold_occ: [
+| smart_global OPT ( "at" occs_nums )
 ]
 
-opt_coercion: [
-| ">"
-|
+pattern_occ: [
+| term1_extended OPT ( "at" occs_nums )
 ]
 
-constructor_list_or_record_decl: [
-| "|" LIST1 constructor SEP "|"
-| ident constructor_type "|" LIST0 constructor SEP "|"
-| ident constructor_type
-| ident "{" record_fields "}"
-| "{" record_fields "}"
-|
+finite_token: [
+| "Inductive"
+| "CoInductive"
+| "Variant"
+| "Record"
+| "Structure"
+| "Class"
 ]
 
-assum_list: [
-| LIST1 assum_coe
-| simple_assum_coe
+inductive_definition: [
+| OPT ">" ident_decl LIST0 binder OPT [ "|" LIST0 binder ] OPT [ ":" type ] OPT ( ":=" OPT constructors_or_record ) OPT decl_notations
 ]
 
-assum_coe: [
-| "(" simple_assum_coe ")"
+constructors_or_record: [
+| OPT "|" LIST1 constructor SEP "|"
+| OPT ident "{" LIST1 record_field SEP ";" "}"
 ]
 
-simple_assum_coe: [
-| LIST1 ident_decl of_type_with_opt_coercion term
+constructor: [
+| ident LIST0 binder OPT of_type
 ]
 
-constructor_type: [
-| LIST0 binder [ of_type_with_opt_coercion term | ]
+record_field: [
+| LIST0 ( "#[" LIST0 attr SEP "," "]" ) name OPT field_body OPT [ "|" num ] OPT decl_notations
 ]
 
-constructor: [
-| ident constructor_type
+field_body: [
+| LIST0 binder of_type
+| LIST0 binder of_type ":=" term
+| LIST0 binder ":=" term
 ]
 
 cofix_definition: [
-| ident_decl LIST0 binder OPT ( ":" term ) OPT [ ":=" term ] decl_notation
+| ident_decl LIST0 binder OPT ( ":" type ) OPT [ ":=" term ] OPT decl_notations
 ]
 
 scheme: [
@@ -624,25 +601,16 @@ sort_family: [
 | "Type"
 ]
 
-smart_global: [
-| qualid
-| by_notation
-]
-
-by_notation: [
-| string OPT [ "%" ident ]
-]
-
 gallina_ext: [
-| "Module" export_token ident LIST0 ( "(" export_token LIST1 ident ":" module_type_inl ")" ) of_module_type is_module_expr
-| "Module" "Type" ident LIST0 ( "(" export_token LIST1 ident ":" module_type_inl ")" ) LIST0 ( "<:" module_type_inl ) is_module_type
-| "Declare" "Module" export_token ident LIST0 ( "(" export_token LIST1 ident ":" module_type_inl ")" ) ":" module_type_inl
+| "Module" OPT export_token ident LIST0 module_binder of_module_type OPT is_module_expr
+| "Module" "Type" ident LIST0 module_binder LIST0 ( "<:" module_type_inl ) OPT is_module_type
+| "Declare" "Module" OPT export_token ident LIST0 module_binder ":" module_type_inl
 | "Section" ident
 | "Chapter" ident
 | "End" ident
 | "Collection" ident ":=" section_subset_expr
-| "Require" export_token LIST1 qualid
-| "From" qualid "Require" export_token LIST1 qualid
+| "Require" OPT export_token LIST1 qualid
+| "From" qualid "Require" OPT export_token LIST1 qualid
 | "Import" LIST1 qualid
 | "Export" LIST1 qualid
 | "Include" module_type_inl LIST0 ( "<+" module_expr_inl )
@@ -650,9 +618,9 @@ gallina_ext: [
 | "Transparent" LIST1 smart_global
 | "Opaque" LIST1 smart_global
 | "Strategy" LIST1 [ strategy_level "[" LIST1 smart_global "]" ]
-| "Canonical" OPT "Structure" qualid OPT [ OPT ( "@{" LIST0 ident [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | "|}" ] ] ) def_body ]
+| "Canonical" OPT "Structure" qualid OPT [ OPT univ_decl def_body ]
 | "Canonical" OPT "Structure" by_notation
-| "Coercion" qualid OPT ( "@{" LIST0 ident [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | "|}" ] ] ) def_body
+| "Coercion" qualid OPT univ_decl def_body
 | "Identity" "Coercion" ident ":" class_rawexpr ">->" class_rawexpr
 | "Coercion" qualid ":" class_rawexpr ">->" class_rawexpr
 | "Coercion" by_notation ":" class_rawexpr ">->" class_rawexpr
@@ -661,7 +629,7 @@ gallina_ext: [
 | "Existing" "Instance" qualid hint_info
 | "Existing" "Instances" LIST1 qualid OPT [ "|" num ]
 | "Existing" "Class" qualid
-| "Arguments" smart_global LIST0 argument_spec_block OPT [ "," LIST1 [ LIST0 more_implicits_block ] SEP "," ] OPT [ ":" LIST1 arguments_modifier SEP "," ]
+| "Arguments" smart_global LIST0 argument_spec_block LIST0 [ "," LIST0 more_implicits_block ] OPT [ ":" LIST1 arguments_modifier SEP "," ]
 | "Implicit" "Type" reserv_list
 | "Implicit" "Types" reserv_list
 | "Generalizable" [ "All" "Variables" | "No" "Variables" | [ "Variable" | "Variables" ] LIST1 ident ]
@@ -689,43 +657,41 @@ hint_info: [
 export_token: [
 | "Import"
 | "Export"
-|
 ]
 
-of_module_type: [
-| ":" module_type_inl
-| LIST0 ( "<:" module_type_inl )
+module_binder: [
+| "(" OPT export_token LIST1 ident ":" module_type_inl ")"
 ]
 
-is_module_type: [
-| ":=" module_type_inl LIST0 ( "<+" module_type_inl )
-|
+module_type_inl: [
+| "!" module_type
+| module_type OPT functor_app_annot
 ]
 
-is_module_expr: [
-| ":=" module_expr_inl LIST0 ( "<+" module_expr_inl )
-|
+module_type: [
+| qualid
+| "(" module_type ")"
+| module_type module_expr_atom
+| module_type "with" with_declaration
+]
+
+with_declaration: [
+| "Definition" qualid OPT univ_decl ":=" term
+| "Module" qualid ":=" qualid
 ]
 
 functor_app_annot: [
 | "[" "inline" "at" "level" num "]"
 | "[" "no" "inline" "]"
-|
-]
-
-module_expr_inl: [
-| "!" module_expr
-| module_expr functor_app_annot
 ]
 
-module_type_inl: [
-| "!" module_type
-| module_type functor_app_annot
+of_module_type: [
+| ":" module_type_inl
+| LIST0 ( "<:" module_type_inl )
 ]
 
-module_expr: [
-| module_expr_atom
-| module_expr module_expr_atom
+is_module_type: [
+| ":=" module_type_inl LIST0 ( "<+" module_type_inl )
 ]
 
 module_expr_atom: [
@@ -733,25 +699,31 @@ module_expr_atom: [
 | "(" module_expr ")"
 ]
 
-module_type: [
-| qualid
-| "(" module_type ")"
-| module_type module_expr_atom
-| module_type "with" with_declaration
+module_expr: [
+| module_expr_atom
+| module_expr module_expr_atom
 ]
 
-with_declaration: [
-| "Definition" qualid OPT ( "@{" LIST0 ident [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | "|}" ] ] ) ":=" term
-| "Module" qualid ":=" qualid
+is_module_expr: [
+| ":=" module_expr_inl LIST0 ( "<+" module_expr_inl )
+]
+
+module_expr_inl: [
+| "!" module_expr
+| module_expr OPT functor_app_annot
 ]
 
 argument_spec_block: [
-| OPT "!" name OPT ( "%" ident )
+| argument_spec
 | "/"
 | "&"
-| "(" LIST1 ( OPT "!" name OPT ( "%" ident ) ) ")" OPT ( "%" ident )
-| "[" LIST1 ( OPT "!" name OPT ( "%" ident ) ) "]" OPT ( "%" ident )
-| "{" LIST1 ( OPT "!" name OPT ( "%" ident ) ) "}" OPT ( "%" ident )
+| "(" LIST1 argument_spec ")" OPT ( "%" ident )
+| "[" LIST1 argument_spec "]" OPT ( "%" ident )
+| "{" LIST1 argument_spec "}" OPT ( "%" ident )
+]
+
+argument_spec: [
+| OPT "!" name OPT ( "%" ident )
 ]
 
 more_implicits_block: [
@@ -760,6 +732,20 @@ more_implicits_block: [
 | "{" LIST1 name "}"
 ]
 
+arguments_modifier: [
+| "simpl" "nomatch"
+| "simpl" "never"
+| "default" "implicits"
+| "clear" "bidirectionality" "hint"
+| "clear" "implicits"
+| "clear" "scopes"
+| "clear" "scopes" "and" "implicits"
+| "clear" "implicits" "and" "scopes"
+| "rename"
+| "assert"
+| "extra" "scopes"
+]
+
 strategy_level: [
 | "expand"
 | "opaque"
@@ -785,20 +771,6 @@ simple_reserv: [
 | LIST1 ident ":" term
 ]
 
-arguments_modifier: [
-| "simpl" "nomatch"
-| "simpl" "never"
-| "default" "implicits"
-| "clear" "implicits"
-| "clear" "scopes"
-| "clear" "bidirectionality" "hint"
-| "rename"
-| "assert"
-| "extra" "scopes"
-| "clear" "scopes" "and" "implicits"
-| "clear" "implicits" "and" "scopes"
-]
-
 command: [
 | "Goal" term
 | "Declare" "Scope" ident
@@ -812,7 +784,43 @@ command: [
 | "Add" "Rec" "LoadPath" string as_dirpath
 | "Remove" "LoadPath" string
 | "Type" term
-| "Print" printable
+| "Print" "Term" smart_global OPT ( "@{" LIST0 name "}" )
+| "Print" "All"
+| "Print" "Section" qualid
+| "Print" "Grammar" ident
+| "Print" "Custom" "Grammar" ident
+| "Print" "LoadPath" OPT dirpath
+| "Print" "Modules"
+| "Print" "Libraries"
+| "Print" "ML" "Path"
+| "Print" "ML" "Modules"
+| "Print" "Debug" "GC"
+| "Print" "Graph"
+| "Print" "Classes"
+| "Print" "TypeClasses"
+| "Print" "Instances" smart_global
+| "Print" "Coercions"
+| "Print" "Coercion" "Paths" class_rawexpr class_rawexpr
+| "Print" "Canonical" "Projections" LIST0 smart_global
+| "Print" "Typing" "Flags"
+| "Print" "Tables"
+| "Print" "Options"
+| "Print" "Hint"
+| "Print" "Hint" smart_global
+| "Print" "Hint" "*"
+| "Print" "HintDb" ident
+| "Print" "Scopes"
+| "Print" "Scope" ident
+| "Print" "Visibility" OPT ident
+| "Print" "Implicit" smart_global
+| "Print" OPT "Sorted" "Universes" OPT ( "Subgraph" "(" LIST0 qualid ")" ) OPT string
+| "Print" "Assumptions" smart_global
+| "Print" "Opaque" "Dependencies" smart_global
+| "Print" "Transparent" "Dependencies" smart_global
+| "Print" "All" "Dependencies" smart_global
+| "Print" "Strategy" smart_global
+| "Print" "Strategies"
+| "Print" "Registered"
 | "Print" smart_global OPT ( "@{" LIST0 name "}" )
 | "Print" "Module" "Type" qualid
 | "Print" "Module" qualid
@@ -931,6 +939,7 @@ command: [
 | "Show" "Ltac" "Profile"
 | "Show" "Ltac" "Profile" "CutOff" int
 | "Show" "Ltac" "Profile" string
+| "Show" "Lia" "Profile"      (* micromega plugin *)
 | "Add" "InjTyp" term1_extended      (* micromega plugin *)
 | "Add" "BinOp" term1_extended      (* micromega plugin *)
 | "Add" "UnOp" term1_extended      (* micromega plugin *)
@@ -959,12 +968,12 @@ command: [
 | "Print" "Rewrite" "HintDb" ident
 | "Print" "Ltac" qualid
 | "Locate" "Ltac" qualid
-| "Ltac" LIST1 tacdef_body SEP "with"
+| "Ltac" tacdef_body LIST0 ( "with" tacdef_body )
 | "Print" "Ltac" "Signatures"
 | "Set" "Firstorder" "Solver" ltac_expr
 | "Print" "Firstorder" "Solver"
-| "Function" LIST1 fix_definition SEP "with"      (* funind plugin *)
-| "Functional" "Scheme" LIST1 fun_scheme_arg SEP "with"      (* funind plugin *)
+| "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 *)
@@ -1002,8 +1011,9 @@ command: [
 | "Print" "Rings"      (* setoid_ring plugin *)
 | "Add" "Field" ident ":" term1_extended OPT ( "(" LIST1 field_mod SEP "," ")" )      (* setoid_ring plugin *)
 | "Print" "Fields"      (* setoid_ring plugin *)
-| "Numeral" "Notation" qualid qualid qualid ":" ident numnotoption
+| "Numeral" "Notation" qualid qualid qualid ":" ident OPT numnotoption
 | "String" "Notation" qualid qualid qualid ":" ident
+| "SubClass" ident_decl def_body
 ]
 
 orient: [
@@ -1043,46 +1053,6 @@ starredidentref: [
 | "Type" "*"
 ]
 
-printable: [
-| "Term" smart_global OPT ( "@{" LIST0 name "}" )
-| "All"
-| "Section" qualid
-| "Grammar" ident
-| "Custom" "Grammar" ident
-| "LoadPath" OPT dirpath
-| "Modules"
-| "Libraries"
-| "ML" "Path"
-| "ML" "Modules"
-| "Debug" "GC"
-| "Graph"
-| "Classes"
-| "TypeClasses"
-| "Instances" smart_global
-| "Coercions"
-| "Coercion" "Paths" class_rawexpr class_rawexpr
-| "Canonical" "Projections"
-| "Typing" "Flags"
-| "Tables"
-| "Options"
-| "Hint"
-| "Hint" smart_global
-| "Hint" "*"
-| "HintDb" ident
-| "Scopes"
-| "Scope" ident
-| "Visibility" OPT ident
-| "Implicit" smart_global
-| [ "Sorted" | ] "Universes" OPT ( "Subgraph" "(" LIST0 qualid ")" ) OPT string
-| "Assumptions" smart_global
-| "Opaque" "Dependencies" smart_global
-| "Transparent" "Dependencies" smart_global
-| "All" "Dependencies" smart_global
-| "Strategy" smart_global
-| "Strategies"
-| "Registered"
-]
-
 dirpath: [
 | ident
 | dirpath field_ident
@@ -1160,7 +1130,6 @@ ltac_production_item: [
 ]
 
 numnotoption: [
-|
 | "(" "warning" "after" num ")"
 | "(" "abstract" "after" num ")"
 ]
@@ -1288,17 +1257,12 @@ syntax: [
 | "Delimit" "Scope" ident "with" ident
 | "Undelimit" "Scope" ident
 | "Bind" "Scope" ident "with" LIST1 class_rawexpr
-| "Infix" string ":=" term1_extended [ "(" LIST1 syntax_modifier SEP "," ")" | ] OPT [ ":" ident ]
-| "Notation" ident LIST0 ident ":=" term1_extended only_parsing
-| "Notation" string ":=" term1_extended [ "(" LIST1 syntax_modifier SEP "," ")" | ] OPT [ ":" ident ]
+| "Infix" string ":=" term1_extended OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" ident ]
+| "Notation" ident LIST0 ident ":=" term1_extended OPT ( "(" "only" "parsing" ")" )
+| "Notation" string ":=" term1_extended OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" ident ]
 | "Format" "Notation" string string string
-| "Reserved" "Infix" string [ "(" LIST1 syntax_modifier SEP "," ")" | ]
-| "Reserved" "Notation" string [ "(" LIST1 syntax_modifier SEP "," ")" | ]
-]
-
-only_parsing: [
-| "(" "only" "parsing" ")"
-|
+| "Reserved" "Infix" string OPT [ "(" LIST1 syntax_modifier SEP "," ")" ]
+| "Reserved" "Notation" string OPT [ "(" LIST1 syntax_modifier SEP "," ")" ]
 ]
 
 level: [
@@ -1317,31 +1281,35 @@ syntax_modifier: [
 | "only" "parsing"
 | "format" string OPT string
 | ident "," LIST1 ident SEP "," "at" level
-| ident "at" level
-| ident "at" level constr_as_binder_kind
+| ident "at" level OPT constr_as_binder_kind
 | ident constr_as_binder_kind
 | ident syntax_extension_type
 ]
 
+constr_as_binder_kind: [
+| "as" "ident"
+| "as" "pattern"
+| "as" "strict" "pattern"
+]
+
 syntax_extension_type: [
 | "ident"
 | "global"
 | "bigint"
 | "binder"
 | "constr"
-| "constr" OPT ( "at" level ) OPT constr_as_binder_kind
+| "constr" at_level_opt OPT constr_as_binder_kind
 | "pattern"
 | "pattern" "at" "level" num
 | "strict" "pattern"
 | "strict" "pattern" "at" "level" num
 | "closed" "binder"
-| "custom" ident OPT ( "at" level ) OPT constr_as_binder_kind
+| "custom" ident at_level_opt OPT constr_as_binder_kind
 ]
 
-constr_as_binder_kind: [
-| "as" "ident"
-| "as" "pattern"
-| "as" "strict" "pattern"
+at_level_opt: [
+| "at" level
+|
 ]
 
 simple_tactic: [
@@ -1591,7 +1559,7 @@ simple_tactic: [
 | "eenough" term1_extended as_ipat by_tactic
 | "generalize" term1_extended
 | "generalize" term1_extended LIST1 term1_extended
-| "generalize" term1_extended occs as_name LIST0 [ "," pattern_occ as_name ]
+| "generalize" term1_extended OPT ( "at" occs_nums ) as_name LIST0 [ "," pattern_occ as_name ]
 | "induction" induction_clause_list
 | "einduction" induction_clause_list
 | "destruct" induction_clause_list
@@ -1605,11 +1573,11 @@ simple_tactic: [
 | "inversion" quantified_hypothesis "using" term1_extended in_hyp_list
 | "red" clause_dft_concl
 | "hnf" clause_dft_concl
-| "simpl" delta_flag OPT ref_or_pattern_occ clause_dft_concl
-| "cbv" strategy_flag clause_dft_concl
-| "cbn" strategy_flag clause_dft_concl
-| "lazy" strategy_flag clause_dft_concl
-| "compute" delta_flag clause_dft_concl
+| "simpl" OPT delta_flag OPT ref_or_pattern_occ clause_dft_concl
+| "cbv" OPT strategy_flag clause_dft_concl
+| "cbn" OPT strategy_flag clause_dft_concl
+| "lazy" OPT strategy_flag clause_dft_concl
+| "compute" OPT delta_flag clause_dft_concl
 | "vm_compute" OPT ref_or_pattern_occ clause_dft_concl
 | "native_compute" OPT ref_or_pattern_occ clause_dft_concl
 | "unfold" LIST1 unfold_occ SEP "," clause_dft_concl
@@ -1631,7 +1599,6 @@ simple_tactic: [
 | "functional" "inversion" quantified_hypothesis OPT qualid      (* funind plugin *)
 | "functional" "induction" LIST1 term1_extended fun_ind_using with_names      (* funind plugin *)
 | "soft" "functional" "induction" LIST1 term1_extended fun_ind_using with_names      (* funind plugin *)
-| "myred"      (* micromega plugin *)
 | "psatz_Z" int_or_var ltac_expr      (* micromega plugin *)
 | "psatz_Z" ltac_expr      (* micromega plugin *)
 | "xlia" ltac_expr      (* micromega plugin *)
@@ -1647,24 +1614,18 @@ simple_tactic: [
 | "psatz_R" ltac_expr      (* micromega plugin *)
 | "psatz_Q" int_or_var ltac_expr      (* micromega plugin *)
 | "psatz_Q" ltac_expr      (* micromega plugin *)
-| "iter_specs" ltac_expr      (* micromega plugin *)
+| "zify_iter_specs" ltac_expr      (* micromega plugin *)
 | "zify_op"      (* micromega plugin *)
-| "saturate"      (* micromega plugin *)
+| "zify_saturate"      (* micromega plugin *)
+| "zify_iter_let" ltac_expr      (* micromega plugin *)
 | "nsatz_compute" term1_extended      (* nsatz plugin *)
 | "omega"      (* omega plugin *)
-| "omega" "with" LIST1 ident      (* omega plugin *)
-| "omega" "with" "*"      (* omega plugin *)
 | "protect_fv" string "in" ident      (* setoid_ring plugin *)
 | "protect_fv" string      (* setoid_ring plugin *)
 | "ring_lookup" ltac_expr0 "[" LIST0 term1_extended "]" LIST1 term1_extended      (* setoid_ring plugin *)
 | "field_lookup" ltac_expr "[" LIST0 term1_extended "]" LIST1 term1_extended      (* setoid_ring plugin *)
 ]
 
-int_or_var: [
-| int
-| ident
-]
-
 hloc: [
 |
 | "in" "|-" "*"
@@ -1686,17 +1647,12 @@ by_arg_tac: [
 
 in_clause: [
 | in_clause
-| "*" occs
+| "*" OPT ( "at" occs_nums )
 | "*" "|-" concl_occ
 | LIST0 hypident_occ SEP "," "|-" concl_occ
 | LIST0 hypident_occ SEP ","
 ]
 
-occs: [
-| "at" occs_nums
-|
-]
-
 as_ipat: [
 | "as" simple_intropattern
 |
@@ -1809,10 +1765,6 @@ bindings: [
 | LIST1 term1_extended
 ]
 
-pattern_occ: [
-| term1_extended occs
-]
-
 comparison: [
 | "="
 | "<"
@@ -1838,12 +1790,12 @@ hypident: [
 ]
 
 hypident_occ: [
-| hypident occs
+| hypident OPT ( "at" occs_nums )
 ]
 
 clause_dft_concl: [
 | "in" in_clause
-| occs
+| OPT ( "at" occs_nums )
 |
 ]
 
@@ -1858,18 +1810,8 @@ opt_clause: [
 |
 ]
 
-occs_nums: [
-| LIST1 num_or_var
-| "-" num_or_var LIST0 int_or_var
-]
-
-num_or_var: [
-| num
-| ident
-]
-
 concl_occ: [
-| "*" occs
+| "*" OPT ( "at" occs_nums )
 |
 ]
 
@@ -1987,7 +1929,7 @@ ltac_expr: [
 
 binder_tactic: [
 | "fun" LIST1 fun_var "=>" ltac_expr
-| "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" ltac_expr
+| "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" ltac_expr
 | "info" ltac_expr
 ]
 
@@ -2005,16 +1947,15 @@ let_clause: [
 ltac_expr4: [
 | ltac_expr3 ";" binder_tactic
 | ltac_expr3 ";" ltac_expr3
-| ltac_expr3 ";" "[" multi_goal_tactics "]"
-| ltac_expr3 ";" "[" ">" multi_goal_tactics "]"
+| ltac_expr3 ";" "[" OPT multi_goal_tactics "]"
 | ltac_expr3
+| ltac_expr3 ";" "[" ">" OPT multi_goal_tactics "]"
 ]
 
 multi_goal_tactics: [
 | OPT ltac_expr "|" multi_goal_tactics
 | ltac_expr_opt ".." OPT "|" ltac_expr_opt_list_or
 | ltac_expr
-|
 ]
 
 ltac_expr_opt: [
@@ -2044,6 +1985,20 @@ ltac_expr3: [
 | ltac_expr2
 ]
 
+only_selector: [
+| "only" selector ":"
+]
+
+selector: [
+| LIST1 range_selector SEP ","
+| "[" ident "]"
+]
+
+range_selector: [
+| num "-" num
+| num
+]
+
 ltac_expr2: [
 | ltac_expr1 "+" binder_tactic
 | ltac_expr1 "+" ltac_expr2
@@ -2058,7 +2013,7 @@ ltac_expr1: [
 | "first" "[" LIST0 ltac_expr SEP "|" "]"
 | "solve" "[" LIST0 ltac_expr SEP "|" "]"
 | "idtac" LIST0 message_token
-| failkw [ int_or_var | ] LIST0 message_token
+| failkw OPT int_or_var LIST0 message_token
 | ltac_match_goal
 | simple_tactic
 | tactic_arg
@@ -2099,7 +2054,7 @@ tactic_arg_compat: [
 
 ltac_expr0: [
 | "(" ltac_expr ")"
-| "[>" multi_goal_tactics "]"
+| "[>" OPT multi_goal_tactics "]"
 | tactic_atom
 ]
 
@@ -2115,20 +2070,6 @@ toplevel_selector: [
 | "!" ":"
 ]
 
-only_selector: [
-| "only" selector ":"
-]
-
-selector: [
-| LIST1 range_selector SEP ","
-| "[" ident "]"
-]
-
-range_selector: [
-| num "-" num
-| num
-]
-
 ltac_match_term: [
 | match_key ltac_expr "with" OPT "|" LIST1 match_rule SEP "|" "end"
 ]
diff --git a/doc/tools/docgram/productionlist.edit_mlg b/doc/tools/docgram/productionlist.edit_mlg
index 8170b71e7a..93eb38d1a0 100644
--- a/doc/tools/docgram/productionlist.edit_mlg
+++ b/doc/tools/docgram/productionlist.edit_mlg
@@ -12,19 +12,3 @@
 (* Contents used to generate productionlists in doc *)
 
 DOC_GRAMMAR
-
-(* this is here because they're inside _opt generated by EXPAND *)
-SPLICE: [
-| ltac_info
-| eliminator
-| field_mods
-| ltac_production_sep
-| ltac_tactic_level
-| module_binder
-| printunivs_subgraph
-| quoted_attributes
-| ring_mods
-| scope_delimiter
-| univ_decl
-| univ_name_list
-]