Merge PR #12172: Refactor first chapter: first step, the section on basics.

Ack-by: JasonGross
Ack-by: jfehrle

25 files changed, 833 insertions, 505 deletions

diff --git a/doc/changelog/07-commands-and-options/11665-cumulative-attr.rst b/doc/changelog/07-commands-and-options/11665-cumulative-attr.rst
index b6a034941d..7b690da68d 100644
--- a/doc/changelog/07-commands-and-options/11665-cumulative-attr.rst
+++ b/doc/changelog/07-commands-and-options/11665-cumulative-attr.rst
@@ -6,7 +6,6 @@
   ``Private`` (`#11665 <https://github.com/coq/coq/pull/11665>`_, by
   Théo Zimmermann).
 
-- **Changed:**
-  Legacy attributes can now be passed in any order.  See
-  :ref:`gallina-attributes` (`#11665
-  <https://github.com/coq/coq/pull/11665>`_, by Théo Zimmermann).
+- **Changed:** :term:`Legacy attributes <attribute>` can now be passed
+  in any order (`#11665 <https://github.com/coq/coq/pull/11665>`_, by
+  Théo Zimmermann).
diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index 315c9d4a80..759f630b85 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -529,7 +529,7 @@ pass additional arguments such as ``using relation``.
           setoid_symmetry {? in @ident}
           setoid_transitivity
           setoid_rewrite {? @orientation} @term {? at @occurrences} {? in @ident}
-          setoid_replace @term with @term {? using relation @term} {? in @ident} {? by @tactic}
+          setoid_replace @term with @term {? using relation @term} {? in @ident} {? by @ltac_expr3}
    :name: setoid_reflexivity; setoid_symmetry; setoid_transitivity; setoid_rewrite; setoid_replace
 
    The ``using relation`` arguments cannot be passed to the unprefixed form.
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index 5cffe9e435..52862dea47 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -290,7 +290,7 @@ optional identifier is used when multiple functions have unsolved
 obligations (e.g. when defining mutually recursive blocks). The
 optional tactic is replaced by the default one if not specified.
 
-.. cmd:: {? {| Local | Global } } Obligation Tactic := @tactic
+.. cmd:: {? {| Local | Global } } Obligation Tactic := @ltac_expr
    :name: Obligation Tactic
 
    Sets the default obligation solving tactic applied to all obligations
@@ -314,11 +314,11 @@ optional tactic is replaced by the default one if not specified.
 
    Start the proof of the next unsolved obligation.
 
-.. cmd:: Solve Obligations {? {? of @ident} with @tactic}
+.. cmd:: Solve Obligations {? {? of @ident} with @ltac_expr}
 
    Tries to solve each obligation of ``ident`` using the given ``tactic`` or the default one.
 
-.. cmd:: Solve All Obligations {? with @tactic}
+.. cmd:: Solve All Obligations {? with @ltac_expr}
 
    Tries to solve each obligation of every program using the given
    tactic or the default one (useful for mutually recursive definitions).
diff --git a/doc/sphinx/appendix/indexes/index.rst b/doc/sphinx/appendix/indexes/index.rst
index c8b2cf46dc..7dd0f62a9f 100644
--- a/doc/sphinx/appendix/indexes/index.rst
+++ b/doc/sphinx/appendix/indexes/index.rst
@@ -11,17 +11,17 @@ find what you are looking for.
 
 .. toctree::
 
-   ../../genindex
+   ../../std-glossindex
    ../../coq-cmdindex
    ../../coq-tacindex
+   ../../coq-attrindex
    ../../coq-optindex
    ../../coq-exnindex
-   ../../coq-attrindex
-   ../../std-glossindex
+   ../../genindex
 
 For reference, here are direct links to the documentation of:
 
-- :ref:`flags, options and tables <flags-options-tables>`;
+- :ref:`attributes`
+- :ref:`flags-options-tables`;
 - controlling the display of warning messages with the :opt:`Warnings`
   option;
-- :ref:`gallina-attributes`.
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 88ca0e63d8..453b8597f9 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -1559,7 +1559,7 @@ changes:
 
 - Vernacular:
 
-  - Experimental support for :ref:`attributes <gallina-attributes>` on
+  - Experimental support for :term:`attributes <attribute>` on
     commands, by Vincent Laporte, as in ``#[local] Lemma foo : bar.``
     Tactics and tactic notations now support the ``deprecated``
     attribute.
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index db1340eacb..dbe582df95 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -186,6 +186,7 @@ nitpick_ignore = [ ('token', token) for token in [
     'binders',
     'collection',
     'modpath',
+    'tactic',
 ]]
 
 # -- Options for HTML output ----------------------------------------------
diff --git a/doc/sphinx/coq-attrindex.rst b/doc/sphinx/coq-attrindex.rst
index f2ace20374..a0c8bba90d 100644
--- a/doc/sphinx/coq-attrindex.rst
+++ b/doc/sphinx/coq-attrindex.rst
@@ -1,5 +1,9 @@
 :orphan:
 
+.. hack to get index in TOC
+
+.. _attribute_index:
+
 ---------------
 Attribute index
 ---------------
diff --git a/doc/sphinx/coq-optindex.rst b/doc/sphinx/coq-optindex.rst
index 0961bea61f..e03b2abc32 100644
--- a/doc/sphinx/coq-optindex.rst
+++ b/doc/sphinx/coq-optindex.rst
@@ -2,6 +2,8 @@
 
 .. hack to get index in TOC
 
+.. _options_index:
+
 -------------------------------
 Flags, options and tables index
 -------------------------------
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 09a3897a06..e5af39c8fb 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -24,9 +24,9 @@ to a type and takes the form “*for all x of type* :math:`T`, :math:`P`”. The
 “:math:`x` *of type* :math:`T`” is written “:math:`x:T`”. Informally, “:math:`x:T`” can be thought as
 “:math:`x` *belongs to* :math:`T`”.
 
-The types of types are *sorts*. Types and sorts are themselves terms
+The types of types are called :gdef:`sort`\s. Types and sorts are themselves terms
 so that terms, types and sorts are all components of a common
-syntactic language of terms which is described in Section :ref:`terms` but,
+syntactic language of terms which is described in Section :ref:`terms`.  But
 first, we describe sorts.
 
 
diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst
new file mode 100644
index 0000000000..9473cc5a15
--- /dev/null
+++ b/doc/sphinx/language/core/basic.rst
@@ -0,0 +1,520 @@
+=============================
+Basic notions and conventions
+=============================
+
+This section provides some essential notions and conventions for reading
+the manual.
+
+We start by explaining the syntax and lexical conventions used in the
+manual.  Then, we present the essential vocabulary necessary to read
+the rest of the manual.  Other terms are defined throughout the manual.
+The reader may refer to the :ref:`glossary index <glossary_index>`
+for a complete list of defined terms.  Finally, we describe the various types of
+settings that |Coq| provides.
+
+Syntax and lexical conventions
+------------------------------
+
+Syntax conventions
+~~~~~~~~~~~~~~~~~~
+
+The syntax described in this documentation is equivalent to that
+accepted by the |Coq| parser, but the grammar has been edited
+to improve readability and presentation.
+
+In the grammar presented in this manual, the terminal symbols are
+black (e.g. :n:`forall`), whereas the nonterminals are green, italic
+and hyperlinked (e.g. :n:`@term`).  Some syntax is represented
+graphically using the following kinds of blocks:
+
+:n:`{? item }`
+   An optional item.
+
+:n:`{+ item }`
+   A list of one or more items.
+
+:n:`{* item }`
+   An optional list of items.
+
+:n:`{+s item}`
+   A list of one or more items separated by "s" (e.g. :n:`item__1 s item__2 s item__3`).
+
+:n:`{*s item}`
+   An optional list of items separated by "s".
+
+:n:`{| item__1 | item__2 | ... }`
+   Alternatives (either :n:`item__1` or :n:`item__2` or ...).
+
+`Precedence levels
+<https://en.wikipedia.org/wiki/Order_of_operations>`_ that are
+implemented in the |Coq| parser are shown in the documentation by
+appending the level to the nonterminal name (as in :n:`@term100` or
+:n:`@ltac_expr3`).
+
+.. note::
+
+   |Coq| uses an extensible parser.  Plugins and the :ref:`notation
+   system <syntax-extensions-and-notation-scopes>` can extend the
+   syntax at run time.  Some notations are defined in the prelude,
+   which is loaded by default.  The documented grammar doesn't include
+   these notations.  Precedence levels not used by the base grammar
+   are omitted from the documentation, even though they could still be
+   populated by notations or plugins.
+
+   Furthermore, some parsing rules are only activated in certain
+   contexts (:ref:`interactive proof mode <proofhandling>`,
+   :ref:`custom entries <custom-entries>`...).
+
+.. warning::
+
+   Given the complexity of these parsing rules, it would be extremely
+   difficult to create an external program that can properly parse a
+   |Coq| document.  Therefore, tool writers are advised to delegate
+   parsing to |Coq|, by communicating with it, for instance through
+   `SerAPI <https://github.com/ejgallego/coq-serapi>`_.
+
+.. seealso:: :cmd:`Print Grammar`
+
+.. _lexical-conventions:
+
+Lexical conventions
+~~~~~~~~~~~~~~~~~~~
+
+Blanks
+  Space, newline and horizontal tab are considered blanks.
+  Blanks are ignored but they separate tokens.
+
+Comments
+  Comments are enclosed between ``(*`` and ``*)``.  They can be nested.
+  They can contain any character. However, embedded :n:`@string` literals must be
+  correctly closed. Comments are treated as blanks.
+
+Identifiers
+  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):
+
+  .. insertprodn ident subsequent_letter
+
+  .. prodn::
+     ident ::= @first_letter {* @subsequent_letter }
+     first_letter ::= {| a .. z | A .. Z | _ | @unicode_letter }
+     subsequent_letter ::= {| @first_letter | @digit | ' | @unicode_id_part }
+
+  All characters are meaningful. In particular, identifiers are case-sensitive.
+  :production:`unicode_letter` non-exhaustively includes Latin,
+  Greek, Gothic, Cyrillic, Arabic, Hebrew, Georgian, Hangul, Hiragana
+  and Katakana characters, CJK ideographs, mathematical letter-like
+  symbols and non-breaking space. :production:`unicode_id_part`
+  non-exhaustively includes symbols for prime letters and subscripts.
+
+Numerals
+  Numerals are sequences of digits with an optional fractional part
+  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``.
+
+  .. insertprodn numeral digit
+
+  .. prodn::
+     numeral ::= {+ @digit } {? . {+ @digit } } {? {| e | E } {? {| + | - } } {+ @digit } }
+     int ::= {? - } {+ @digit }
+     num ::= {+ @digit }
+     digit ::= 0 .. 9
+
+Strings
+  Strings begin and end with ``"`` (double quote).  Use ``""`` to represent
+  a double quote character within a string.  In the grammar, strings are
+  identified with :production:`string`.
+
+Keywords
+  The following character sequences are reserved keywords that cannot be
+  used as identifiers::
+
+    _ Axiom CoFixpoint Definition Fixpoint Hypothesis Parameter Prop
+    SProp Set Theorem Type Variable as at cofix discriminated else end
+    fix for forall fun if in let match return then where with
+
+  Note that notations and plugins may define additional keywords.
+
+Other tokens
+  The set of
+  tokens defined at any given time can vary because the :cmd:`Notation`
+  command can define new tokens.  A :cmd:`Require` command may load more notation definitions,
+  while the end of a :cmd:`Section` may remove notations.  Some notations
+  are defined in the standard library (see :ref:`thecoqlibrary`) and are generally
+  loaded automatically at startup time.
+
+  Here are the character sequences that |Coq| directly defines as tokens
+  without using :cmd:`Notation`::
+
+    ! #[ % & ' ( () (bfs) (dfs) ) * ** + , - ->
+    . .( .. ... / : ::= := :> :>> ; < <+ <- <:
+    <<: <= = => > >-> >= ? @ @{ [ [= ] _
+    `( `{ { {| | |- || }
+
+  When multiple tokens match the beginning of a sequence of characters,
+  the longest matching token is used.
+  Occasionally you may need to insert spaces to separate tokens.  For example,
+  if ``~`` and ``~~`` are both defined as tokens, the inputs ``~ ~`` and
+  ``~~`` generate different tokens, whereas if `~~` is not defined, then the
+  two inputs are equivalent.
+
+Essential vocabulary
+--------------------
+
+This section presents the most essential notions to understand the
+rest of the |Coq| manual: :term:`terms <term>` and :term:`types
+<type>` on the one hand, :term:`commands <command>` and :term:`tactics
+<tactic>` on the other hand.
+
+.. glossary::
+
+   term
+
+     Terms are the basic expressions of |Coq|.  Terms can represent
+     mathematical expressions, propositions and proofs, but also
+     executable programs and program types.
+
+     Here is the top-level syntax of terms.  Each of the listed
+     constructs is presented in a dedicated section.  Some of these
+     constructs (like :n:`@term_forall_or_fun`) are part of the core
+     language that the kernel of |Coq| understands and are therefore
+     described in :ref:`this chapter <core-language>`, while
+     others (like :n:`@term_if`) are language extensions that are
+     presented in :ref:`the next chapter <extensions>`.
+
+     .. insertprodn term qualid_annotated
+
+     .. prodn::
+        term ::= @term_forall_or_fun
+        | @term_let
+        | @term_if
+        | @term_fix
+        | @term_cofix
+        | @term100
+        term100 ::= @term_cast
+        | @term10
+        term10 ::= @term_application
+        | @one_term
+        one_term ::= @term_explicit
+        | @term1
+        term1 ::= @term_projection
+        | @term_scope
+        | @term0
+        term0 ::= @qualid_annotated
+        | @sort
+        | @primitive_notations
+        | @term_evar
+        | @term_match
+        | @term_record
+        | @term_generalizing
+        | @term_ltac
+        | ( @term )
+        qualid_annotated ::= @qualid {? @univ_annot }
+
+     .. note::
+
+        Many :term:`commands <command>` and :term:`tactics <tactic>`
+        use :n:`@one_term` (in the syntax of their arguments) rather
+        than :n:`@term`.  The former need to be enclosed in
+        parentheses unless they're very simple, such as a single
+        identifier.  This avoids confusing a space-separated list of
+        terms or identifiers with a :n:`@term_application`.
+
+   type
+
+     To be valid and accepted by the |Coq| kernel, a term needs an
+     associated type.  We express this relationship by “:math:`x` *of
+     type* :math:`T`”, which we write as “:math:`x:T`”.  Informally,
+     “:math:`x:T`” can be thought as “:math:`x` *belongs to*
+     :math:`T`”.
+
+     The |Coq| kernel is a type checker: it verifies that a term has
+     the expected type by applying a set of typing rules (see
+     :ref:`Typing-rules`).  If that's indeed the case, we say that the
+     term is :gdef:`well-typed`.
+
+     A special feature of the |Coq| language is that types can depend
+     on terms (we say that the language is `dependently-typed
+     <https://en.wikipedia.org/wiki/Dependent_type>`_).  Because of
+     this, types and terms share a common syntax.  All types are terms,
+     but not all terms are types:
+
+     .. insertprodn type type
+
+     .. prodn::
+        type ::= @term
+
+     Intuitively, types may be viewed as sets containing terms.  We
+     say that a type is :gdef:`inhabited` if it contains at least one
+     term (i.e. if we can find a term which is associated with this
+     type).  We call such terms :gdef:`witness`\es.  Note that deciding
+     whether a type is inhabited is `undecidable
+     <https://en.wikipedia.org/wiki/Undecidable_problem>`_.
+
+     Formally, types can be used to construct logical foundations for
+     mathematics alternative to the standard `"set theory"
+     <https://en.wikipedia.org/wiki/Set_theory>`_: we call such
+     logical foundations `"type theories"
+     <https://en.wikipedia.org/wiki/Type_theory>`_.  |Coq| is based on
+     the Calculus of Inductive Constructions, which is a particular
+     instance of type theory.
+
+   sentence
+
+     |Coq| documents are made of a series of sentences that contain
+     :term:`commands <command>` or :term:`tactics <tactic>`, generally
+     terminated with a period and optionally decorated with
+     :term:`attributes <attribute>`.
+
+     .. insertprodn document sentence
+
+     .. prodn::
+        document ::= {* @sentence }
+        sentence ::= {? @attributes } @command .
+        | {? @attributes } {? @num : } @query_command .
+        | {? @attributes } {? @toplevel_selector } @ltac_expr {| . | ... }
+        | @control_command
+
+     :n:`@ltac_expr` syntax supports both simple and compound
+     :term:`tactics <tactic>`.  For example: ``split`` is a simple
+     tactic while ``split; auto`` combines two simple tactics.
+
+   command
+
+     A :production:`command` can be used to modify the state of a |Coq|
+     document, for instance by declaring a new object, or to get
+     information about the current state.
+
+     By convention, command names begin with uppercase letters.
+     Commands appear in the HTML documentation in blue or gray boxes
+     after the label "Command".  In the pdf, they appear after the
+     boldface label "Command:".  Commands are listed in the
+     :ref:`command_index`.  Example:
+
+     .. cmd:: Comments {* @string }
+
+        This command prints "Comments ok" and does not change anything
+        to the state of the document.
+
+   tactic
+
+     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, tactic names begin with lowercase letters.  Tactic
+     appear in the HTML documentation in blue or gray boxes after the
+     label "Tactic".  In the pdf, they appear after the boldface label
+     "Tactic:".  Tactics are listed in the :ref:`tactic_index`.
+
+Settings
+--------
+
+There are several mechanisms for changing the behavior of |Coq|.  The
+:term:`attribute` mechanism is used to modify the behavior of a single
+:term:`sentence`.  The :term:`flag`, :term:`option` and :term:`table`
+mechanisms are used to modify the behavior of |Coq| more globally in a
+document or project.
+
+.. _attributes:
+
+Attributes
+~~~~~~~~~~
+
+An :gdef:`attribute` modifies the behavior of a single sentence.
+Syntactically, most commands and tactics can be decorated with
+attributes (cf. :n:`@sentence`), but attributes not supported by the
+command or tactic will trigger :warn:`This command does not support
+this attribute`.
+
+.. insertprodn attributes legacy_attr
+
+.. prodn::
+   attributes ::= {* #[ {*, @attribute } ] } {* @legacy_attr }
+   attribute ::= @ident {? @attr_value }
+   attr_value ::= = @string
+   | ( {*, @attribute } )
+   legacy_attr ::= {| Local | Global }
+   | {| Polymorphic | Monomorphic }
+   | {| Cumulative | NonCumulative }
+   | Private
+   | Program
+
+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_attr`) 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`      :attr:`universes(cumulative)`
+`NonCumulative`   :attr:`universes(noncumulative)`
+`Private`         :attr:`private(matching)`
+`Program`         :attr:`program`
+================  ================================
+
+Attributes appear in the HTML documentation in blue or gray boxes
+after the label "Attribute".  In the pdf, they appear after the
+boldface label "Attribute:".  Attributes are listed in the
+:ref:`attribute_index`.
+
+.. warn:: This command does not support this attribute: @ident.
+   :name: This command does not support this attribute
+
+   This warning is configured to behave as an error by default.  You
+   may turn it into a normal warning by using the :opt:`Warnings` option:
+
+   .. coqtop:: none
+
+      Set Silent.
+
+   .. coqtop:: all warn
+
+      Set Warnings "unsupported-attributes".
+      #[ foo ] Comments.
+
+.. _flags-options-tables:
+
+Flags, Options and Tables
+~~~~~~~~~~~~~~~~~~~~~~~~~
+
+The following types of settings can be used to change the behavior of |Coq| in
+subsequent commands and tactics (see :ref:`set_unset_scope_qualifiers` for a
+more precise description of the scope of these settings):
+
+* A :gdef:`flag` has a boolean value, such as :flag:`Universe Polymorphism`.
+* An :gdef:`option` generally has a numeric or string value, such as :opt:`Firstorder Depth`.
+* A :gdef:`table` contains a set of :token:`string`\s or :token:`qualid`\s.
+* In addition, some commands provide settings, such as :cmd:`Extraction Language`.
+
+.. FIXME Convert "Extraction Language" to an option.
+
+Flags, options and tables are identified by a series of identifiers, each with an initial
+capital letter.
+
+Flags, options and tables appear in the HTML documentation in blue or
+gray boxes after the labels "Flag", "Option" and "Table".  In the pdf,
+they appear after a boldface label.  They are listed in the
+:ref:`options_index`.
+
+.. cmd:: Set @setting_name {? {| @int | @string } }
+   :name: Set
+
+   .. insertprodn setting_name setting_name
+
+   .. prodn::
+      setting_name ::= {+ @ident }
+
+   If :n:`@setting_name` is a flag, no value may be provided; the flag
+   is set to on.
+   If :n:`@setting_name` is an option, a value of the appropriate type
+   must be provided; the option is set to the specified value.
+
+   This command supports the :attr:`local`, :attr:`global` and :attr:`export` attributes.
+   They are described :ref:`here <set_unset_scope_qualifiers>`.
+
+   .. warn:: There is no flag or option with this name: "@setting_name".
+
+      This warning message can be raised by :cmd:`Set` and
+      :cmd:`Unset` when :n:`@setting_name` is unknown.  It is a
+      warning rather than an error because this helps library authors
+      produce |Coq| code that is compatible with several |Coq| versions.
+      To preserve the same behavior, they may need to set some
+      compatibility flags or options that did not exist in previous
+      |Coq| versions.
+
+.. cmd:: Unset @setting_name
+   :name: Unset
+
+   If :n:`@setting_name` is a flag, it is set to off.  If :n:`@setting_name` is an option, it is
+   set to its default value.
+
+   This command supports the :attr:`local`, :attr:`global` and :attr:`export` attributes.
+   They are described :ref:`here <set_unset_scope_qualifiers>`.
+
+.. cmd:: Add @setting_name {+ {| @qualid | @string } }
+
+   Adds the specified values to the table :n:`@setting_name`.
+
+.. cmd:: Remove @setting_name {+ {| @qualid | @string } }
+
+   Removes the specified value from the table :n:`@setting_name`.
+
+.. cmd:: Test @setting_name {? for {+ {| @qualid | @string } } }
+
+   If :n:`@setting_name` is a flag or option, prints its current value.
+   If :n:`@setting_name` is a table: if the `for` clause is specified, reports
+   whether the table contains each specified value, otherwise this is equivalent to
+   :cmd:`Print Table`.  The `for` clause is not valid for flags and options.
+
+   .. exn:: There is no flag, option or table with this name: "@setting_name".
+
+      This error message is raised when calling the :cmd:`Test`
+      command (without the `for` clause), or the :cmd:`Print Table`
+      command, for an unknown :n:`@setting_name`.
+
+   .. exn:: There is no qualid-valued table with this name: "@setting_name".
+            There is no string-valued table with this name: "@setting_name".
+
+      These error messages are raised when calling the :cmd:`Add` or
+      :cmd:`Remove` commands, or the :cmd:`Test` command with the
+      `for` clause, if :n:`@setting_name` is unknown or does not have
+      the right type.
+
+.. cmd:: Print Options
+
+   Prints the current value of all flags and options, and the names of all tables.
+
+.. cmd:: Print Table @setting_name
+
+   Prints the values in the table :n:`@setting_name`.
+
+.. cmd:: Print Tables
+
+   A synonym for :cmd:`Print Options`.
+
+.. _set_unset_scope_qualifiers:
+
+Locality attributes supported by :cmd:`Set` and :cmd:`Unset`
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+The :cmd:`Set` and :cmd:`Unset` commands support the :attr:`local`,
+:attr:`global` and :attr:`export` locality attributes:
+
+* no attribute: the original setting is *not* restored at the end of
+  the current module or section.
+* :attr:`local` (or alternatively, the ``Local`` prefix): the setting
+  is applied within the current module or section.  The original value
+  of the setting is restored at the end of the current module or
+  section.
+* :attr:`export` (or alternatively, the ``Export`` prefix): similar to
+  :attr:`local`, the original value of the setting is restored at the
+  end of the current module or section.  In addition, if the value is
+  set in a module, then :cmd:`Import`\-ing the module sets the option
+  or flag.
+* :attr:`global` (or alternatively, the ``Global`` prefix): the
+  original setting is *not* restored at the end of the current module
+  or section.  In addition, if the value is set in a file, then
+  :cmd:`Require`\-ing the file sets the option.
+
+Newly opened modules and sections inherit the current settings.
+
+.. note::
+
+   We discourage using the :attr:`global` attribute with the :cmd:`Set` and
+   :cmd:`Unset` commands.  If your goal is to define
+   project-wide settings, you should rather use the command-line
+   arguments ``-set`` and ``-unset`` for setting flags and options
+   (cf. :ref:`command-line-options`).
diff --git a/doc/sphinx/language/core/index.rst b/doc/sphinx/language/core/index.rst
index 5ee960d99b..5e83672463 100644
--- a/doc/sphinx/language/core/index.rst
+++ b/doc/sphinx/language/core/index.rst
@@ -6,23 +6,26 @@ Core language
 
 At the heart of the Coq proof assistant is the Coq kernel.  While
 users have access to a language with many convenient features such as
-notations, implicit arguments, etc. (that are presented in the
-:ref:`next chapter <extensions>`), such complex terms get translated
-down to a core language (the Calculus of Inductive Constructions) that
-the kernel understands, and which we present here.  Furthermore, while
-users can build proofs interactively using tactics (see Chapter
+:ref:`notations <syntax-extensions-and-notation-scopes>`,
+:ref:`implicit arguments <ImplicitArguments>`, etc.  (presented in the
+:ref:`next chapter <extensions>`), those features are translated into
+the core language (the Calculus of Inductive Constructions) that the
+kernel understands, which we present here.  Furthermore, while users
+can build proofs interactively using tactics (see Chapter
 :ref:`writing-proofs`), the role of these tactics is to incrementally
 build a "proof term" which the kernel will verify.  More precisely, a
-proof term is a term of the Calculus of Inductive Constructions whose
-type corresponds to a theorem statement.  The kernel is a type checker
-which verifies that terms have their expected type.
+proof term is a :term:`term` of the Calculus of Inductive
+Constructions whose :term:`type` corresponds to a theorem statement.
+The kernel is a type checker which verifies that terms have their
+expected types.
 
-This separation between the kernel on the one hand and the elaboration
-engine and tactics on the other hand follows what is known as the "de
-Bruijn criterion" (keeping a small and well delimited trusted code
+This separation between the kernel on one hand and the
+:ref:`elaboration engine <extensions>` and :ref:`tactics
+<writing-proofs>` on the other follows what is known as the :gdef:`de
+Bruijn criterion` (keeping a small and well delimited trusted code
 base within a proof assistant which can be much more complex).  This
-separation makes it possible to reduce the trust in the whole system
-to trusting a smaller, critical component: the kernel.  In particular,
+separation makes it necessary to trust only a smaller, critical
+component (the kernel) instead of the entire system.  In particular,
 users may rely on external plugins that provide advanced and complex
 tactics without fear of these tactics being buggy, because the kernel
 will have to check their output.
@@ -30,6 +33,7 @@ will have to check their output.
 .. toctree::
    :maxdepth: 1
 
+   basic
    ../gallina-specification-language
    ../cic
    records
diff --git a/doc/sphinx/language/core/records.rst b/doc/sphinx/language/core/records.rst
index 928378f55e..0080f1d052 100644
--- a/doc/sphinx/language/core/records.rst
+++ b/doc/sphinx/language/core/records.rst
@@ -15,14 +15,17 @@ expressions. In this sense, the :cmd:`Record` construction allows defining
 .. cmd:: {| Record | Structure } @record_definition {* with @record_definition }
    :name: Record; Structure
 
-   .. insertprodn record_definition field_body
+   .. insertprodn record_definition field_def
 
    .. prodn::
       record_definition ::= {? > } @ident_decl {* @binder } {? : @type } {? @ident } %{ {*; @record_field } %} {? @decl_notations }
-      record_field ::= {* #[ {*, @attr } ] } @name {? @field_body } {? %| @num } {? @decl_notations }
+      record_field ::= {* #[ {*, @attribute } ] } @name {? @field_body } {? %| @num } {? @decl_notations }
       field_body ::= {* @binder } @of_type
       | {* @binder } @of_type := @term
       | {* @binder } := @term
+      term_record ::= %{%| {* @field_def } %|%}
+      field_def ::= @qualid {* @binder } := @term
+
 
    Each :n:`@record_definition` defines a record named by :n:`@ident_decl`.
    The constructor name is given by :n:`@ident`.
diff --git a/doc/sphinx/language/extensions/implicit-arguments.rst b/doc/sphinx/language/extensions/implicit-arguments.rst
index d93dc00e24..73b1b65097 100644
--- a/doc/sphinx/language/extensions/implicit-arguments.rst
+++ b/doc/sphinx/language/extensions/implicit-arguments.rst
@@ -351,7 +351,7 @@ application. Use the :n:`(@ident := @term)` form of :token:`arg` to do so,
 where :token:`ident` is the name of the implicit argument and :token:`term`
 is its corresponding explicit term. Alternatively, one can deactivate
 the hiding of implicit arguments for a single function application using the
-:n:`@ @qualid {? @univ_annot } {* @term1 }` form of :token:`term10`.
+:n:`@@qualid_annotated {+ @term1 }` form of :token:`term_application`.
 
 .. example:: Syntax for explicitly giving implicit arguments (continued)
 
@@ -420,6 +420,30 @@ but succeeds in
 Deactivation of implicit arguments for parsing
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
+.. insertprodn term_explicit term_explicit
+
+.. prodn::
+   term_explicit ::= @ @qualid_annotated
+
+This syntax can be used to disable implicit arguments for a single
+function.
+
+.. example::
+
+   The function `id` has one implicit argument and one explicit
+   argument.
+
+   .. coqtop:: all reset
+
+      Check (id 0).
+      Definition id' := @id.
+
+   The function `id'` has no implicit argument.
+
+   .. coqtop:: all
+
+      Check (id' nat 0).
+
 .. flag:: Parsing Explicit
 
    Turning this flag on (it is off by default) deactivates the use of implicit arguments.
@@ -429,6 +453,19 @@ Deactivation of implicit arguments for parsing
    to be given as if no arguments were implicit. By symmetry, this also
    affects printing.
 
+.. example::
+
+   We can reproduce the example above using the :flag:`Parsing
+   Explicit` flag:
+
+   .. coqtop:: all reset
+
+      Set Parsing Explicit.
+      Definition id' := id.
+      Unset Parsing Explicit.
+      Check (id 1).
+      Check (id' nat 1).
+
 .. _canonical-structure-declaration:
 
 Canonical structures
@@ -606,7 +643,7 @@ Implicit generalization
 .. index:: `[! ]
 .. index:: `(! )
 
-.. insertprodn generalizing_binder typeclass_constraint
+.. insertprodn generalizing_binder term_generalizing
 
 .. prodn::
    generalizing_binder ::= `( {+, @typeclass_constraint } )
@@ -615,7 +652,8 @@ Implicit generalization
    typeclass_constraint ::= {? ! } @term
    | %{ @name %} : {? ! } @term
    | @name : {? ! } @term
-
+   term_generalizing ::= `%{ @term %}
+   | `( @term )
 
 Implicit generalization is an automatic elaboration of a statement
 with free variables into a closed statement where these variables are
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 51dc169def..5b78280edc 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -30,6 +30,11 @@ under its expanded form (see :flag:`Printing Matching`).
 Pattern-matching on boolean values: the if expression
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
+.. insertprodn term_if term_if
+
+.. prodn::
+   term_if ::= if @term {? {? as @name } return @term100 } then @term else @term
+
 For inductive types with exactly two constructors and for pattern matching
 expressions that do not depend on the arguments of the constructors, it is possible
 to use a ``if … then … else`` notation. For instance, the definition
@@ -852,7 +857,7 @@ Printing constructions in full
 .. flag:: Printing All
 
    Coercions, implicit arguments, the type of pattern matching, but also
-   notations (see :ref:`syntaxextensionsandnotationscopes`) can obfuscate the behavior of some
+   notations (see :ref:`syntax-extensions-and-notation-scopes`) can obfuscate the behavior of some
    tactics (typically the tactics applying to occurrences of subterms are
    sensitive to the implicit arguments). Turning this flag on
    deactivates all high-level printing features such as coercions,
@@ -913,7 +918,8 @@ Existential variables
 .. insertprodn term_evar term_evar
 
 .. prodn::
-   term_evar ::= ?[ @ident ]
+   term_evar ::= _
+   | ?[ @ident ]
    | ?[ ?@ident ]
    | ?@ident {? @%{ {+; @ident := @term } %} }
 
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 186a23897d..353bed1b3d 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -7,197 +7,13 @@
 This chapter describes Gallina, the specification language of Coq. It allows
 developing mathematical theories and to prove specifications of programs. The
 theories are built from axioms, hypotheses, parameters, lemmas, theorems and
-definitions of constants, functions, predicates and sets. The syntax of logical
-objects involved in theories is described in Section :ref:`term`. The
-language of commands, called *The Vernacular* is described in Section
-:ref:`vernacular`.
-
-In Coq, logical objects are typed to ensure their logical correctness.  The
-rules implemented by the typing algorithm are described in Chapter :ref:`calculusofinductiveconstructions`.
-
-
-..  About the grammars in the manual
-    ================================
-
-    Grammars are presented in Backus-Naur form (BNF). Terminal symbols are
-    set in black ``typewriter font``. In addition, there are special notations for
-    regular expressions.
-
-    An expression enclosed in square brackets ``[…]`` means at most one
-    occurrence of this expression (this corresponds to an optional
-    component).
-
-    The notation “``entry sep … sep entry``” stands for a non empty sequence
-    of expressions parsed by entry and separated by the literal “``sep``” [1]_.
-
-    Similarly, the notation “``entry … entry``” stands for a non empty
-    sequence of expressions parsed by the “``entry``” entry, without any
-    separator between.
-
-    At the end, the notation “``[entry sep … sep entry]``” stands for a
-    possibly empty sequence of expressions parsed by the “``entry``” entry,
-    separated by the literal “``sep``”.
-
-.. _lexical-conventions:
-
-Lexical conventions
-===================
-
-Blanks
-  Space, newline and horizontal tab are considered blanks.
-  Blanks are ignored but they separate tokens.
-
-Comments
-  Comments are enclosed between ``(*`` and ``*)``.  They can be nested.
-  They can contain any character. However, embedded :n:`@string` literals must be
-  correctly closed. Comments are treated as blanks.
-
-Identifiers
-  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):
-
-  .. insertprodn ident subsequent_letter
-
-  .. prodn::
-     ident ::= @first_letter {* @subsequent_letter }
-     first_letter ::= {| a .. z | A .. Z | _ | @unicode_letter }
-     subsequent_letter ::= {| @first_letter | @digit | ' | @unicode_id_part }
-
-  All characters are meaningful. In particular, identifiers are case-sensitive.
-  :production:`unicode_letter` non-exhaustively includes Latin,
-  Greek, Gothic, Cyrillic, Arabic, Hebrew, Georgian, Hangul, Hiragana
-  and Katakana characters, CJK ideographs, mathematical letter-like
-  symbols and non-breaking space. :production:`unicode_id_part`
-  non-exhaustively includes symbols for prime letters and subscripts.
-
-Numerals
-  Numerals are sequences of digits with an optional fractional part
-  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``.
-
-  .. insertprodn numeral digit
-
-  .. prodn::
-     numeral ::= {+ @digit } {? . {+ @digit } } {? {| e | E } {? {| + | - } } {+ @digit } }
-     int ::= {? - } {+ @digit }
-     num ::= {+ @digit }
-     digit ::= 0 .. 9
-
-Strings
-  Strings begin and end with ``"`` (double quote).  Use ``""`` to represent
-  a double quote character within a string.  In the grammar, strings are
-  identified with :production:`string`.
-
-Keywords
-  The following character sequences are reserved keywords that cannot be
-  used as identifiers::
-
-    _ Axiom CoFixpoint Definition Fixpoint Hypothesis IF Parameter Prop
-    SProp Set Theorem Type Variable as at by cofix discriminated else
-    end exists exists2 fix for forall fun if in lazymatch let match
-    multimatch return then using where with
-
-  Note that plugins may define additional keywords when they are loaded.
-
-Other tokens
-  The set of
-  tokens defined at any given time can vary because the :cmd:`Notation`
-  command can define new tokens.  A :cmd:`Require` command may load more notation definitions,
-  while the end of a :cmd:`Section` may remove notations.  Some notations
-  are defined in the basic library (see :ref:`thecoqlibrary`) and are normally
-  loaded automatically at startup time.
-
-  Here are the character sequences that Coq directly defines as tokens
-  without using :cmd:`Notation` (omitting 25 specialized tokens that begin with
-  ``#int63_``)::
-
-    ! #[ % & ' ( () (bfs) (dfs) ) * ** + , - ->
-    . .( .. ... / : ::= := :> :>> ; < <+ <- <:
-    <<: <= = => > >-> >= ? @ @{ [ [= ] _
-    `( `{ { {| | |- || }
-
-  When multiple tokens match the beginning of a sequence of characters,
-  the longest matching token is used.
-  Occasionally you may need to insert spaces to separate tokens.  For example,
-  if ``~`` and ``~~`` are both defined as tokens, the inputs ``~ ~`` and
-  ``~~`` generate different tokens, whereas if `~~` is not defined, then the
-  two inputs are equivalent.
+definitions of constants, functions, predicates and sets.
 
 .. _term:
 
 Terms
 =====
 
-Syntax of terms
----------------
-
-The following grammars describe the basic syntax of the terms of the
-*Calculus of Inductive Constructions* (also called Cic). The formal
-presentation of Cic is given in Chapter :ref:`calculusofinductiveconstructions`. Extensions of this syntax
-are given in Chapter :ref:`extensionsofgallina`. How to customize the syntax
-is described in Chapter :ref:`syntaxextensionsandnotationscopes`.
-
-.. insertprodn term field_def
-
-.. prodn::
-   term ::= forall @open_binders , @term
-   | fun @open_binders => @term
-   | @term_let
-   | if @term {? {? as @name } return @term100 } then @term else @term
-   | @term_fix
-   | @term_cofix
-   | @term100
-   term100 ::= @term_cast
-   | @term10
-   term10 ::= @term1 {+ @arg }
-   | @ @qualid {? @univ_annot } {* @term1 }
-   | @term1
-   arg ::= ( @ident := @term )
-   | @term1
-   one_term ::= @term1
-   | @ @qualid {? @univ_annot }
-   term1 ::= @term_projection
-   | @term0 % @scope_key
-   | @term0
-   term0 ::= @qualid {? @univ_annot }
-   | @sort
-   | @numeral
-   | @string
-   | _
-   | @term_evar
-   | @term_match
-   | ( @term )
-   | %{%| {* @field_def } %|%}
-   | `%{ @term %}
-   | `( @term )
-   | ltac : ( @ltac_expr )
-   field_def ::= @qualid {* @binder } := @term
-
-.. note::
-
-   Many commands and tactics use :n:`@one_term` rather than :n:`@term`.
-   The former need to be enclosed in parentheses unless they're very
-   simple, such as a single identifier.  This avoids confusing a space-separated
-   list of terms with a :n:`@term1` applied to a list of arguments.
-
-.. _types:
-
-Types
------
-
-.. 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:
 
 Qualified identifiers and simple identifiers
@@ -223,9 +39,15 @@ Field identifiers, written :n:`@field_ident`, are identifiers prefixed by
 Numerals and strings
 --------------------
 
+.. insertprodn primitive_notations primitive_notations
+
+.. prodn::
+   primitive_notations ::= @numeral
+   | @string
+
 Numerals and strings have no predefined semantics in the calculus. They are
 merely notations that can be bound to objects through the notation mechanism
-(see Chapter :ref:`syntaxextensionsandnotationscopes` for details).
+(see Chapter :ref:`syntax-extensions-and-notation-scopes` for details).
 Initially, numerals are bound to Peano’s representation of natural
 numbers (see :ref:`datatypes`).
 
@@ -352,6 +174,12 @@ Section :ref:`let-in`).
 Products: forall
 ----------------
 
+.. insertprodn term_forall_or_fun term_forall_or_fun
+
+.. prodn::
+   term_forall_or_fun ::= forall @open_binders , @term
+   | fun @open_binders => @term
+
 The expression :n:`forall @ident : @type, @term` denotes the
 *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
@@ -373,6 +201,14 @@ the propositional implication and function types.
 Applications
 ------------
 
+.. insertprodn term_application arg
+
+.. prodn::
+   term_application ::= @term1 {+ @arg }
+   | @ @qualid_annotated {+ @term1 }
+   arg ::= ( @ident := @term )
+   | @term1
+
 :n:`@term__fun @term` denotes applying the function :n:`@term__fun` to :token:`term`.
 
 :n:`@term__fun {+ @term__i }` denotes applying
@@ -634,34 +470,6 @@ co-recursion. It is the local counterpart of the :cmd:`CoFixpoint` command. When
 The Vernacular
 ==============
 
-.. insertprodn vernacular sentence
-
-.. prodn::
-   vernacular ::= {* @sentence }
-   sentence ::= {? @all_attrs } @command .
-   | {? @all_attrs } {? @num : } @query_command .
-   | {? @all_attrs } {? @toplevel_selector } @ltac_expr {| . | ... }
-   | @control_command
-
-The top-level input to |Coq| is a series of :n:`@sentence`\s,
-which are :production:`tactic`\s or :production:`command`\s,
-generally 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:
 
 Assumptions
@@ -697,7 +505,7 @@ has type :n:`@type`.
    of an object of this type) is accepted as a postulate.
 
    :cmd:`Axiom`, :cmd:`Conjecture`, :cmd:`Parameter` and their plural forms
-   are equivalent.  They can take the :attr:`local` attribute (see :ref:`gallina-attributes`),
+   are equivalent.  They can take the :attr:`local` :term:`attribute`,
    which makes the defined :n:`@ident`\s accessible by :cmd:`Import` and its variants
    only through their fully qualified names.
 
@@ -764,7 +572,7 @@ Section :ref:`typing-rules`.
       | {* @binder } : @type
 
    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`),
+   provided that :n:`@term` is well-typed.  They can take the :attr:`local` :term:`attribute`,
    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
@@ -1639,82 +1447,6 @@ the proof and adds it to the environment.
    #. One can also use :cmd:`Admitted` in place of :cmd:`Qed` to turn the
       current asserted statement into an axiom and exit the proof editing mode.
 
-.. _gallina-attributes:
-
-Attributes
------------
-
-.. insertprodn all_attrs legacy_attr
-
-.. prodn::
-   all_attrs ::= {* #[ {*, @attr } ] } {* @legacy_attr }
-   attr ::= @ident {? @attr_value }
-   attr_value ::= = @string
-   | ( {*, @attr } )
-   legacy_attr ::= {| Local | Global }
-   | {| Polymorphic | Monomorphic }
-   | {| Cumulative | NonCumulative }
-   | Private
-   | Program
-
-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_attr`) 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`      :attr:`universes(cumulative)`
-`NonCumulative`   :attr:`universes(noncumulative)`
-`Private`         :attr:`private(matching)`
-`Program`         :attr:`program`
-================  ================================
-
-.. 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`.
-
-    It can trigger the following warnings:
-
-    .. warn:: Tactic @qualid is deprecated since @string__since. @string__note.
-              Tactic Notation @qualid is deprecated since @string__since. @string__note.
-              Notation @string is deprecated since @string__since. @string__note.
-
-       :n:`@qualid` or :n:`@string` is the notation, :n:`@string__since` is the version number,
-       :n:`@string__note` is the note (usually explains the replacement).
-
-    .. example::
-
-       .. coqtop:: all reset warn
-
-          #[deprecated(since="8.9.0", note="Use idtac instead.")]
-          Ltac foo := idtac.
-
-          Goal True.
-          Proof.
-          now foo.
-          Abort.
-
-.. warn:: Unsupported attribute
-
-   This warning is an error by default. It is caused by using a
-   command with some attribute it does not understand.
-
 .. [1]
    Except if the inductive type is empty in which case there is no
    equation that can be used to infer the return type.
diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst
index 4e8a2b0879..42e752841d 100644
--- a/doc/sphinx/practical-tools/coqide.rst
+++ b/doc/sphinx/practical-tools/coqide.rst
@@ -206,7 +206,7 @@ Displaying Unicode symbols
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 You just need to define suitable notations as described in the chapter
-:ref:`syntaxextensionsandnotationscopes`. For example, to use the
+:ref:`syntax-extensions-and-notation-scopes`. For example, to use the
 mathematical symbols ∀ and ∃, you may define:
 
 .. coqtop:: in
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index c1eb1f974c..8418e9c73d 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -174,6 +174,14 @@ mode but it can also be used in toplevel definitions as shown below.
    ltac_def         : `ident` [`ident` ... `ident`] := `ltac_expr`
                     : `qualid` [`ident` ... `ident`] ::= `ltac_expr`
 
+Tactics in terms
+~~~~~~~~~~~~~~~~
+
+.. insertprodn term_ltac term_ltac
+
+.. prodn::
+   term_ltac ::= ltac : ( @ltac_expr )
+
 .. _ltac-semantics:
 
 Semantics
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 3d69126b2d..1759264e87 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -56,135 +56,6 @@ Displaying
    .. todo: "A.B" is permitted but unnecessary for modules/sections.
       should the command just take an @ident?
 
-
-.. _flags-options-tables:
-
-Flags, Options and Tables
------------------------------
-
-Coq has many settings to control its behavior.  Setting types include flags, options
-and tables:
-
-* A *flag* has a boolean value, such as :flag:`Asymmetric Patterns`.
-* An *option* generally has a numeric or string value, such as :opt:`Firstorder Depth`.
-* A *table* contains a set of strings or qualids.
-* In addition, some commands provide settings, such as :cmd:`Extraction Language`.
-
-.. FIXME Convert "Extraction Language" to an option.
-
-Flags, options and tables are identified by a series of identifiers, each with an initial
-capital letter.
-
-.. cmd:: Set @setting_name {? {| @int | @string } }
-   :name: Set
-
-   .. insertprodn setting_name setting_name
-
-   .. prodn::
-      setting_name ::= {+ @ident }
-
-   If :n:`@setting_name` is a flag, no value may be provided; the flag
-   is set to on.
-   If :n:`@setting_name` is an option, a value of the appropriate type
-   must be provided; the option is set to the specified value.
-
-   This command supports the :attr:`local`, :attr:`global` and :attr:`export` attributes.
-   They are described :ref:`here <set_unset_scope_qualifiers>`.
-
-   .. warn:: There is no flag or option with this name: "@setting_name".
-
-      This warning message can be raised by :cmd:`Set` and
-      :cmd:`Unset` when :n:`@setting_name` is unknown.  It is a
-      warning rather than an error because this helps library authors
-      produce Coq code that is compatible with several Coq versions.
-      To preserve the same behavior, they may need to set some
-      compatibility flags or options that did not exist in previous
-      Coq versions.
-
-.. cmd:: Unset @setting_name
-   :name: Unset
-
-   If :n:`@setting_name` is a flag, it is set to off.  If :n:`@setting_name` is an option, it is
-   set to its default value.
-
-   This command supports the :attr:`local`, :attr:`global` and :attr:`export` attributes.
-   They are described :ref:`here <set_unset_scope_qualifiers>`.
-
-.. cmd:: Add @setting_name {+ {| @qualid | @string } }
-
-   Adds the specified values to the table :n:`@setting_name`.
-
-.. cmd:: Remove @setting_name {+ {| @qualid | @string } }
-
-   Removes the specified value from the table :n:`@setting_name`.
-
-.. cmd:: Test @setting_name {? for {+ {| @qualid | @string } } }
-
-   If :n:`@setting_name` is a flag or option, prints its current value.
-   If :n:`@setting_name` is a table: if the `for` clause is specified, reports
-   whether the table contains each specified value, otherise this is equivalent to
-   :cmd:`Print Table`.  The `for` clause is not valid for flags and options.
-
-   .. exn:: There is no flag, option or table with this name: "@setting_name".
-
-      This error message is raised when calling the :cmd:`Test`
-      command (without the `for` clause), or the :cmd:`Print Table`
-      command, for an unknown :n:`@setting_name`.
-
-   .. exn:: There is no qualid-valued table with this name: "@setting_name".
-            There is no string-valued table with this name: "@setting_name".
-
-      These error messages are raised when calling the :cmd:`Add` or
-      :cmd:`Remove` commands, or the :cmd:`Test` command with the
-      `for` clause, if :n:`@setting_name` is unknown or does not have
-      the right type.
-
-.. cmd:: Print Options
-
-   Prints the current value of all flags and options, and the names of all tables.
-
-.. cmd:: Print Table @setting_name
-
-   Prints the values in the table :n:`@setting_name`.
-
-.. cmd:: Print Tables
-
-   A synonym for :cmd:`Print Options`.
-
-.. _set_unset_scope_qualifiers:
-
-Locality attributes supported by :cmd:`Set` and :cmd:`Unset`
-````````````````````````````````````````````````````````````
-
-The :cmd:`Set` and :cmd:`Unset` commands support the :attr:`local`,
-:attr:`global` and :attr:`export` locality attributes:
-
-* no attribute: the original setting is *not* restored at the end of
-  the current module or section.
-* :attr:`local` (an alternative syntax is to use the ``Local``
-  prefix): the setting is applied within the current module or
-  section.  The original value of the setting is restored at the end
-  of the current module or section.
-* :attr:`export` (an alternative syntax is to use the ``Export``
-  prefix): similar to :attr:`local`, the original value of the setting
-  is restored at the end of the current module or section.  In
-  addition, if the value is set in a module, then :cmd:`Import`\-ing
-  the module sets the option or flag.
-* :attr:`global` (an alternative syntax is to use the ``Global``
-  prefix): the original setting is *not* restored at the end of the
-  current module or section.  In addition, if the value is set in a
-  file, then :cmd:`Require`\-ing the file sets the option.
-
-Newly opened modules and sections inherit the current settings.
-
-.. note::
-
-   The use of the :attr:`global` attribute with the :cmd:`Set` and
-   :cmd:`Unset` commands is discouraged.  If your goal is to define
-   project-wide settings, you should rather use the command-line
-   arguments ``-set`` and ``-unset`` for setting flags and options
-   (cf. :ref:`command-line-options`).
-
 Query commands
 --------------
 
diff --git a/doc/sphinx/std-glossindex.rst b/doc/sphinx/std-glossindex.rst
index 3f085ca737..91e9da20fe 100644
--- a/doc/sphinx/std-glossindex.rst
+++ b/doc/sphinx/std-glossindex.rst
@@ -2,6 +2,8 @@
 
 .. hack to get index in TOC
 
+.. _glossary_index:
+
 --------------
 Glossary index
 --------------
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 93d2439412..d72409e0d9 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1,4 +1,4 @@
-.. _syntaxextensionsandnotationscopes:
+.. _syntax-extensions-and-notation-scopes:
 
 Syntax extensions and notation scopes
 =====================================
@@ -433,9 +433,7 @@ Displaying information about notations
        [ IDENT "try"; SELF
 
    Note that the productions printed by this command are represented in the form used by
-   |Coq|'s parser (coqpp), which differs from how productions are shown in the documentation.  The grammar
-   described in this documentation is equivalent to the grammar of the |Coq| parser, but has been
-   heavily edited to improve readability and presentation.
+   |Coq|'s parser (coqpp), which differs from how productions are shown in the documentation.
 
 .. _locating-notations:
 
@@ -1088,12 +1086,17 @@ ways to change the interpretation of subterms are available.
 Opening a notation scope locally
 ++++++++++++++++++++++++++++++++
 
+.. insertprodn term_scope term_scope
+
+.. prodn::
+   term_scope ::= @term0 % @scope_key
+
 The notation scope stack can be locally extended within
 a :token:`term` with the syntax
-:n:`(@term)%@scope_key` (or simply :n:`@term%@scope_key` for atomic terms).
+:n:`(@term)%@scope_key` (or simply :n:`@term0%@scope_key` for atomic terms).
 
 In this case, :n:`@term` is
-interpreted in the scope stack extended with the scope bound to :token:`ident`.
+interpreted in the scope stack extended with the scope bound to :n:`@scope_key`.
 
 .. cmd:: Delimit Scope @scope_name with @scope_key
 
diff --git a/doc/sphinx/using/libraries/index.rst b/doc/sphinx/using/libraries/index.rst
index ad10869439..0bd3054788 100644
--- a/doc/sphinx/using/libraries/index.rst
+++ b/doc/sphinx/using/libraries/index.rst
@@ -23,3 +23,4 @@ installed with the `opam package manager
    ../../addendum/extraction
    ../../addendum/miscellaneous-extensions
    funind
+   writing
diff --git a/doc/sphinx/using/libraries/writing.rst b/doc/sphinx/using/libraries/writing.rst
new file mode 100644
index 0000000000..801d492acb
--- /dev/null
+++ b/doc/sphinx/using/libraries/writing.rst
@@ -0,0 +1,71 @@
+Writing Coq libraries and plugins
+=================================
+
+This section presents the part of the Coq language that is useful only
+to library and plugin authors.  A tutorial for writing Coq plugins is
+available in the Coq repository in `doc/plugin_tutorial
+<https://github.com/coq/coq/tree/master/doc/plugin_tutorial>`_.
+
+Deprecating library objects or tactics
+--------------------------------------
+
+You may use the following :term:`attribute` to deprecate a notation or
+tactic.  When renaming a definition or theorem, you can introduce a
+deprecated compatibility alias using :cmd:`Notation (abbreviation)`
+(see :ref:`the example below <compatibility-alias>`).
+
+.. 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`.
+
+   It can trigger the following warnings:
+
+   .. warn:: Tactic @qualid is deprecated since @string__since. @string__note.
+             Tactic Notation @qualid is deprecated since @string__since. @string__note.
+             Notation @string is deprecated since @string__since. @string__note.
+
+      :n:`@qualid` or :n:`@string` is the notation,
+      :n:`@string__since` is the version number, :n:`@string__note` is
+      the note (usually explains the replacement).
+
+.. example:: Deprecating a tactic.
+
+   .. coqtop:: all abort warn
+
+      #[deprecated(since="0.9", note="Use idtac instead.")]
+      Ltac foo := idtac.
+      Goal True.
+      Proof.
+      now foo.
+
+.. _compatibility-alias:
+
+.. example:: Introducing a compatibility alias
+
+   Let's say your library initially contained:
+
+   .. coqtop:: in
+
+      Definition foo x := S x.
+
+   and you want to rename `foo` into `bar`, but you want to avoid breaking
+   your users' code without advanced notice.  To do so, replace the previous
+   code by the following:
+
+   .. coqtop:: in reset
+
+      Definition bar x := S x.
+      #[deprecated(since="1.2", note="Use bar instead.")]
+      Notation foo := bar.
+
+   Then, the following code still works, but emits a warning:
+
+   .. coqtop:: all warn
+
+      Check (foo 0).
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 6111eaa160..c7e3ee18ad 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -179,7 +179,10 @@ case_item: [
 ]
 
 binder_constr: [
+| MOVETO term_forall_or_fun "forall" open_binders "," operconstr200
+| MOVETO term_forall_or_fun "fun" open_binders "=>" operconstr200
 | MOVETO term_let "let" name binders let_type_cstr ":=" operconstr200 "in" operconstr200
+| MOVETO term_if "if" operconstr200 as_return_type "then" operconstr200 "else" operconstr200
 | MOVETO term_fix "let" "fix" fix_decl "in" operconstr200
 | MOVETO term_cofix "let" "cofix" cofix_decl "in" operconstr200
 | MOVETO term_let "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" operconstr200 "in" operconstr200
@@ -203,8 +206,10 @@ term_let: [
 ]
 
 atomic_constr: [
-(* @Zimmi48: "string" used only for notations, but keep to be consistent with patterns *)
-(* | DELETE string *)
+| MOVETO qualid_annotated global univ_instance
+| MOVETO primitive_notations NUMERAL
+| MOVETO primitive_notations string
+| MOVETO term_evar "_"
 | REPLACE "?" "[" ident "]"
 | WITH "?[" ident "]"
 | MOVETO term_evar "?[" ident "]"
@@ -243,7 +248,21 @@ operconstr100: [
 | MOVETO term_cast operconstr99 ":>"
 ]
 
+constr: [
+| REPLACE "@" global univ_instance
+| WITH "@" qualid_annotated
+| MOVETO term_explicit "@" qualid_annotated
+]
+
 operconstr10: [
+(* Separate this LIST0 in the nonempty and the empty case *)
+(* The empty case is covered by constr *)
+| REPLACE "@" global univ_instance LIST0 operconstr9
+| WITH "@" qualid_annotated LIST1 operconstr9
+| REPLACE operconstr9
+| WITH constr
+| MOVETO term_application operconstr9 LIST1 appl_arg
+| MOVETO term_application "@" qualid_annotated LIST1 operconstr9
 (* fixme: add in as a prodn somewhere *)
 | MOVETO dangling_pattern_extension_rule "@" pattern_identref LIST1 identref
 | DELETE dangling_pattern_extension_rule
@@ -259,6 +278,7 @@ operconstr1: [
 | WITH    operconstr0 ".(" global LIST0 appl_arg ")" (* huh? *)
 | REPLACE operconstr0 "%" IDENT
 | WITH operconstr0 "%" scope_key
+| MOVETO term_scope operconstr0 "%" scope_key
 | MOVETO term_projection operconstr0 ".(" global LIST0 appl_arg ")"
 | MOVETO term_projection operconstr0 ".(" "@" global LIST0 ( operconstr9 ) ")"
 ]
@@ -268,6 +288,10 @@ operconstr0: [
 | DELETE "{" binder_constr "}"
 | REPLACE "{|" record_declaration bar_cbrace
 | WITH "{|" LIST0 field_def bar_cbrace
+| MOVETO term_record "{|" LIST0 field_def bar_cbrace
+| MOVETO term_generalizing "`{" operconstr200 "}"
+| MOVETO term_generalizing "`(" operconstr200 ")"
+| MOVETO term_ltac "ltac" ":" "(" tactic_expr5 ")"
 ]
 
 fix_decls: [
@@ -1132,7 +1156,7 @@ assumption_token: [
 | WITH [ "Variable" | "Variables" ]
 ]
 
-all_attrs: [
+attributes: [
 | LIST0 ( "#[" LIST0 attribute SEP "," "]" ) LIST0 legacy_attr
 ]
 
@@ -1696,7 +1720,6 @@ RENAME: [
 | univ_instance univ_annot
 | simple_assum_coe assumpt
 | of_type_with_opt_coercion of_type
-| attribute attr
 | attribute_value attr_value
 | constructor_list_or_record_decl constructors_or_record
 | record_binder_body field_body
@@ -1807,12 +1830,12 @@ control_command: [ ]
 query_command: [ ] (* re-add since previously spliced *)
 
 sentence: [
-| OPT all_attrs command "."
-| OPT all_attrs OPT ( num ":" ) query_command "."
-| OPT all_attrs OPT toplevel_selector ltac_expr [ "." | "..." ]
+| OPT attributes command "."
+| OPT attributes OPT ( num ":" ) query_command "."
+| OPT attributes OPT toplevel_selector ltac_expr [ "." | "..." ]
 | control_command
 ]
 
-vernacular: [
+document: [
 | LIST0 sentence
 ]
diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml
index 98f826cd29..6d4c33f7be 100644
--- a/doc/tools/docgram/doc_grammar.ml
+++ b/doc/tools/docgram/doc_grammar.ml
@@ -50,7 +50,7 @@ let default_args = {
   verify = false;
 }
 
-let start_symbols = ["vernacular"]
+let start_symbols = ["document"]
 let tokens = [ "bullet"; "string"; "unicode_id_part"; "unicode_letter" ]
 
 (* translated symbols *)
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 2a30c03dd2..df4e5a22e3 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -15,10 +15,9 @@ ltac_use_default: [
 ]
 
 term: [
-| "forall" open_binders "," term
-| "fun" open_binders "=>" term
+| term_forall_or_fun
 | term_let
-| "if" term OPT [ OPT [ "as" name ] "return" term100 ] "then" term "else" term
+| term_if
 | term_fix
 | term_cofix
 | term100
@@ -30,44 +29,39 @@ term100: [
 ]
 
 term10: [
-| term1 LIST1 arg
-| "@" qualid OPT univ_annot LIST0 term1
-| term1
-]
-
-arg: [
-| "(" ident ":=" term ")"
-| term1
+| term_application
+| one_term
 ]
 
 one_term: [
+| term_explicit
 | term1
-| "@" qualid OPT univ_annot
 ]
 
 term1: [
 | term_projection
-| term0 "%" scope_key
+| term_scope
 | term0
 ]
 
 term0: [
-| qualid OPT univ_annot
+| qualid_annotated
 | sort
-| numeral
-| string
-| "_"
+| primitive_notations
 | term_evar
 | term_match
+| term_record
+| term_generalizing
+| term_ltac
 | "(" term ")"
-| "{|" LIST0 field_def "|}"
-| "`{" term "}"
-| "`(" term ")"
-| "ltac" ":" "(" ltac_expr ")"
 ]
 
-field_def: [
-| qualid LIST0 binder ":=" term
+qualid_annotated: [
+| qualid OPT univ_annot
+]
+
+term_ltac: [
+| "ltac" ":" "(" ltac_expr ")"
 ]
 
 term_projection: [
@@ -75,7 +69,12 @@ term_projection: [
 | term0 ".(" "@" qualid LIST0 ( term1 ) ")"
 ]
 
+term_scope: [
+| term0 "%" scope_key
+]
+
 term_evar: [
+| "_"
 | "?[" ident "]"
 | "?[" "?" ident "]"
 | "?" ident OPT ( "@{" LIST1 ( ident ":=" term ) SEP ";" "}" )
@@ -85,6 +84,25 @@ dangling_pattern_extension_rule: [
 | "@" "?" ident LIST1 ident
 ]
 
+term_application: [
+| term1 LIST1 arg
+| "@" qualid_annotated LIST1 term1
+]
+
+arg: [
+| "(" ident ":=" term ")"
+| term1
+]
+
+term_explicit: [
+| "@" qualid_annotated
+]
+
+primitive_notations: [
+| numeral
+| string
+]
+
 assumption_token: [
 | [ "Axiom" | "Axioms" ]
 | [ "Conjecture" | "Conjectures" ]
@@ -158,14 +176,14 @@ where: [
 | "before" ident
 ]
 
-vernacular: [
+document: [
 | LIST0 sentence
 ]
 
 sentence: [
-| OPT all_attrs command "."
-| OPT all_attrs OPT ( num ":" ) query_command "."
-| OPT all_attrs OPT toplevel_selector ltac_expr [ "." | "..." ]
+| OPT attributes command "."
+| OPT attributes OPT ( num ":" ) query_command "."
+| OPT attributes OPT toplevel_selector ltac_expr [ "." | "..." ]
 | control_command
 ]
 
@@ -178,17 +196,17 @@ query_command: [
 tacticals: [
 ]
 
-all_attrs: [
-| LIST0 ( "#[" LIST0 attr SEP "," "]" ) LIST0 legacy_attr
+attributes: [
+| LIST0 ( "#[" LIST0 attribute SEP "," "]" ) LIST0 legacy_attr
 ]
 
-attr: [
+attribute: [
 | ident OPT attr_value
 ]
 
 attr_value: [
 | "=" string
-| "(" LIST0 attr SEP "," ")"
+| "(" LIST0 attribute SEP "," ")"
 ]
 
 legacy_attr: [
@@ -267,6 +285,10 @@ cofix_body: [
 | ident LIST0 binder OPT ( ":" type ) ":=" term
 ]
 
+term_if: [
+| "if" term OPT [ OPT [ "as" name ] "return" term100 ] "then" term "else" term
+]
+
 term_let: [
 | "let" name OPT ( ":" type ) ":=" term "in" term
 | "let" name LIST1 binder OPT ( ":" type ) ":=" term "in" term
@@ -275,6 +297,11 @@ term_let: [
 | "let" "'" pattern "in" pattern ":=" term "return" term100 "in" term
 ]
 
+term_forall_or_fun: [
+| "forall" open_binders "," term
+| "fun" open_binders "=>" term
+]
+
 open_binders: [
 | LIST1 name ":" term
 | LIST1 binder
@@ -312,6 +339,11 @@ typeclass_constraint: [
 | name ":" OPT "!" term
 ]
 
+term_generalizing: [
+| "`{" term "}"
+| "`(" term ")"
+]
+
 term_cast: [
 | term10 "<:" term
 | term10 "<<:" term
@@ -467,7 +499,7 @@ record_definition: [
 ]
 
 record_field: [
-| LIST0 ( "#[" LIST0 attr SEP "," "]" ) name OPT field_body OPT [ "|" num ] OPT decl_notations
+| LIST0 ( "#[" LIST0 attribute SEP "," "]" ) name OPT field_body OPT [ "|" num ] OPT decl_notations
 ]
 
 field_body: [
@@ -476,6 +508,14 @@ field_body: [
 | LIST0 binder ":=" term
 ]
 
+term_record: [
+| "{|" LIST0 field_def "|}"
+]
+
+field_def: [
+| qualid LIST0 binder ":=" term
+]
+
 inductive_definition: [
 | OPT ">" ident_decl LIST0 binder OPT [ "|" LIST0 binder ] OPT [ ":" type ] OPT ( ":=" OPT constructors_or_record ) OPT decl_notations
 ]