Convert vernac commands chapter to prodn, update syntax

17 files changed, 642 insertions, 703 deletions

diff --git a/Makefile.doc b/Makefile.doc
index 9da175f0e5..effd624cff 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -248,7 +248,7 @@ PLUGIN_MLGS := $(wildcard plugins/*/*.mlg)
 OMITTED_PLUGIN_MLGS := plugins/ssr/ssrparser.mlg plugins/ssr/ssrvernac.mlg plugins/ssrmatching/g_ssrmatching.mlg
 DOC_MLGS := $(wildcard */*.mlg) $(sort $(filter-out $(OMITTED_PLUGIN_MLGS), $(PLUGIN_MLGS)))
 DOC_EDIT_MLGS := $(wildcard doc/tools/docgram/*.edit_mlg)
-DOC_RSTS := $(wildcard doc/sphinx/*/*.rst)
+DOC_RSTS := $(wildcard doc/sphinx/*/*.rst) $(wildcard doc/sphinx/*/*/*.rst)
 
 doc/tools/docgram/fullGrammar: $(DOC_GRAM) $(DOC_MLGS)
 	$(SHOW)'DOC_GRAM'
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index 1f33775a01..cfaa681d20 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -257,7 +257,7 @@ Activating the Printing of Coercions
    :name: Printing Coercion
 
    Specifies a set of qualids for which coercions are always displayed.  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.
 
 .. _coercions-classes-as-records:
 
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/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.
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index aa4b6edd7d..9d57864a07 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -379,7 +379,7 @@ Compiled libraries checker (coqchk)
 ----------------------------------------
 
 The ``coqchk`` command takes a list of library paths as argument, described either
-by their logical name or by their physical filename, hich must end in ``.vo``. The
+by their logical name or by their physical filename, which must end in ``.vo``. The
 corresponding compiled libraries (``.vo`` files) are searched in the path,
 recursively processing the libraries they depend on. The content of all these
 libraries is then type checked. The effect of ``coqchk`` is only to return with
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index d61e5ddce7..921c7bbbf7 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -42,6 +42,8 @@ As of today it is possible to build Coq projects using two tools:
 - coq_makefile, which is distributed by Coq and is based on generating a makefile,
 - Dune, the standard OCaml build tool, which, since version 1.9, supports building Coq libraries.
 
+.. _coq_makefile:
+
 Building a |Coq| project with coq_makefile
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index b2b426ada5..62708b01ed 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -258,6 +258,9 @@ following form:
 Goal selectors
 ~~~~~~~~~~~~~~
 
+.. todo: mention this applies to Print commands and the Info command
+
+
 We can restrict the application of a tactic to a subset of the currently
 focused goals with:
 
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 03eebc32f9..3b5233502d 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -41,8 +41,8 @@ terms are called *proof terms*.
 
 .. _proof-editing-mode:
 
-Switching on/off the proof editing mode
--------------------------------------------
+Entering and leaving proof editing mode
+---------------------------------------
 
 The proof editing mode is entered by asserting a statement, which typically is
 the assertion of a theorem using an assertion command like :cmd:`Theorem`. The
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 19573eee43..6a280b74c2 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -51,6 +51,11 @@ specified, the default selector is used.
      tactic_invocation : `toplevel_selector` : `tactic`.
                        : `tactic`.
 
+.. todo: fully describe selectors.  At the moment, ltac has a fairly complete description
+
+.. todo: mention selectors can be applied to some commands, such as
+   Check, Search, SearchHead, SearchPattern, SearchRewrite.
+
 .. opt:: Default Goal Selector "@toplevel_selector"
    :name: Default Goal Selector
 
@@ -3032,8 +3037,8 @@ following:
 For backward compatibility, the notation :n:`in {+ @ident}` performs
 the conversion in hypotheses :n:`{+ @ident}`.
 
-.. tacn:: cbv {* @flag}
-          lazy {* @flag}
+.. tacn:: {? @strategy_flag }
+          lazy {? @strategy_flag }
    :name: cbv; lazy
 
    These parameterized reduction tactics apply to any goal and perform
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index b22c5286fe..10c172137d 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -6,18 +6,28 @@ Vernacular commands
 .. _displaying:
 
 Displaying
---------------
+----------
 
 
 .. _Print:
 
-.. cmd:: Print @qualid
-   :name: Print
+.. cmd:: Print {? Term } @smart_qualid {? @univ_name_list }
+
+   .. insertprodn univ_name_list univ_name_list
+
+   .. prodn::
+      univ_name_list ::= @%{ {* @name } %}
 
-   This command displays on the screen information about the declared or
-   defined object referred by :n:`@qualid`.
+   Displays definitions of terms, including opaque terms, for the object :n:`@smart_qualid`.
 
-   Error messages:
+   * :n:`Term` - a syntactic marker to allow printing a term
+     that is the same as one of the various :n:`Print` commands.  For example,
+     :cmd:`Print All` is a different command, while :n:`Print Term All` shows
+     information on the object whose name is ":n:`All`".
+
+   * :n:`@univ_name_list` - locally renames the
+     polymorphic universes of :n:`@smart_qualid`.
+     The name `_` means the usual name is printed.
 
    .. exn:: @qualid not a defined object.
       :undocumented:
@@ -29,48 +39,22 @@ Displaying
       :undocumented:
 
 
-   .. cmdv:: Print Term @qualid
-      :name: Print Term
-
-      This is a synonym of :cmd:`Print` :n:`@qualid` when :n:`@qualid`
-      denotes a global constant.
-
-   .. cmdv:: Print {? Term } @qualid\@@name
-
-      This locally renames the polymorphic universes of :n:`@qualid`.
-      An underscore means the usual name is printed.
-
-
-.. cmd:: About @qualid
-   :name: About
-
-   This displays various information about the object
-   denoted by :n:`@qualid`: its kind (module, constant, assumption, inductive,
-   constructor, abbreviation, …), long name, type, implicit arguments and
-   argument scopes. It does not print the body of definitions or proofs.
-
-   .. cmdv:: About @qualid\@@name
-
-      This locally renames the polymorphic universes of :n:`@qualid`.
-      An underscore means the usual name is printed.
-
-
 .. cmd:: Print All
 
    This command displays information about the current state of the
    environment, including sections and modules.
 
-   .. cmdv:: Inspect @num
-      :name: Inspect
+.. cmd:: Inspect @num
 
-      This command displays the :n:`@num` last objects of the
-      current environment, including sections and modules.
+   This command displays the :n:`@num` last objects of the
+   current environment, including sections and modules.
 
-   .. cmdv:: Print Section @ident
+.. cmd:: Print Section @qualid
 
-      The name :n:`@ident` should correspond to a currently open section,
-      this command displays the objects defined since the beginning of this
-      section.
+   Displays the objects defined since the beginning of the section named :n:`@qualid`.
+
+   .. todo: "A.B" is permitted but unnecessary for modules/sections.
+      should the command just take an @ident?
 
 
 .. _flags-options-tables:
@@ -81,9 +65,9 @@ Flags, Options and Tables
 Coq has many settings to control its behavior.  Setting types include flags, options
 and tables:
 
-* A :production:`flag` has a boolean value, such as :flag:`Asymmetric Patterns`.
-* An :production:`option` generally has a numeric or string value, such as :opt:`Firstorder Depth`.
-* A :production:`table` contains a set of strings or qualids.
+* 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.
@@ -91,68 +75,64 @@ and tables:
 Flags, options and tables are identified by a series of identifiers, each with an initial
 capital letter.
 
-.. cmd::  Set @flag
+.. cmd:: Set @setting_name {? {| @int | @string } }
    :name: Set
 
-   Sets :token:`flag` on.
+   .. insertprodn setting_name setting_name
 
-.. cmd:: Unset @flag
-   :name: Unset
+   .. prodn::
+      setting_name ::= {+ @ident }
 
-   Sets :token:`flag` off.
+   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.
 
-.. cmd:: Test @flag
+   This command supports the :attr:`local`, :attr:`global` and :attr:`export` attributes.
+   They are described :ref:`here <set_unset_scope_qualifiers>`.
 
-   Prints the current value of :token:`flag`.
+   .. warn:: There is no option @setting_name.
 
+      This message also appears for unknown flags.
 
-.. cmd:: Set @option {| @num | @string }
-   :name: Set @option
-
-   Sets :token:`option` to the specified value.
-
-.. cmd:: Unset @option
-   :name: Unset @option
-
-   Sets :token:`option` to its default value.
-
-.. cmd:: Test @option
-
-   Prints the current value of :token:`option`.
-
-.. cmd:: Print Options
+.. cmd:: Unset @setting_name
+   :name: Unset
 
-   Prints the current value of all flags and options, and the names of all tables.
+   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 @table {| @string | @qualid }
-   :name: Add @table
+.. cmd:: Add @setting_name {+ {| @qualid | @string } }
 
-   Adds the specified value to :token:`table`.
+   Adds the specified values to the table :n:`@setting_name`.
 
-.. cmd:: Remove @table {| @string | @qualid }
-   :name: Remove @table
+.. cmd:: Remove @setting_name {+ {| @qualid | @string } }
 
-   Removes the specified value from :token:`table`.
+   Removes the specified value from the table :n:`@setting_name`.
 
-.. cmd:: Test @table for {| @string | @qualid }
-   :name: Test @table for
+.. cmd:: Test @setting_name {? for {+ {| @qualid | @string } } }
 
-   Reports whether :token:`table` contains the specified value.
+   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.
 
-.. cmd:: Print Table @table
-   :name: Print Table @table
+.. cmd:: Print Options
 
-   Prints the values in :token:`table`.
+   Prints the current value of all flags and options, and the names of all tables.
 
-.. cmd:: Test @table
+.. cmd:: Print Table @setting_name
 
-   A synonym for :cmd:`Print Table @table`.
+   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`
 ````````````````````````````````````````````````````````````
 
@@ -185,194 +165,128 @@ Newly opened modules and sections inherit the current settings.
    arguments ``-set`` and ``-unset`` for setting flags and options
    (cf. :ref:`command-line-options`).
 
-.. _requests-to-the-environment:
+Query commands
+--------------
 
-Requests to the environment
--------------------------------
+Unlike other commands, :production:`query_command`\s may be prefixed with
+a goal selector (:n:`@num:`) to specify which goal context it applies to.
+If no selector is provided,
+the command applies to the current goal.  If no proof is open, then the command only applies
+to accessible objects.  (see Section :ref:`invocation-of-tactics`).
 
-.. cmd:: Check @term
+.. cmd:: About @smart_qualid {? @univ_name_list }
 
-   This command displays the type of :n:`@term`. When called in proof mode, the
-   term is checked in the local context of the current subgoal.
-
-   .. cmdv:: @selector: Check @term
+   Displays information about the :n:`@smart_qualid` object, which,
+   if a proof is open,  may be a hypothesis of the selected goal,
+   or an accessible theorem, axiom, etc.:
+   its kind (module, constant, assumption, inductive,
+   constructor, abbreviation, …), long name, type, implicit arguments and
+   argument scopes. It does not print the body of definitions or proofs.
 
-      This variant specifies on which subgoal to perform typing
-      (see Section :ref:`invocation-of-tactics`).
+.. cmd:: Check @term
 
+   Displays the type of :n:`@term`. When called in proof mode, the
+   term is checked in the local context of the selected goal.
 
 .. cmd:: Eval @red_expr in @term
 
-   This command performs the specified reduction on :n:`@term`, and displays
-   the resulting term with its type. The term to be reduced may depend on
-   hypothesis introduced in the first subgoal (if a proof is in
-   progress).
+   Performs the specified reduction on :n:`@term` and displays
+   the resulting term with its type. If a proof is open, :n:`@term`
+   may reference hypotheses of the selected goal.
 
    .. seealso:: Section :ref:`performingcomputations`.
 
 
 .. cmd:: Compute @term
 
-   This command performs a call-by-value evaluation of term by using the
-   bytecode-based virtual machine. It is a shortcut for ``Eval vm_compute in``
-   :n:`@term`.
+   Evaluates :n:`@term` using the bytecode-based virtual machine.
+   It is a shortcut for :cmd:`Eval` :n:`vm_compute in @term`.
 
    .. seealso:: Section :ref:`performingcomputations`.
 
+.. cmd:: Search {+ {? - } @search_item } {? {| inside | outside } {+ @qualid } }
 
-.. cmd:: Print Assumptions @qualid
-
-   This commands display all the assumptions (axioms, parameters and
-   variables) a theorem or definition depends on. Especially, it informs
-   on the assumptions with respect to which the validity of a theorem
-   relies.
-
-   .. cmdv:: Print Opaque Dependencies @qualid
-      :name: Print Opaque Dependencies
-
-      Displays the set of opaque constants :n:`@qualid` relies on in addition to
-      the assumptions.
-
-   .. cmdv:: Print Transparent Dependencies @qualid
-      :name: Print Transparent Dependencies
-
-      Displays the set of transparent constants :n:`@qualid` relies on
-      in addition to the assumptions.
-
-   .. cmdv:: Print All Dependencies @qualid
-      :name: Print All Dependencies
-
-      Displays all assumptions and constants :n:`@qualid` relies on.
-
-
-.. cmd:: Search @qualid
-
-   This command displays the name and type of all objects (hypothesis of
-   the current goal, theorems, axioms, etc) of the current context whose
-   statement contains :n:`@qualid`. This command is useful to remind the user
-   of the name of library lemmas.
-
-   .. exn:: The reference @qualid was not found in the current environment.
-
-      There is no constant in the environment named qualid.
-
-   .. cmdv:: Search @string
-
-      If :n:`@string` is a valid identifier, this command
-      displays the name and type of all objects (theorems, axioms, etc) of
-      the current context whose name contains string. If string is a
-      notation’s string denoting some reference :n:`@qualid` (referred to by its
-      main symbol as in `"+"` or by its notation’s string as in `"_ + _"` or
-      `"_ 'U' _"`, see Section :ref:`notations`), the command works like ``Search`` :n:`@qualid`.
-
-   .. cmdv:: Search @string%@ident
-
-      The string string must be a notation or the main
-      symbol of a notation which is then interpreted in the scope bound to
-      the delimiting key :token:`ident` (see Section :ref:`LocalInterpretationRulesForNotations`).
-
-   .. cmdv:: Search @term_pattern
+   .. insertprodn search_item search_item
 
-      This searches for all statements or types of
-      definition that contains a subterm that matches the pattern
-      :token:`term_pattern` (holes of the pattern are either denoted by `_` or by
-      :n:`?@ident` when non linear patterns are expected).
+   .. prodn::
+      search_item ::= @one_term
+      | @string {? % @scope }
 
-   .. cmdv:: Search {+ {? -}@term_pattern_string}
+   Displays the name and type of all hypotheses of the
+   selected goal (if any) and theorems of the current context
+   matching :n:`@search_item`\s.
+   It's useful for finding the names of library lemmas.
 
-      where
-      :n:`@term_pattern_string` is a term_pattern, a string, or a string followed
-      by a scope delimiting key `%key`.  This generalization of ``Search`` searches
-      for all objects whose statement or type contains a subterm matching
-      :n:`@term_pattern` (or :n:`@qualid` if :n:`@string` is the notation for a reference
-      qualid) and whose name contains all string of the request that
-      correspond to valid identifiers. If a term_pattern or a string is
-      prefixed by `-`, the search excludes the objects that mention that
-      term_pattern or that string.
+   * :n:`@one_term` - Search for objects containing a subterm matching the pattern
+     :n:`@one_term` in which holes of the pattern are indicated by `_` or :n:`?@ident`.
+     If the same :n:`?@ident` occurs more than once in the pattern, all occurrences must
+     match the same value.
 
-   .. cmdv:: Search {+ {? -}@term_pattern_string} inside {+ @qualid }
+   * :n:`@string` - If :n:`@string` is a substring of a valid identifier,
+     search for objects whose name contains :n:`@string`. If :n:`@string` is a notation
+     string associated with a :n:`@qualid`, that's equivalent to :cmd:`Search` :n:`@qualid`.
+     For example, specifying `"+"` or `"_ + _"`, which are notations for `Nat.add`, are equivalent
+     to :cmd:`Search` `Nat.add`.
 
-      This restricts the search to constructions defined in the modules
-      named by the given :n:`qualid` sequence.
+   * :n:`% @scope` - limits the search to the scope bound to
+     the delimiting key :n:`@scope`, such as, for example, :n:`%nat`.
+     This clause may be used only if :n:`@string` contains a notation string.
+     (see Section :ref:`LocalInterpretationRulesForNotations`)
 
-   .. cmdv:: Search {+ {? -}@term_pattern_string} outside {+ @qualid }
+   If you specify multiple :n:`@search_item`\s, all the conditions must be satisfied
+   for the object to be displayed.  The minus sign `-` excludes objects that contain
+   the :n:`@search_item`.
 
-      This restricts the search to constructions not defined in the modules
-      named by the given :n:`qualid` sequence.
+   Additional clauses:
 
-   .. cmdv:: @selector: Search {+ {? -}@term_pattern_string}
+   * :n:`inside {+ @qualid }` - limit the search to the specified modules
+   * :n:`outside {+ @qualid }` - exclude the specified modules from the search
 
-      This specifies the goal on which to search hypothesis (see
-      Section :ref:`invocation-of-tactics`).
-      By default the 1st goal is searched. This variant can
-      be combined with other variants presented here.
+   .. exn:: Module/section @qualid not found.
 
-      .. example::
+      There is no constant in the environment named :n:`@qualid`, where :n:`@qualid`
+      is in an `inside` or `outside` clause.
 
-         .. coqtop:: in
+   .. example:: :cmd:`Search` examples
 
-            Require Import ZArith.
+      .. coqtop:: in
 
-         .. coqtop:: all
+         Require Import ZArith.
 
-            Search Z.mul Z.add "distr".
+      .. coqtop:: all
 
-            Search "+"%Z "*"%Z "distr" -positive -Prop.
+         Search Z.mul Z.add "distr".
+         Search "+"%Z "*"%Z "distr" -Prop.
+         Search (?x * _ + ?x * _)%Z outside OmegaLemmas.
 
-            Search (?x * _ + ?x * _)%Z outside OmegaLemmas.
 
+.. cmd:: SearchHead @one_term {? {| inside | outside } {+ @qualid } }
 
-.. cmd:: SearchHead @term
+   Displays the name and type of all hypotheses of the
+   selected goal (if any) and theorems of the current context that have the
+   form :n:`{? forall {* @binder }, } {* P__i -> } C` where :n:`@one_term`
+   matches a prefix of `C`.  For example, a :n:`@one_term` of `f _ b`
+   matches `f a b`, which is a prefix of `C` when `C` is `f a b c`.
 
-   This command displays the name and type of all hypothesis of the
-   current goal (if any) and theorems of the current context whose
-   statement’s conclusion has the form `(term t1 .. tn)`. This command is
-   useful to remind the user of the name of library lemmas.
+   See :cmd:`Search` for an explanation of the `inside`/`outside` clauses.
 
-   .. example::
+   .. example:: :cmd:`SearchHead` examples
 
       .. coqtop:: reset all
 
          SearchHead le.
-
          SearchHead (@eq bool).
 
-   .. cmdv:: SearchHead @term inside {+ @qualid }
-
-      This restricts the search to constructions defined in the modules named
-      by the given :n:`qualid` sequence.
-
-   .. cmdv:: SearchHead @term outside {+ @qualid }
-
-      This restricts the search to constructions not defined in the modules
-      named by the given :n:`qualid` sequence.
-
-   .. exn:: Module/section @qualid not found.
-
-      No module :n:`@qualid` has been required (see Section :ref:`compiled-files`).
-
-   .. cmdv:: @selector: SearchHead @term
-
-      This specifies the goal on which to
-      search hypothesis (see Section :ref:`invocation-of-tactics`).
-      By default the 1st goal is searched. This variant can be combined
-      with other variants presented here.
+.. cmd:: SearchPattern @one_term {? {| inside | outside } {+ @qualid } }
 
-   .. note:: Up to |Coq| version 8.4, ``SearchHead`` was named ``Search``.
+   Displays the name and type of all hypotheses of the
+   selected goal (if any) and theorems of the current context
+   ending with :n:`{? forall {* @binder }, } {* P__i -> } C` that match the pattern
+   :n:`@one_term`.
 
+   See :cmd:`Search` for an explanation of the `inside`/`outside` clauses.
 
-.. cmd:: SearchPattern @term
-
-   This command displays the name and type of all hypothesis of the
-   current goal (if any) and theorems of the current context whose
-   statement’s conclusion or last hypothesis and conclusion matches the
-   expressionterm where holes in the latter are denoted by `_`.
-   It is a variant of :n:`Search @term_pattern` that does not look for subterms
-   but searches for statements whose conclusion has exactly the expected
-   form, or whose statement finishes by the given series of
-   hypothesis/conclusion.
-
-   .. example::
+   .. example:: :cmd:`SearchPattern` examples
 
       .. coqtop:: in
 
@@ -381,123 +295,118 @@ Requests to the environment
       .. coqtop:: all
 
          SearchPattern (_ + _ = _ + _).
-
          SearchPattern (nat -> bool).
-
          SearchPattern (forall l : list _, _ l l).
 
-   Patterns need not be linear: you can express that the same expression
-   must occur in two places by using pattern variables `?ident`.
-
-
-   .. example::
-
       .. coqtop:: all
 
          SearchPattern (?X1 + _ = _ + ?X1).
 
-   .. cmdv:: SearchPattern @term inside {+ @qualid }
+.. cmd:: SearchRewrite @one_term {? {| inside | outside } {+ @qualid } }
 
-      This restricts the search to constructions defined in the modules
-      named by the given :n:`qualid` sequence.
+   Displays the name and type of all hypotheses of the
+   selected goal (if any) and theorems of the current context that have the form
+   :n:`{? forall {* @binder }, } {* P__i -> } LHS = RHS` where :n:`@one_term`
+   matches either `LHS` or `RHS`.
 
-   .. cmdv:: SearchPattern @term outside {+ @qualid }
+   See :cmd:`Search` for an explanation of the `inside`/`outside` clauses.
 
-      This restricts the search to constructions not defined in the modules
-      named by the given :n:`qualid` sequence.
+   .. example:: :cmd:`SearchRewrite` examples
 
-   .. cmdv:: @selector: SearchPattern @term
+      .. coqtop:: in
 
-      This specifies the goal on which to
-      search hypothesis (see Section :ref:`invocation-of-tactics`).
-      By default the 1st goal is
-      searched. This variant can be combined with other variants presented
-      here.
+         Require Import Arith.
 
+      .. coqtop:: all
 
-.. cmd:: SearchRewrite @term
+         SearchRewrite (_ + _ + _).
 
-   This command displays the name and type of all hypothesis of the
-   current goal (if any) and theorems of the current context whose
-   statement’s conclusion is an equality of which one side matches the
-   expression term. Holes in term are denoted by “_”.
+.. table:: Search Blacklist @string
+   :name: Search Blacklist
 
-   .. example::
+   Specifies a set of strings used to exclude lemmas from the results of :cmd:`Search`,
+   :cmd:`SearchHead`, :cmd:`SearchPattern` and :cmd:`SearchRewrite` queries.  A lemma whose
+   fully-qualified name contains any of the strings will be excluded from the
+   search results.  The default blacklisted substrings are ``_subterm``, ``_subproof`` and
+   ``Private_``.
 
-      .. coqtop:: in
+   Use the :cmd:`Add` and :cmd:`Remove` commands to update the set of
+   blacklisted strings.
 
-         Require Import Arith.
 
-      .. coqtop:: all
+.. _requests-to-the-environment:
 
-         SearchRewrite (_ + _ + _).
+Requests to the environment
+-------------------------------
 
-   .. cmdv:: SearchRewrite @term inside {+ @qualid }
+.. cmd:: Print Assumptions @smart_qualid
 
-      This restricts the search to constructions defined in the modules
-      named by the given :n:`qualid` sequence.
+   Displays all the assumptions (axioms, parameters and
+   variables) a theorem or definition depends on.
 
-   .. cmdv:: SearchRewrite @term outside {+ @qualid }
+   The message "Closed under the global context" indicates that the theorem or
+   definition has no dependencies.
 
-      This restricts the search to constructions not defined in the modules
-      named by the given :n:`qualid` sequence.
+.. cmd:: Print Opaque Dependencies @smart_qualid
 
-   .. cmdv:: @selector: SearchRewrite @term
+   Displays the assumptions and opaque constants that :n:`@smart_qualid` depends on.
 
-      This specifies the goal on which to
-      search hypothesis (see Section :ref:`invocation-of-tactics`).
-      By default the 1st goal is
-      searched. This variant can be combined with other variants presented
-      here.
+.. cmd:: Print Transparent Dependencies @smart_qualid
 
-.. note::
+   Displays the assumptions and  transparent constants that :n:`@smart_qualid` depends on.
 
-   .. table:: Search Blacklist @string
-      :name: Search Blacklist
+.. cmd:: Print All Dependencies @smart_qualid
 
-      Specifies a set of strings used to exclude lemmas from the results of :cmd:`Search`,
-      :cmd:`SearchHead`, :cmd:`SearchPattern` and :cmd:`SearchRewrite` queries.  A lemma whose
-      fully-qualified name contains any of the strings will be excluded from the
-      search results.  The default blacklisted substrings are ``_subterm``, ``_subproof`` and
-      ``Private_``.
+   Displays all the assumptions and constants :n:`@smart_qualid` depends on.
 
-      Use the :cmd:`Add @table` and :cmd:`Remove @table` commands to update the set of
-      blacklisted strings.
+.. cmd:: Locate @smart_qualid
 
-.. cmd:: Locate @qualid
+   Displays the full name of objects from |Coq|'s various qualified namespaces such as terms,
+   modules and Ltac.  It also displays notation definitions.
 
-   This command displays the full name of objects whose name is a prefix
-   of the qualified identifier :n:`@qualid`, and consequently the |Coq| module in
-   which they are defined. It searches for objects from the different
-   qualified namespaces of |Coq|: terms, modules, Ltac, etc.
+   If the argument is:
 
-   .. example::
+   * :n:`@qualid` - displays the full name of objects that
+     end with :n:`@qualid`, thereby showing the module they are defined in.
+   * :n:`@string {? "%" @ident }` - displays the definition of a notation.  :n:`@string`
+     can be a single token in the notation such as "`->`" or a pattern that matches the
+     notation.  See :ref:`locating-notations`.
 
-      .. coqtop:: all
+   .. todo somewhere we should list all the qualified namespaces
 
-         Locate nat.
+.. cmd:: Locate Term @smart_qualid
 
-         Locate Datatypes.O.
+   Like :cmd:`Locate`, but limits the search to terms
 
-         Locate Init.Datatypes.O.
+.. cmd:: Locate Module @qualid
 
-         Locate Coq.Init.Datatypes.O.
+   Like :cmd:`Locate`, but limits the search to modules
 
-         Locate I.Dont.Exist.
+.. cmd:: Locate Ltac @qualid
 
-   .. cmdv:: Locate Term @qualid
+   Like :cmd:`Locate`, but limits the search to tactics
 
-      As Locate but restricted to terms.
+.. cmd:: Locate Library @qualid
 
-   .. cmdv:: Locate Module @qualid
+   Displays the full name, status and file system path of the module :n:`@qualid`, whether loaded or not.
+
+.. cmd:: Locate File @string
 
-      As Locate but restricted to modules.
+   Displays the file system path of the file ending with :n:`@string`.
+   Typically, :n:`@string` has a suffix such as ``.cmo`` or ``.vo`` or ``.v`` file, such as :n:`Nat.v`.
 
-   .. cmdv:: Locate Ltac @qualid
+      .. todo: also works for directory names such as "Data" (parent of Nat.v)
+         also "Data/Nat.v" works, but not a substring match
 
-      As Locate but restricted to tactics.
+.. example:: Locate examples
 
-.. seealso:: Section :ref:`locating-notations`
+   .. coqtop:: all
+
+      Locate nat.
+      Locate Datatypes.O.
+      Locate Init.Datatypes.O.
+      Locate Coq.Init.Datatypes.O.
+      Locate I.Dont.Exist.
 
 .. _printing-flags:
 
@@ -522,35 +431,32 @@ Loading files
 |Coq| offers the possibility of loading different parts of a whole
 development stored in separate files. Their contents will be loaded as
 if they were entered from the keyboard. This means that the loaded
-files are ASCII files containing sequences of commands for |Coq|’s
+files are text files containing sequences of commands for |Coq|’s
 toplevel. This kind of file is called a *script* for |Coq|. The standard
 (and default) extension of |Coq|’s script files is .v.
 
 
-.. cmd:: Load @ident
+.. cmd:: Load {? Verbose } {| @string | @ident }
 
-   This command loads the file named :n:`ident`.v, searching successively in
+   Loads a file.  If :n:`@ident` is specified, the command loads a file
+   named :n:`@ident.v`, searching successively in
    each of the directories specified in the *loadpath*. (see Section
    :ref:`libraries-and-filesystem`)
 
-   Files loaded this way cannot leave proofs open, and the ``Load``
-   command cannot be used inside a proof either.
-
-   .. cmdv:: Load @string
+   If :n:`@string` is specified, it must specify a complete filename.
+   `~` and .. abbreviations are
+   allowed as well as shell variables. If no extension is specified, |Coq|
+   will use the default extension ``.v``.
 
-      Loads the file denoted by the string :n:`@string`, where
-      string is any complete filename. Then the `~` and .. abbreviations are
-      allowed as well as shell variables. If no extension is specified, |Coq|
-      will use the default extension ``.v``.
+   Files loaded this way can't leave proofs open, nor can :cmd:`Load`
+   be used inside a proof.
 
-   .. cmdv:: Load Verbose @ident
-             Load Verbose @string
+   We discourage the use of :cmd:`Load`; use :cmd:`Require` instead.
+   :cmd:`Require` loads `.vo` files that were previously
+   compiled from `.v` files.
 
-      Display, while loading,
-      the answers of |Coq| to each command (including tactics) contained in
-      the loaded file.
-
-      .. seealso:: Section :ref:`controlling-display`.
+   :n:`Verbose` displays the |Coq| output for each command and tactic
+   in the loaded file, as if the commands and tactics were entered interactively.
 
    .. exn:: Can’t find file @ident on loadpath.
       :undocumented:
@@ -568,67 +474,50 @@ Compiled files
 
 This section describes the commands used to load compiled files (see
 Chapter :ref:`thecoqcommands` for documentation on how to compile a file). A compiled
-file is a particular case of module called *library file*.
-
-
-.. cmd:: Require @qualid
-
-   This command looks in the loadpath for a file containing module :n:`@qualid`
-   and adds the corresponding module to the environment of |Coq|. As
-   library files have dependencies in other library files, the command
-   :cmd:`Require` :n:`@qualid` recursively requires all library files the module
-   qualid depends on and adds the corresponding modules to the
-   environment of |Coq| too. |Coq| assumes that the compiled files have been
-   produced by a valid |Coq| compiler and their contents are then not
-   replayed nor rechecked.
-
-   To locate the file in the file system, :n:`@qualid` is decomposed under the
-   form :n:`dirpath.@ident` and the file :n:`@ident.vo` is searched in the physical
-   directory of the file system that is mapped in |Coq| loadpath to the
-   logical path dirpath (see Section :ref:`libraries-and-filesystem`). The mapping between
-   physical directories and logical names at the time of requiring the
-   file must be consistent with the mapping used to compile the file. If
-   several files match, one of them is picked in an unspecified fashion.
+file is a particular case of a module called a *library file*.
 
 
-   .. cmdv:: Require Import @qualid
-      :name: Require Import
+.. cmd:: Require {? {| Import | Export } } {+ @qualid }
+   :name: Require; Require Import; Require Export
 
-      This loads and declares the module :n:`@qualid`
-      and its dependencies then imports the contents of :n:`@qualid` as described
-      for :cmd:`Import`. It does not import the modules that
-      :n:`@qualid` depends on unless these modules were themselves required in module
-      :n:`@qualid`
-      using :cmd:`Require Export`, or recursively required
-      through a series of :cmd:`Require Export`.  If the module required has
-      already been loaded, :cmd:`Require Import` :n:`@qualid` simply imports it, as
-      :cmd:`Import` :n:`@qualid` would.
+   Loads compiled modules into the |Coq| environment.  For each :n:`@qualid`, which has the form
+   :n:`{* @ident__prefix . } @ident`, the command searches for the logical name represented
+   by the :n:`@ident__prefix`\s and loads the compiled file :n:`@ident.vo` from the associated
+   filesystem directory.
 
-   .. cmdv:: Require Export @qualid
-      :name: Require Export
+   The process is applied recursively to all the loaded files;
+   if they contain :cmd:`Require` commands, those commands are executed as well.
+   The compiled files must have been compiled with the same version of |Coq|.
+   The compiled files are neither replayed nor rechecked.
 
-      This command acts as :cmd:`Require Import` :n:`@qualid`,
-      but if a further module, say `A`, contains a command :cmd:`Require Export` `B`,
-      then the command :cmd:`Require Import` `A` also imports the module `B.`
+   * :n:`Import` - additionally does an :cmd:`Import` on the loaded module, making components defined
+     in the module available by their short names
+   * :n:`Export` - additionally does an :cmd:`Export` on the loaded module, making components defined
+     in the module available by their short names *and* marking them to be exported by the current
+     module
 
-   .. cmdv:: Require {| Import | Export } {+ @qualid }
+   If the required module has already been loaded, :n:`Import` and :n:`Export` make the command
+   equivalent to :cmd:`Import` or :cmd:`Export`.
+
+   The loadpath must contain the same mapping used to compile the file
+   (see Section :ref:`libraries-and-filesystem`). If
+   several files match, one of them is picked in an unspecified fashion.
+   Therefore, library authors should use a unique name for each module and
+   users are encouraged to use fully-qualified names
+   or the :cmd:`From ... Require` command to load files.
 
-      This loads the
-      modules named by the :token:`qualid` sequence and their recursive
-      dependencies. If
-      ``Import`` or ``Export`` is given, it also imports these modules and
-      all the recursive dependencies that were marked or transitively marked
-      as ``Export``.
 
-   .. cmdv:: From @dirpath Require @qualid
-      :name: From ... Require ...
+   .. todo common user error on dirpaths see https://github.com/coq/coq/pull/11961#discussion_r402852390
 
-      This command acts as :cmd:`Require`, but picks
-      any library whose absolute name is of the form :n:`@dirpath.@dirpath’.@qualid`
-      for some :n:`@dirpath’`. This is useful to ensure that the :token:`qualid` library
-      comes from a given package by making explicit its absolute root.
+   .. cmd:: From @dirpath Require {? {| Import | Export } } {+ @qualid }
+      :name: From ... Require
 
-   .. exn:: Cannot load qualid: no physical path bound to dirpath.
+      Works like :cmd:`Require`, but loads, for each :n:`@qualid`,
+      the library whose fully-qualified name matches :n:`@dirpath.{* @ident . }@qualid`
+      for some :n:`{* @ident . }`. This is useful to ensure that the :n:`@qualid` library
+      comes from a particular package.
+
+   .. exn:: Cannot load @qualid: no physical path bound to @dirpath.
       :undocumented:
 
    .. exn:: Cannot find library foo in loadpath.
@@ -637,7 +526,7 @@ file is a particular case of module called *library file*.
       file foo.vo. Either foo.v exists but is not compiled or foo.vo is in a
       directory which is not in your LoadPath (see Section :ref:`libraries-and-filesystem`).
 
-   .. exn:: Compiled library @ident.vo makes inconsistent assumptions over library qualid.
+   .. exn:: Compiled library @ident.vo makes inconsistent assumptions over library @qualid.
 
       The command tried to load library file :n:`@ident`.vo that
       depends on some specific version of library :n:`@qualid` which is not the
@@ -651,13 +540,13 @@ file is a particular case of module called *library file*.
       |Coq| compiled module, or it was compiled with an incompatible
       version of |Coq|.
 
-   .. exn:: The file :n:`@ident.vo` contains library dirpath and not library dirpath’.
-
-      The library file :n:`@dirpath’` is indirectly required by the
-      ``Require`` command but it is bound in the current loadpath to the
-      file :n:`@ident.vo` which was bound to a different library name :token:`dirpath` at
-      the time it was compiled.
+   .. exn:: The file @ident.vo contains library @qualid__1 and not library @qualid__2.
 
+      The library :n:`@qualid__2` is indirectly required by a :cmd:`Require` or
+      :cmd:`From ... Require` command.  The loadpath maps :n:`@qualid__2` to :n:`@ident.vo`,
+      which was compiled using a loadpath that bound it to :n:`@qualid__1`.  Usually
+      the appropriate solution is to recompile :n:`@ident.v` using the correct loadpath.
+      See :ref:`libraries-and-filesystem`.
 
    .. warn:: Require inside a module is deprecated and strongly discouraged. You can Require a module at toplevel and optionally Import it inside another one.
 
@@ -674,27 +563,22 @@ file is a particular case of module called *library file*.
 
 .. cmd:: Declare ML Module {+ @string }
 
-   This commands loads the OCaml compiled files
-   with names given by the :token:`string` sequence
-   (dynamic link). It is mainly used to load tactics dynamically. The
-   files are searched into the current OCaml loadpath (see the
-   command :cmd:`Add ML Path`).
-   Loading of OCaml files is only possible under the bytecode version of
-   ``coqtop`` (i.e. ``coqtop`` called with option ``-byte``, see chapter
-   :ref:`thecoqcommands`), or when |Coq| has been compiled with a
-   version of OCaml that supports native Dynlink (≥ 3.11).
+   This commands dynamically loads OCaml compiled code from
+   a :n:`.mllib` file.
+   It is used to load plugins dynamically.  The
+   files must be accessible in the current OCaml loadpath (see the
+   command :cmd:`Add ML Path`).  The :n:`.mllib` suffix may be omitted.
 
-   .. cmdv:: Local Declare ML Module {+ @string }
+   This command is reserved for plugin developers, who should provide
+   a .v file containing the command. Users of the plugins will then generally
+   load the .v file.
 
-      This variant is not exported to the modules that import the module
-      where they occur, even if outside a section.
+   This command supports the :attr:`local` attribute.  If present,
+   the listed files are not exported, even if they're outside a section.
 
    .. exn:: File not found on loadpath: @string.
       :undocumented:
 
-   .. exn:: Loading of ML object file forbidden in a native Coq.
-      :undocumented:
-
 
 .. cmd:: Print ML Modules
 
@@ -709,7 +593,7 @@ Loadpath
 ------------
 
 Loadpaths are preferably managed using |Coq| command line options (see
-Section `libraries-and-filesystem`) but there remain vernacular commands to manage them
+Section :ref:`libraries-and-filesystem`) but there remain vernacular commands to manage them
 for practical purposes. Such commands are only meant to be issued in
 the toplevel, and using them in source files is discouraged.
 
@@ -719,22 +603,27 @@ the toplevel, and using them in source files is discouraged.
    This command displays the current working directory.
 
 
-.. cmd:: Cd @string
+.. cmd:: Cd {? @string }
 
-   This command changes the current directory according to :token:`string` which
-   can be any valid path.
+   If :n:`@string` is specified, changes the current directory according to :token:`string` which
+   can be any valid path.  Otherwise, it displays the current directory.
 
-   .. cmdv:: Cd
 
-      Is equivalent to Pwd.
+.. cmd:: Add LoadPath @string as @dirpath
 
+   .. insertprodn dirpath dirpath
 
-.. cmd:: Add LoadPath @string as @dirpath
+   .. prodn::
+      dirpath ::= {* @ident . } @ident
 
    This command is equivalent to the command line option
-   :n:`-Q @string @dirpath`. It adds the physical directory string to the current
-   |Coq| loadpath and maps it to the logical directory dirpath.
+   :n:`-Q @string @dirpath`. It adds a mapping to the loadpath from
+   the logical name :n:`@dirpath` to the file system directory :n:`@string`.
 
+   * :n:`@dirpath` is a prefix of a module name.  The module name hierarchy
+     follows the file system hierarchy.  On Linux, for example, the prefix
+     `A.B.C` maps to the directory :n:`@string/B/C`.  Avoid using spaces after a `.` in the
+     path because the parser will interpret that as the end of a command or tactic.
 
 .. cmd:: Add Rec LoadPath @string as @dirpath
 
@@ -748,42 +637,24 @@ the toplevel, and using them in source files is discouraged.
    This command removes the path :n:`@string` from the current |Coq| loadpath.
 
 
-.. cmd:: Print LoadPath
+.. cmd:: Print LoadPath {? @dirpath }
 
-   This command displays the current |Coq| loadpath.
-
-   .. cmdv:: Print LoadPath @dirpath
-
-      Works as :cmd:`Print LoadPath` but displays only
-      the paths that extend the :n:`@dirpath` prefix.
+   This command displays the current |Coq| loadpath.  If :n:`@dirpath` is specified,
+   displays only the paths that extend that prefix.
 
 
 .. cmd:: Add ML Path @string
 
    This command adds the path :n:`@string` to the current OCaml
-   loadpath (see the command `Declare ML Module`` in Section :ref:`compiled-files`).
+   loadpath (cf. :cmd:`Declare ML Module`).
 
 
-.. cmd:: Print ML Path @string
+.. cmd:: Print ML Path
 
    This command displays the current OCaml loadpath. This
    command makes sense only under the bytecode version of ``coqtop``, i.e.
    using option ``-byte``
-   (see the command Declare ML Module in Section :ref:`compiled-files`).
-
-.. _locate-file:
-
-.. cmd:: Locate File @string
-
-   This command displays the location of file string in the current
-   loadpath. Typically, string is a ``.cmo`` or ``.vo`` or ``.v`` file.
-
-
-.. cmd:: Locate Library @dirpath
-
-   This command gives the status of the |Coq| module dirpath. It tells if
-   the module is loaded and if not searches in the load path for a module
-   of logical name :n:`@dirpath`.
+   (cf. :cmd:`Declare ML Module`).
 
 
 .. _backtracking:
@@ -806,30 +677,22 @@ interactively, they cannot be part of a vernacular file loaded via
    .. exn:: @ident: no such entry.
       :undocumented:
 
-   .. cmdv:: Reset Initial
+.. cmd:: Reset Initial
 
-      Goes back to the initial state, just after the start
-      of the interactive session.
+   Goes back to the initial state, just after the start
+   of the interactive session.
 
 
-.. cmd:: Back
+.. cmd:: Back {? @num }
 
-   This command undoes all the effects of the last vernacular command.
-   Commands read from a vernacular file via a :cmd:`Load` are considered as a
-   single command. Proof management commands are also handled by this
-   command (see Chapter :ref:`proofhandling`). For that, Back may have to undo more than
-   one command in order to reach a state where the proof management
-   information is available. For instance, when the last command is a
-   :cmd:`Qed`, the management information about the closed proof has been
-   discarded. In this case, :cmd:`Back` will then undo all the proof steps up to
-   the statement of this proof.
-
-   .. cmdv:: Back @num
-
-      Undo :n:`@num` vernacular commands. As for Back, some extra
-      commands may be undone in order to reach an adequate state. For
-      instance Back :n:`@num` will not re-enter a closed proof, but rather go just
-      before that proof.
+   Undoes all the effects of the last :n:`@num @sentence`\s.  If
+   :n:`@num` is not specified, the command undoes one sentence.
+   Sentences read from a `.v` file via a :cmd:`Load` are considered a
+   single sentence.  While :cmd:`Back` can undo tactics and commands executed
+   within proof mode, once you exit proof mode, such as with :cmd:`Qed`, all
+   the statements executed within are thereafter considered a single sentence.
+   :cmd:`Back` immediately following :cmd:`Qed` gets you back to the state
+   just after the statement of the proof.
 
    .. exn:: Invalid backtrack.
 
@@ -850,18 +713,17 @@ interactively, they cannot be part of a vernacular file loaded via
 Quitting and debugging
 --------------------------
 
-
 .. cmd:: Quit
 
-   This command permits to quit |Coq|.
+   Causes |Coq| to exit.  Valid only in coqtop.
 
 
 .. cmd:: Drop
 
-   This is used mostly as a debug facility by |Coq|’s implementers and does
-   not concern the casual user. This command permits to leave |Coq|
-   temporarily and enter the OCaml toplevel. The OCaml
-   command:
+   This command temporarily enters the OCaml toplevel.
+   It is a debug facility used by |Coq|’s implementers.  Valid only in the
+   bytecode version of coqtop.
+   The OCaml command:
 
    ::
 
@@ -886,49 +748,53 @@ Quitting and debugging
          (see Section `customization-by-environment-variables`).
 
 
-.. TODO : command is not a syntax entry
-
-.. cmd:: Time @command
+.. cmd:: Time @sentence
 
-   This command executes the vernacular command :n:`@command` and displays the
+   Executes :n:`@sentence` and displays the
    time needed to execute it.
 
 
-.. cmd:: Redirect @string @command
+.. cmd:: Redirect @string @sentence
 
-   This command executes the vernacular command :n:`@command`, redirecting its
-   output to ":n:`@string`.out".
+   Executes :n:`@sentence`, redirecting its
+   output to the file ":n:`@string`.out".
 
 
-.. cmd:: Timeout @num @command
+.. cmd:: Timeout @num @sentence
 
-   This command executes the vernacular command :n:`@command`. If the command
-   has not terminated after the time specified by the :n:`@num` (time
-   expressed in seconds), then it is interrupted and an error message is
+   Executes :n:`@sentence`. If the operation
+   has not terminated after :n:`@num` seconds, then it is interrupted and an error message is
    displayed.
 
    .. opt:: Default Timeout @num
       :name: Default Timeout
 
-      This option controls a default timeout for subsequent commands, as if they
-      were passed to a :cmd:`Timeout` command. Commands already starting by a
-      :cmd:`Timeout` are unaffected.
+      If set, each :n:`@sentence` is treated as if it was prefixed with :cmd:`Timeout` :n:`@num`,
+      except for :cmd:`Timeout` commands themselves.  If unset,
+      no timeout is applied.
 
 
-.. cmd:: Fail @command
+.. cmd:: Fail @sentence
 
    For debugging scripts, sometimes it is desirable to know whether a
-   command or a tactic fails. If the given :n:`@command` fails, then
-   :n:`Fail @command` succeeds (excepts in the case of
-   critical errors, like a "stack overflow"), without changing the
-   proof state, and in interactive mode, the system prints a message
+   command or a tactic fails. If :n:`@sentence` fails, then
+   :n:`Fail @sentence` succeeds (except for
+   critical errors, such as "stack overflow"), without changing the
+   proof state.  In interactive mode, the system prints a message
    confirming the failure.
 
    .. exn:: The command has not failed!
 
-      If the given :n:`@command` succeeds, then :n:`Fail @command`
+      If the given :n:`@command` succeeds, then :n:`Fail @sentence`
       fails with this error message.
 
+.. note::
+
+   :cmd:`Time`, :cmd:`Redirect`, :cmd:`Timeout` and :cmd:`Fail` are
+   :production:`control_command`\s. For these commands, attributes and goal
+   selectors, when specified, are part of the :n:`@sentence` argument, and thus come after
+   the control command prefix and before the inner command or tactic. For
+   example: `Time #[ local ] Definition foo := 0.` or `Fail Timeout 10 all: auto.`
 
 .. _controlling-display:
 
@@ -1010,13 +876,16 @@ as numbers, and for reflection-based tactics. The commands to fine-
 tune the reduction strategies and the lazy conversion algorithm are
 described first.
 
-.. cmd:: Opaque {+ @qualid }
+.. cmd:: Opaque {+ @smart_qualid }
+
+   This command accepts the :attr:`global` attribute.  By default, the scope
+   of :cmd:`Opaque` is limited to the current section or module.
 
    This command has an effect on unfoldable constants, i.e. on constants
    defined by :cmd:`Definition` or :cmd:`Let` (with an explicit body), or by a command
    assimilated to a definition such as :cmd:`Fixpoint`, :cmd:`Program Definition`, etc,
    or by a proof ended by :cmd:`Defined`. The command tells not to unfold the
-   constants in the :n:`@qualid` sequence in tactics using δ-conversion (unfolding
+   constants in the :n:`@smart_qualid` sequence in tactics using δ-conversion (unfolding
    a constant is replacing it by its definition).
 
    :cmd:`Opaque` has also an effect on the conversion algorithm of |Coq|, telling
@@ -1024,24 +893,15 @@ described first.
    has to check the conversion (see Section :ref:`conversion-rules`) of two distinct
    applied constants.
 
-   .. cmdv:: Global Opaque {+ @qualid }
-      :name: Global Opaque
-
-      The scope of :cmd:`Opaque` is limited to the current section, or current
-      file, unless the variant :cmd:`Global Opaque` is used.
-
    .. seealso::
 
       Sections :ref:`performingcomputations`, :ref:`tactics-automating`,
       :ref:`proof-editing-mode`
 
-   .. exn:: The reference @qualid was not found in the current environment.
-
-      There is no constant referred by :n:`@qualid` in the environment.
-      Nevertheless, if you asked :cmd:`Opaque` `foo` `bar` and if `bar` does
-      not exist, `foo` is set opaque.
+.. cmd:: Transparent {+ @smart_qualid }
 
-.. cmd:: Transparent {+ @qualid }
+   This command accepts the :attr:`global` attribute.  By default, the scope
+   of :cmd:`Transparent` is limited to the current section or module.
 
    This command is the converse of :cmd:`Opaque` and it applies on unfoldable
    constants to restore their unfoldability after an Opaque command.
@@ -1054,16 +914,9 @@ described first.
    the usual defined constants, whose actual values are of course
    relevant in general.
 
-   .. cmdv:: Global Transparent {+ @qualid }
-      :name: Global Transparent
-
-      The scope of Transparent is limited to the current section, or current
-      file, unless the variant :cmd:`Global Transparent` is
-      used.
-
    .. exn:: The reference @qualid was not found in the current environment.
 
-      There is no constant referred by :n:`@qualid` in the environment.
+      There is no constant named :n:`@qualid` in the environment.
 
       .. seealso::
 
@@ -1072,63 +925,66 @@ described first.
 
 .. _vernac-strategy:
 
-.. cmd:: Strategy @level [ {+ @qualid } ]
+.. cmd:: Strategy {+ @strategy_level [ {+ @smart_qualid } ] }
 
-   This command generalizes the behavior of Opaque and Transparent
+   .. insertprodn strategy_level strategy_level
+
+   .. prodn::
+      strategy_level ::= opaque
+      | @int
+      | expand
+      | transparent
+
+   This command accepts the :attr:`local` attribute, which limits its effect
+   to the current section or module, in which case the section and module
+   behavior is the same as :cmd:`Opaque` and :cmd:`Transparent` (without :attr:`global`).
+
+   This command generalizes the behavior of the :cmd:`Opaque` and :cmd:`Transparent`
    commands. It is used to fine-tune the strategy for unfolding
    constants, both at the tactic level and at the kernel level. This
-   command associates a level to the qualified names in the :n:`@qualid`
+   command associates a :n:`@strategy_level` with the qualified names in the :n:`@smart_qualid`
    sequence. Whenever two
    expressions with two distinct head constants are compared (for
    instance, this comparison can be triggered by a type cast), the one
    with lower level is expanded first. In case of a tie, the second one
    (appearing in the cast type) is expanded.
 
-   .. prodn:: level ::= {| opaque | @num | expand }
-
    Levels can be one of the following (higher to lower):
 
     + ``opaque`` : level of opaque constants. They cannot be expanded by
       tactics (behaves like +∞, see next item).
-    + :n:`@num` : levels indexed by an integer. Level 0 corresponds to the
+    + :n:`@int` : levels indexed by an integer. Level 0 corresponds to the
       default behavior, which corresponds to transparent constants. This
-      level can also be referred to as transparent. Negative levels
+      level can also be referred to as ``transparent``. Negative levels
       correspond to constants to be expanded before normal transparent
       constants, while positive levels correspond to constants to be
       expanded after normal transparent constants.
     + ``expand`` : level of constants that should be expanded first (behaves
       like −∞)
+    + ``transparent`` : Equivalent to level 0
 
-    .. cmdv:: Local Strategy @level [ {+ @qualid } ]
+.. cmd:: Print Strategy @smart_qualid
 
-       These directives survive section and module closure, unless the
-       command is prefixed by ``Local``. In the latter case, the behavior
-       regarding sections and modules is the same as for the :cmd:`Transparent` and
-       :cmd:`Opaque` commands.
-
-
-.. cmd:: Print Strategy @qualid
-
-   This command prints the strategy currently associated to :n:`@qualid`. It
-   fails if :n:`@qualid` is not an unfoldable reference, that is, neither a
+   This command prints the strategy currently associated with :n:`@smart_qualid`. It
+   fails if :n:`@smart_qualid` is not an unfoldable reference, that is, neither a
    variable nor a constant.
 
    .. exn:: The reference is not unfoldable.
       :undocumented:
 
-   .. cmdv:: Print Strategies
+.. cmd:: Print Strategies
 
-      Print all the currently non-transparent strategies.
+   Print all the currently non-transparent strategies.
 
 
 .. cmd:: Declare Reduction @ident := @red_expr
 
-   This command allows giving a short name to a reduction expression, for
+   Declares a short name for the reduction expression :n:`@red_expr`, for
    instance ``lazy beta delta [foo bar]``. This short name can then be used
-   in :n:`Eval @ident in` or ``eval`` directives. This command
-   accepts the
-   ``Local`` modifier, for discarding this reduction name at the end of the
-   file or module. For the moment, the name is not qualified. In
+   in :n:`Eval @ident in` or ``eval`` constructs. This command
+   accepts the :attr:`local` attribute, which indicates that the reduction
+   will be discarded at the end of the
+   file or module. The name is not qualified. In
    particular declaring the same name in several modules or in several
    functor applications will be rejected if these declarations are not
    local. The name :n:`@ident` cannot be used directly as an Ltac tactic, but
@@ -1274,14 +1130,15 @@ in support libraries of plug-ins.
 .. _exposing-constants-to-ocaml-libraries:
 
 Exposing constants to OCaml libraries
-````````````````````````````````````````````````````````````````
+`````````````````````````````````````
 
 .. cmd:: Register @qualid__1 as @qualid__2
 
-   This command exposes the constant :n:`@qualid__1` to OCaml libraries under
-   the name :n:`@qualid__2`.  This constant can then be dynamically located
-   calling :n:`Coqlib.lib_ref "@qualid__2"`; i.e., there is no need to known
-   where is the constant defined (file, module, library, etc.).
+   Makes the constant :n:`@qualid__1` accessible to OCaml libraries under
+   the name :n:`@qualid__2`.  The constant can then be dynamically located
+   in OCaml code by
+   calling :n:`Coqlib.lib_ref "@qualid__2"`.  The OCaml code doesn't need
+   to know where the constant is defined (what file, module, library, etc.).
 
    As a special case, when the first segment of :n:`@qualid__2` is :g:`kernel`,
    the constant is exposed to the kernel. For instance, the `Int63` module
@@ -1291,27 +1148,41 @@ Exposing constants to OCaml libraries
 
       Register bool as kernel.ind_bool.
 
-   This makes the kernel aware of what is the type of boolean values. This
-   information is used for instance to define the return type of the
-   :g:`#int63_eq` primitive.
+   This makes the kernel aware of the `bool` type, which is used, for example,
+   to define the return type of the :g:`#int63_eq` primitive.
 
    .. seealso:: :ref:`primitive-integers`
 
 Inlining hints for the fast reduction machines
-````````````````````````````````````````````````````````````````
+``````````````````````````````````````````````
 
 .. cmd:: Register Inline @qualid
 
-   This command gives as a hint to the reduction machines (VM and native) that
+   Gives a hint to the reduction machines (VM and native) that
    the body of the constant :n:`@qualid` should be inlined in the generated code.
 
 Registering primitive operations
 ````````````````````````````````
 
-.. cmd:: Primitive @ident__1 := #@ident__2.
+.. cmd:: Primitive @ident {? : @term } := #@ident__prim
+
+   Makes the primitive type or primitive operator :n:`#@ident__prim` defined in OCaml
+   accessible in |Coq| commands and tactics.
+   For internal use by implementors of |Coq|'s standard library or standard library
+   replacements.  No space is allowed after the `#`.  Invalid values give a syntax
+   error.
+
+   For example, the standard library files `Int63.v` and `PrimFloat.v` use :cmd:`Primitive`
+   to support, respectively, the features described in :ref:`primitive-integers` and
+   :ref:`primitive-floats`.
+
+   The types associated with an operator must be declared to the kernel before declaring operations
+   that use the type.  Do this with :cmd:`Primitive` for primitive types and
+   :cmd:`Register` with the :g:`kernel` prefix for other types.  For example,
+   in `Int63.v`, `#int63_type` must be declared before the associated operations.
+
+   .. exn:: The type @ident must be registered before this construction can be typechecked.
+      :undocumented:
 
-   Declares :n:`@ident__1` as the primitive operator :n:`#@ident__2`. When
-   running this command, the type of the primitive should be already known by
-   the kernel (this is achieved through this command for primitive types and
-   through the :cmd:`Register` command with the :g:`kernel` name-space for other
-   types).
+      The type must be defined with :cmd:`Primitive` command before this
+      :cmd:`Primitive` command (declaring an operation using the type) will succeed.
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 669975ba7e..512378b9fc 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -902,7 +902,7 @@ Syntax of notations
 +++++++++++++++++++
 
 The different syntactic forms taken by the commands declaring
-notations are given below. The optional :production:`scope` is described in
+notations are given below. The optional :n:`@scope` is described in
 :ref:`Scopes`.
 
 .. productionlist:: coq
@@ -1001,6 +1001,11 @@ Notations disappear when a section is closed.
 Interpretation scopes
 ----------------------
 
+   .. insertprodn scope scope
+
+   .. prodn::
+      scope ::= @ident
+
 An *interpretation scope* is a set of notations for terms with their
 interpretations. Interpretation scopes provide a weak, purely
 syntactical form of notation overloading: the same notation, for
@@ -1090,7 +1095,7 @@ Local opening of an interpretation scope
 
 It is possible to locally extend the interpretation scope stack using the syntax
 :n:`(@term)%@ident` (or simply :n:`@term%@ident` for atomic terms), where :token:`ident` is a
-special identifier called *delimiting key* and bound to a given scope.
+special identifier called a *delimiting key* and bound to a given scope.
 
 In such a situation, the term term, and all its subterms, are
 interpreted in the scope stack extended with the scope bound to :token:`ident`.
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 60b845c4be..a01f57eb22 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -151,8 +151,7 @@ fields: [ | DELETENT ]
 
 dirpath: [
 | REPLACE ident LIST0 field
-| WITH ident
-| dirpath field_ident
+| WITH LIST0 ( ident "." ) ident
 ]
 
 binders: [
@@ -220,6 +219,15 @@ tactic_expr0: [
 | WITH "[>" tactic_then_gen "]"
 ]
 
+(* lexer token *)
+IDENT: [
+| ident
+]
+
+scope: [
+| IDENT
+]
+
 operconstr100: [
 | MOVETO term_cast operconstr99 "<:" operconstr200
 | MOVETO term_cast operconstr99 "<<:" operconstr200
@@ -240,7 +248,9 @@ operconstr9: [
 
 operconstr1: [
 | REPLACE operconstr0 ".(" global LIST0 appl_arg ")"
-| WITH operconstr0 ".(" global LIST0 appl_arg ")"
+| WITH    operconstr0 ".(" global LIST0 appl_arg ")" (* huh? *)
+| REPLACE operconstr0 "%" IDENT
+| WITH operconstr0 "%" scope
 | MOVETO term_projection operconstr0 ".(" global LIST0 appl_arg ")"
 | MOVETO term_projection operconstr0 ".(" "@" global LIST0 ( operconstr9 ) ")"
 ]
@@ -364,6 +374,11 @@ pattern10: [
 | DELETE pattern1
 ]
 
+pattern1: [
+| REPLACE pattern0 "%" IDENT
+| WITH pattern0 "%" scope
+]
+
 pattern0: [
 | REPLACE "(" pattern200 ")"
 | WITH "(" LIST1 pattern200 SEP "|" ")"
@@ -419,6 +434,8 @@ gallina: [
 | WITH "Let" "CoFixpoint" corec_definition LIST0 ( "with" corec_definition )
 | REPLACE "Scheme" LIST1 scheme SEP "with"
 | WITH "Scheme" scheme LIST0 ( "with" scheme )
+| REPLACE "Primitive" identref OPT [ ":" lconstr ] ":=" register_token
+| WITH "Primitive" identref OPT [ ":" lconstr ] ":=" "#" identref
 ]
 
 constructor_list_or_record_decl: [
@@ -494,10 +511,6 @@ strategy_flag: [
 | OPTINREF
 ]
 
-export_token: [
-| OPTINREF
-]
-
 functor_app_annot: [
 | OPTINREF
 ]
@@ -536,20 +549,23 @@ gallina_ext: [
 | REPLACE "Generalizable" [ "All" "Variables" | "No" "Variables" | [ "Variable" | "Variables" ] LIST1 identref ]
 | WITH "Generalizable" [  [ "Variable" | "Variables" ] LIST1 identref | "All" "Variables" | "No" "Variables" ]
 
+(* don't show Export for Set, Unset *)
 | REPLACE "Export" "Set" option_table option_setting
-| WITH OPT "Export" "Set" option_table option_setting
+| WITH "Set" option_table option_setting
 | REPLACE "Export" "Unset" option_table
-| WITH OPT "Export" "Unset" option_table
+| WITH "Unset" option_table
 | REPLACE "Instance" instance_name ":" operconstr200 hint_info [ ":=" "{" record_declaration "}" | ":=" lconstr | ]
 | WITH "Instance" instance_name ":" operconstr200 hint_info OPT [ ":=" "{" record_declaration "}" | ":=" lconstr ]
 
+| REPLACE "From" global "Require" export_token LIST1 global
+| WITH "From" dirpath "Require" export_token LIST1 global
 ]
 
-(* lexer stuff *)
-IDENT: [
-| ident
+export_token: [
+| OPTINREF
 ]
 
+(* lexer stuff *)
 integer: [ | DELETENT ]
 RENAME: [
 | integer int (* todo: review uses in .mlg files, some should be "natural" *)
@@ -859,6 +875,7 @@ bar_cbrace: [
 printable: [
 | REPLACE [ "Sorted" | ] "Universes" OPT printunivs_subgraph OPT ne_string
 | WITH OPT "Sorted" "Universes" OPT printunivs_subgraph OPT ne_string
+| DELETE "Term" smart_global OPT univ_name_list  (* readded in commands *)
 | INSERTALL "Print"
 ]
 
@@ -878,15 +895,18 @@ command: [
 | DELETE "Back"
 | REPLACE "Back" natural
 | WITH "Back" OPT natural
-| REPLACE "Test" option_table "for" LIST1 option_ref_value
-| WITH "Test" option_table OPT ( "for" LIST1 option_ref_value )
-| DELETE "Test" option_table
 | REPLACE "Load" [ "Verbose" | ] [ ne_string | IDENT ]
 | WITH "Load" OPT "Verbose" [ ne_string | IDENT ]
 | DELETE "Unset" option_table
-| DELETE "Set" option_table option_setting
+| REPLACE "Set" option_table option_setting
+| WITH OPT "Export" "Set" option_table   (* set flag *)
+| REPLACE "Test" option_table "for" LIST1 option_ref_value
+| WITH "Test" option_table OPT ( "for" LIST1 option_ref_value )
+| DELETE "Test" option_table
+
+(* hide the fact that table names are limited to 2 IDENTs *)
 | REPLACE "Add" IDENT IDENT LIST1 option_ref_value
-| WITH "Add" IDENT OPT IDENT LIST1 option_ref_value
+| WITH "Add" option_table LIST1 option_ref_value
 | DELETE "Add" IDENT LIST1 option_ref_value
 | DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "as" ident
 | DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "as" ident
@@ -941,7 +961,11 @@ command: [
 | REPLACE "Preterm" "of" ident
 | WITH "Preterm" OPT ( "of" ident )
 | DELETE "Preterm"
-| EDIT "Remove" ADD_OPT IDENT IDENT LIST1 option_ref_value
+
+(* hide the fact that table names are limited to 2 IDENTs *)
+| REPLACE "Remove" IDENT IDENT LIST1 option_ref_value
+| WITH "Remove" option_table LIST1 option_ref_value
+| DELETE "Remove" IDENT LIST1 option_ref_value
 | DELETE "Restore" "State" IDENT
 | DELETE "Restore" "State" ne_string
 | "Restore" "State" [ IDENT | ne_string ]
@@ -976,6 +1000,16 @@ command: [
 | REPLACE "Abort" identref
 | WITH "Abort" OPT [ "All" | identref ]
 
+(* show the locate options as separate commands *)
+| DELETE "Locate" locatable
+| locatable
+| REPLACE "Print" smart_global OPT univ_name_list
+| WITH "Print" OPT "Term" smart_global OPT univ_name_list
+
+]
+
+option_setting: [
+| OPTINREF
 ]
 
 only_parsing: [
@@ -1062,9 +1096,7 @@ legacy_attr: [
 | DELETE "NonCumulative"
 ]
 
-vernacular: [
-| LIST0 ( OPT all_attrs [ command | tactic ] "." )
-]
+sentence: [ ]  (* productions defined below *)
 
 rec_definition: [
 | REPLACE ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notations
@@ -1124,7 +1156,7 @@ query_command: [
 | REPLACE "SearchRewrite" constr_pattern in_or_out_modules "."
 | WITH "SearchRewrite" constr_pattern in_or_out_modules
 | REPLACE "Search" searchabout_query searchabout_queries "."
-| WITH "Search" searchabout_query searchabout_queries
+| WITH "Search" searchabout_queries
 ]
 
 vernac_toplevel: [
@@ -1142,37 +1174,25 @@ vernac_toplevel: [
 | DELETE vernac_control
 ]
 
-positive_search_mark: [
-| OPTINREF
-]
-
 in_or_out_modules: [
 | OPTINREF
 ]
 
-searchabout_queries: [
-| OPTINREF
-]
-
 vernac_control: [
 (* replacing vernac_control with command is cheating a little;
    they can't refer to the vernac_toplevel commands.
    cover this the descriptions of these commands *)
 | REPLACE "Time" vernac_control
-| WITH "Time" command
+| WITH "Time" sentence
 | REPLACE "Redirect" ne_string vernac_control
-| WITH "Redirect" ne_string command
+| WITH "Redirect" ne_string sentence
 | REPLACE "Timeout" natural vernac_control
-| WITH "Timeout" natural command
+| WITH "Timeout" natural sentence
 | REPLACE "Fail" vernac_control
-| WITH "Fail" command
+| WITH "Fail" sentence
 | DELETE decorated_vernac
 ]
 
-option_setting: [
-| OPTINREF
-]
-
 orient: [
 | OPTINREF
 ]
@@ -1351,6 +1371,51 @@ module_expr: [
 | DELETE module_expr module_expr_atom
 ]
 
+locatable: [
+| INSERTALL "Locate"
+]
+
+ne_in_or_out_modules: [
+| REPLACE "inside" LIST1 global
+| WITH [ "inside" | "outside" ] LIST1 global
+| DELETE "outside" LIST1 global
+]
+
+searchabout_query: [
+| REPLACE positive_search_mark ne_string OPT scope_delimiter
+| WITH ne_string OPT scope_delimiter
+| REPLACE positive_search_mark constr_pattern
+| WITH constr_pattern
+]
+
+searchabout_queries: [
+| DELETE ne_in_or_out_modules
+| REPLACE searchabout_query searchabout_queries
+| WITH LIST1 ( positive_search_mark searchabout_query ) OPT ne_in_or_out_modules
+| DELETE (* empty *)
+]
+
+positive_search_mark: [
+| OPTINREF
+]
+
+by_notation: [
+| REPLACE ne_string OPT [ "%" IDENT ]
+| WITH ne_string OPT [ "%" scope ]
+]
+
+scope_delimiter: [
+| REPLACE "%" IDENT
+| WITH "%" scope
+]
+
+(* Don't show these details *)
+DELETE: [
+| register_token
+| register_prim_token
+| register_type_token
+]
+
 SPLICE: [
 | noedit_mode
 | bigint
@@ -1435,9 +1500,7 @@ SPLICE: [
 | mode
 | mult_pattern
 | open_constr
-| option_table
 | record_declaration
-| register_type_token
 | tactic
 | uconstr
 | impl_ident_head
@@ -1466,14 +1529,12 @@ SPLICE: [
 | 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
@@ -1486,7 +1547,6 @@ SPLICE: [
 | option_ref_value
 | positive_search_mark
 | in_or_out_modules
-| register_prim_token
 | option_setting
 | orient
 | with_bindings
@@ -1518,6 +1578,10 @@ SPLICE: [
 | ltac_def_kind
 | intropatterns
 | instance_name
+| ne_in_or_out_modules
+| searchabout_queries
+| locatable
+| scope_delimiter
 ] (* end SPLICE *)
 
 RENAME: [
@@ -1567,8 +1631,12 @@ RENAME: [
 | record_binder_body field_body
 | class_rawexpr class
 | smart_global smart_qualid
+| searchabout_query search_item
+| option_table setting_name
 ]
 
+(* todo: positive_search_mark is a lousy name for OPT "-" *)
+
 (* todo: doesn't work if up above... maybe because 'clause' doesn't exist? *)
 clause_dft_concl: [
 | OPTINREF
@@ -1656,3 +1724,18 @@ SPLICE: [
 | tactic_notation_tactics
 ]
 (* todo: ssrreflect*.rst ref to fix_body is incorrect *)
+
+(* not included in insertprodn; defined in rst with :production: *)
+control_command: [ ]
+query_command: [ ] (* re-add since previously spliced *)
+
+sentence: [
+| OPT all_attrs command "."
+| OPT all_attrs OPT ( num ":" ) query_command "."
+| OPT all_attrs OPT toplevel_selector ltac_expr [ "." | "..." ]
+| control_command
+]
+
+vernacular: [
+| LIST0 sentence
+]
diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml
index 1afa2338fd..f00fda0e8c 100644
--- a/doc/tools/docgram/doc_grammar.ml
+++ b/doc/tools/docgram/doc_grammar.ml
@@ -1768,8 +1768,14 @@ let process_rst g file args seen tac_prods cmd_prods =
 (*  in*)
 
   let cmd_replace_files = [
+    "doc/sphinx/language/core/records.rst";
+    "doc/sphinx/language/core/sections.rst";
+    "doc/sphinx/language/extensions/implicit-arguments.rst";
+    "doc/sphinx/language/using/libraries/funind.rst";
+
     "doc/sphinx/language/gallina-specification-language.rst";
-    "doc/sphinx/language/gallina-extensions.rst"
+    "doc/sphinx/language/gallina-extensions.rst";
+    "doc/sphinx/proof-engine/vernacular-commands.rst"
   ]
   in
 
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 272d17bb35..f2b737832f 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -1027,7 +1027,6 @@ gallina_ext: [
 | "Module" "Type" identref LIST0 module_binder check_module_types is_module_type
 | "Declare" "Module" export_token identref LIST0 module_binder ":" module_type_inl
 | "Section" identref
-| "Chapter" identref
 | "End" identref
 | "Collection" identref ":=" section_subset_expr
 | "Require" export_token LIST1 global
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 0c9d7a853b..67f5b8e63f 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -47,7 +47,7 @@ one_term: [
 
 term1: [
 | term_projection
-| term0 "%" ident
+| term0 "%" scope
 | term0
 ]
 
@@ -159,7 +159,20 @@ where: [
 ]
 
 vernacular: [
-| LIST0 ( OPT all_attrs [ command | ltac_expr ] "." )
+| LIST0 sentence
+]
+
+sentence: [
+| OPT all_attrs command "."
+| OPT all_attrs OPT ( num ":" ) query_command "."
+| OPT all_attrs OPT toplevel_selector ltac_expr [ "." | "..." ]
+| control_command
+]
+
+control_command: [
+]
+
+query_command: [
 ]
 
 tacticals: [
@@ -330,7 +343,7 @@ pattern10: [
 ]
 
 pattern1: [
-| pattern0 "%" ident
+| pattern0 "%" scope
 | pattern0
 ]
 
@@ -367,53 +380,6 @@ decl_notation: [
 | string ":=" one_term OPT ( "(" "only" "parsing" ")" ) OPT [ ":" ident ]
 ]
 
-register_token: [
-| "#int63_type"
-| "#float64_type"
-| "#int63_head0"
-| "#int63_tail0"
-| "#int63_add"
-| "#int63_sub"
-| "#int63_mul"
-| "#int63_div"
-| "#int63_mod"
-| "#int63_lsr"
-| "#int63_lsl"
-| "#int63_land"
-| "#int63_lor"
-| "#int63_lxor"
-| "#int63_addc"
-| "#int63_subc"
-| "#int63_addcarryc"
-| "#int63_subcarryc"
-| "#int63_mulc"
-| "#int63_diveucl"
-| "#int63_div21"
-| "#int63_addmuldiv"
-| "#int63_eq"
-| "#int63_lt"
-| "#int63_le"
-| "#int63_compare"
-| "#float64_opp"
-| "#float64_abs"
-| "#float64_eq"
-| "#float64_lt"
-| "#float64_le"
-| "#float64_compare"
-| "#float64_classify"
-| "#float64_add"
-| "#float64_sub"
-| "#float64_mul"
-| "#float64_div"
-| "#float64_sqrt"
-| "#float64_of_int63"
-| "#float64_normfr_mantissa"
-| "#float64_frshiftexp"
-| "#float64_ldshiftexp"
-| "#float64_next_up"
-| "#float64_next_down"
-]
-
 thm_token: [
 | "Theorem"
 | "Lemma"
@@ -601,20 +567,20 @@ smart_qualid: [
 ]
 
 by_notation: [
-| string OPT [ "%" ident ]
+| string OPT [ "%" scope ]
 ]
 
 argument_spec_block: [
 | argument_spec
 | "/"
 | "&"
-| "(" LIST1 argument_spec ")" OPT ( "%" ident )
-| "[" LIST1 argument_spec "]" OPT ( "%" ident )
-| "{" LIST1 argument_spec "}" OPT ( "%" ident )
+| "(" LIST1 argument_spec ")" OPT ( "%" scope )
+| "[" LIST1 argument_spec "]" OPT ( "%" scope )
+| "{" LIST1 argument_spec "}" OPT ( "%" scope )
 ]
 
 argument_spec: [
-| OPT "!" name OPT ( "%" ident )
+| OPT "!" name OPT ( "%" scope )
 ]
 
 more_implicits_block: [
@@ -637,10 +603,14 @@ arguments_modifier: [
 | "extra" "scopes"
 ]
 
+scope: [
+| ident
+]
+
 strategy_level: [
-| "expand"
 | "opaque"
 | int
+| "expand"
 | "transparent"
 ]
 
@@ -660,12 +630,16 @@ command: [
 | "Cd" OPT string
 | "Load" OPT "Verbose" [ string | ident ]
 | "Declare" "ML" "Module" LIST1 string
-| "Locate" locatable
+| "Locate" smart_qualid
+| "Locate" "Term" smart_qualid
+| "Locate" "Module" qualid
+| "Locate" "Ltac" qualid
+| "Locate" "Library" qualid
+| "Locate" "File" string
 | "Add" "LoadPath" string "as" dirpath
 | "Add" "Rec" "LoadPath" string "as" dirpath
 | "Remove" "LoadPath" string
 | "Type" term
-| "Print" "Term" smart_qualid OPT ( "@{" LIST0 name "}" )
 | "Print" "All"
 | "Print" "Section" qualid
 | "Print" "Grammar" ident
@@ -702,18 +676,17 @@ command: [
 | "Print" "Strategy" smart_qualid
 | "Print" "Strategies"
 | "Print" "Registered"
-| "Print" smart_qualid OPT ( "@{" LIST0 name "}" )
+| "Print" OPT "Term" smart_qualid OPT univ_name_list
 | "Print" "Module" "Type" qualid
 | "Print" "Module" qualid
 | "Print" "Namespace" dirpath
 | "Inspect" num
 | "Add" "ML" "Path" string
-| OPT "Export" "Set" LIST1 ident OPT [ int | string ]
-| OPT "Export" "Unset" LIST1 ident
-| "Print" "Table" LIST1 ident
-| "Add" ident OPT ident LIST1 [ qualid | string ]
-| "Test" LIST1 ident OPT ( "for" LIST1 [ qualid | string ] )
-| "Remove" OPT ident ident LIST1 [ qualid | string ]
+| OPT "Export" "Set" setting_name
+| "Print" "Table" setting_name
+| "Add" setting_name LIST1 [ qualid | string ]
+| "Test" setting_name OPT ( "for" LIST1 [ qualid | string ] )
+| "Remove" setting_name LIST1 [ qualid | string ]
 | "Write" "State" [ ident | string ]
 | "Restore" "State" [ ident | string ]
 | "Reset" "Initial"
@@ -806,7 +779,6 @@ command: [
 | "Tactic" "Notation" OPT ( "(" "at" "level" num ")" ) LIST1 ltac_production_item ":=" ltac_expr
 | "Print" "Rewrite" "HintDb" ident
 | "Print" "Ltac" qualid
-| "Locate" "Ltac" qualid
 | "Ltac" tacdef_body LIST0 ( "with" tacdef_body )
 | "Print" "Ltac" "Signatures"
 | "Set" "Firstorder" "Solver" ltac_expr
@@ -861,7 +833,7 @@ command: [
 | "Combined" "Scheme" ident "from" LIST1 ident SEP ","
 | "Register" qualid "as" qualid
 | "Register" "Inline" qualid
-| "Primitive" ident OPT [ ":" term ] ":=" register_token
+| "Primitive" ident OPT [ ":" term ] ":=" "#" ident
 | "Universe" LIST1 ident
 | "Universes" LIST1 ident
 | "Constraint" LIST1 univ_constraint SEP ","
@@ -873,11 +845,10 @@ command: [
 | "Module" "Type" ident LIST0 module_binder LIST0 ( "<:" module_type_inl ) OPT ( ":=" LIST1 module_type_inl SEP "<+" )
 | "Declare" "Module" OPT [ "Import" | "Export" ] ident LIST0 module_binder ":" module_type_inl
 | "Section" ident
-| "Chapter" ident
 | "End" ident
 | "Collection" ident ":=" section_subset_expr
 | "Require" OPT [ "Import" | "Export" ] LIST1 qualid
-| "From" qualid "Require" OPT [ "Import" | "Export" ] LIST1 qualid
+| "From" dirpath "Require" OPT [ "Import" | "Export" ] LIST1 qualid
 | "Import" LIST1 qualid
 | "Export" LIST1 qualid
 | "Include" module_type_inl LIST0 ( "<+" module_expr_inl )
@@ -899,6 +870,8 @@ command: [
 | "Arguments" smart_qualid LIST0 argument_spec_block LIST0 [ "," LIST0 more_implicits_block ] OPT [ ":" LIST1 arguments_modifier SEP "," ]
 | "Implicit" [ "Type" | "Types" ] reserv_list
 | "Generalizable" [ [ "Variable" | "Variables" ] LIST1 ident | "All" "Variables" | "No" "Variables" ]
+| "Set" setting_name OPT [ int | string ]
+| "Unset" setting_name
 | "Open" "Scope" ident
 | "Close" "Scope" ident
 | "Delimit" "Scope" ident "with" ident
@@ -913,15 +886,15 @@ command: [
 | "Eval" red_expr "in" term
 | "Compute" term
 | "Check" term
-| "About" smart_qualid OPT ( "@{" LIST0 name "}" )
-| "SearchHead" one_term OPT ne_in_or_out_modules
-| "SearchPattern" one_term OPT ne_in_or_out_modules
-| "SearchRewrite" one_term OPT ne_in_or_out_modules
-| "Search" searchabout_query OPT searchabout_queries
-| "Time" command
-| "Redirect" string command
-| "Timeout" num command
-| "Fail" command
+| "About" smart_qualid OPT univ_name_list
+| "SearchHead" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
+| "SearchPattern" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
+| "SearchRewrite" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
+| "Search" LIST1 ( OPT "-" search_item ) OPT ( [ "inside" | "outside" ] LIST1 qualid )
+| "Time" sentence
+| "Redirect" string sentence
+| "Timeout" num sentence
+| "Fail" sentence
 | "Drop"
 | "Quit"
 | "BackTo" num
@@ -960,20 +933,15 @@ starredidentref: [
 ]
 
 dirpath: [
-| ident
-| dirpath field_ident
+| LIST0 ( ident "." ) ident
 ]
 
 bignat: [
 | numeral
 ]
 
-locatable: [
-| smart_qualid
-| "Term" smart_qualid
-| "File" string
-| "Library" qualid
-| "Module" qualid
+setting_name: [
+| LIST1 ident
 ]
 
 comment: [
@@ -982,6 +950,15 @@ comment: [
 | num
 ]
 
+search_item: [
+| one_term
+| string OPT ( "%" scope )
+]
+
+univ_name_list: [
+| "@{" LIST0 name "}"
+]
+
 hint: [
 | "Resolve" LIST1 [ qualid | one_term ] OPT hint_info
 | "Resolve" "->" LIST1 qualid OPT num
@@ -1069,21 +1046,6 @@ class: [
 | smart_qualid
 ]
 
-ne_in_or_out_modules: [
-| "inside" LIST1 qualid
-| "outside" LIST1 qualid
-]
-
-searchabout_query: [
-| OPT "-" string OPT ( "%" ident )
-| OPT "-" one_term
-]
-
-searchabout_queries: [
-| ne_in_or_out_modules
-| searchabout_query searchabout_queries
-]
-
 level: [
 | "level" num
 | "next" "level"