5 files changed, 27 insertions, 24 deletions

diff --git a/doc/sphinx/language/core/records.rst b/doc/sphinx/language/core/records.rst
index d380d83d6c..928378f55e 100644
--- a/doc/sphinx/language/core/records.rst
+++ b/doc/sphinx/language/core/records.rst
@@ -112,13 +112,13 @@ You can override the display format for specified types by adding entries to the
    :name: Printing Record
 
    Specifies a set of qualids which are displayed as records.  Use the
-   :cmd:`Add @table` and :cmd:`Remove @table` commands to update the set of qualids.
+   :cmd:`Add` and :cmd:`Remove` commands to update the set of qualids.
 
 .. table:: Printing Constructor @qualid
    :name: Printing Constructor
 
    Specifies a set of qualids which are displayed as constructors.  Use the
-   :cmd:`Add @table` and :cmd:`Remove @table` commands to update the set of qualids.
+   :cmd:`Add` and :cmd:`Remove` commands to update the set of qualids.
 
 This syntax can also be used for pattern matching.
 
diff --git a/doc/sphinx/language/core/sections.rst b/doc/sphinx/language/core/sections.rst
index 9ad8df2b1b..df50dbafe3 100644
--- a/doc/sphinx/language/core/sections.rst
+++ b/doc/sphinx/language/core/sections.rst
@@ -72,7 +72,7 @@ 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:: Let @ident @def_body
+.. cmd:: Let @ident_decl @def_body
          Let Fixpoint @fix_definition {* with @fix_definition }
          Let CoFixpoint @cofix_definition {* with @cofix_definition }
    :name: Let; Let Fixpoint; Let CoFixpoint
diff --git a/doc/sphinx/language/extensions/implicit-arguments.rst b/doc/sphinx/language/extensions/implicit-arguments.rst
index fb762a00f1..36ce2fdd25 100644
--- a/doc/sphinx/language/extensions/implicit-arguments.rst
+++ b/doc/sphinx/language/extensions/implicit-arguments.rst
@@ -273,14 +273,14 @@ Declaring Implicit Arguments
    .. prodn::
       smart_qualid ::= @qualid
       | @by_notation
-      by_notation ::= @string {? % @ident }
+      by_notation ::= @string {? % @scope }
       argument_spec_block ::= @argument_spec
       | /
       | &
-      | ( {+ @argument_spec } ) {? % @ident }
-      | [ {+ @argument_spec } ] {? % @ident }
-      | %{ {+ @argument_spec } %} {? % @ident }
-      argument_spec ::= {? ! } @name {? % @ident }
+      | ( {+ @argument_spec } ) {? % @scope }
+      | [ {+ @argument_spec } ] {? % @scope }
+      | %{ {+ @argument_spec } %} {? % @scope }
+      argument_spec ::= {? ! } @name {? % @scope }
       more_implicits_block ::= @name
       | [ {+ @name } ]
       | %{ {+ @name } %}
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index a859aa46eb..78b1f02383 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -238,7 +238,7 @@ written using the first destructuring let syntax.
    Note that this only applies to pattern matching instances entered with :g:`match`.
    It doesn't affect pattern matching explicitly entered with a destructuring
    :g:`let`.
-   Use the :cmd:`Add @table` and :cmd:`Remove @table` commands to update this set.
+   Use the :cmd:`Add` and :cmd:`Remove` commands to update this set.
 
 
 Printing matching on booleans
@@ -252,7 +252,7 @@ which types are written this way:
    :name: Printing If
 
    Specifies a set of qualids for which pattern matching is displayed using
-   ``if`` … ``then`` … ``else`` ….  Use the :cmd:`Add @table` and :cmd:`Remove @table`
+   ``if`` … ``then`` … ``else`` ….  Use the :cmd:`Add` and :cmd:`Remove`
    commands to update this set.
 
 This example emphasizes what the printing settings offer.
@@ -719,7 +719,7 @@ accessible, absolute names can never be hidden.
 
        Locate nat.
 
-.. seealso:: Commands :cmd:`Locate` and :cmd:`Locate Library`.
+.. seealso:: Commands :cmd:`Locate`.
 
 .. _libraries-and-filesystem:
 
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index f4592f8f37..ccb236a174 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -161,7 +161,7 @@ is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`.
    one_term ::= @term1
    | @ @qualid {? @univ_annot }
    term1 ::= @term_projection
-   | @term0 % @ident
+   | @term0 % @scope
    | @term0
    term0 ::= @qualid {? @univ_annot }
    | @sort
@@ -373,12 +373,10 @@ the propositional implication and function types.
 Applications
 ------------
 
-The expression :n:`@term__fun @term` denotes the application of
-:n:`@term__fun` (which is expected to have a function type) to
-:token:`term`.
+:n:`@term__fun @term` denotes applying the function :n:`@term__fun` to :token:`term`.
 
-The expression :n:`@term__fun {+ @term__i }` denotes the application
-of the term :n:`@term__fun` to the arguments :n:`@term__i`.  It is
+:n:`@term__fun {+ @term__i }` denotes applying
+:n:`@term__fun` to the arguments :n:`@term__i`.  It is
 equivalent to :n:`( … ( @term__fun @term__1 ) … ) @term__n`:
 associativity is to the left.
 
@@ -458,7 +456,7 @@ Definition by cases: match
    pattern10 ::= @pattern1 as @name
    | @pattern1 {* @pattern1 }
    | @ @qualid {* @pattern1 }
-   pattern1 ::= @pattern0 % @ident
+   pattern1 ::= @pattern0 % @scope
    | @pattern0
    pattern0 ::= @qualid
    | %{%| {* @qualid := @pattern } %|%}
@@ -636,13 +634,18 @@ co-recursion. It is the local counterpart of the :cmd:`CoFixpoint` command. When
 The Vernacular
 ==============
 
-.. insertprodn vernacular vernacular
+.. insertprodn vernacular sentence
 
 .. 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
+   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.
@@ -718,7 +721,7 @@ has type :n:`@type`.
    :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
 
    Warning generated when using :cmd:`Variable` or its equivalent
    instead of :n:`Local Parameter` or its equivalent.